A Formal Description And Security Analysis Of A Digital Signature System

This society is an information society, the internal information and files of some companies are evolving to digital from papery. E-mails, digital documents, digital chatting records, digital file abstracts, digital archives, are becoming the main way of managing documents in companies instead of papery documents. Digital documents make cost down, protect environments, and raise efficiency, which is preferred by many companies and organizations. But digital documents don't has force ad effect until August 2004, ( for short) was issued. The main purpose of this paper is to develop a digital signature system software which can fit the requirements of the , and analysis and validates the security of this software, prove the software does guarantee the availability of the digital signature.The main content of his paper is a formal description of a digital signature system software which can fit the requirements of digital signatures which is regulated by , and analysis the security protocols which is used in the software using the formal modeling tool for network security protocols—GSPM, and use an automatic security protocol validating tool based on GSPM which named GSPMC to validate the security protocols which is used in the digital signature system software. Last, we give the results that whether the security of the digital signature system can fit the requirements, and extend the security of the digital signature system to the World Wide Web from a LAN, discuss some large-scale instance.This paper firstly expounds the meaning of the developing of the digital signature system and the effect and the meaning of the security validating of the digital signature system. Secondly, we summarize some main methods of formal modeling of security protocols simply and introduced the formal modeling language for security protocols—GSPM particularly, and expound that why we use GSPM as the formal modeling tool in this paper. Mean a while, we introduced an automatic formal validating tool for security protocols—GSPMC, and expound why GSPMC is credible. Thirdly, we expound the structure of the digital signature system particularly, and analysis and validate the security protocols used in the digital signature system in LAN or in World Wide Web using GSPM and GSPMC.The main method we used in this paper is formal modeling. We find out the security protocols used in the digital signature system and formalize it with GSPM, and analysis it with the automatic validating tool based on GSPM—GSPMC, and raise results and resolves.In this paper, we give the result that there are no leeks of secrecy and authentication in the security protocols used in the digital signature system under the World Wide Web and LAN; and analysis the hidden troubles of security in other aspects and raise resolves. This result can provide advice for the improvement and perfect of the digital signature system, and has some reference value for the future development of the future digital systems.