Study On Theory And Applications Of Security Protocols Formal Analysis

Security protocol is a type of communication protocol based on cryptographywhich runs over the computer network or distributed systems. It arranges the executionsteps and rules with the cryptographic algorithms among the participants whoimplement tasks such as key distribution and identity authentication etc. A safe securityprotocol is the basis of information security systems and become one of absolutelynecessary components of network and kinds of applications. However, the securityprotocols do not always achieve their design objectives for the reasons that theirinterleaving runs and the attacker’s deliberate demolishment. Formal methods havebeen proved to be an effective way for the analysis and verification of securityprotocols and have become the focus in the domain of security protocols.In this dissertation, security protocol is the main object of study, and the DDMP isthe main research tool, the formal analysis methods theory and applications are themain research contents. Primary innovative work can be summarized as following：(1) Security protocol formal analysis model is proposed. The system model ofsecurity protocol environment, the general model of formal analysis (named as SPFAM)and the model DDMP-SPFAM which is based on the theory of DDMP are proposed.On the basis of model sketch diagrams, the detailed steps of analysis security protocolformally through the algorithm and fake code. This work can provide guidance forfuture security design and analysis.(2) Formal verification based on protocol compositon logic PCL is studied. Firstly,Helsinki protocol which is the authentication protocol from international standardISO/IEC DIS11770-3is selected as the research object. Then, after discussion ofimplementation、defects and attacks of Helsinki, the amended protocol is proposed.Finally, the formal method to prove the secrecy and authentication of protocol isdiscussed and the amended Helsinki protocol is proved with PCL.(3) The problem of protocol compositon security is researched. Two kinds ofprotocol compositon methods are discussed firstly. One is PCL which is the typicalmember of formal compositon tool based on symbols and the other is UC which comesfrom formal methods based on computation complexity. PCL will be selected as thecurrent tool in the paper. After detailed introduces of sequential and parallelcompositon proving steps of PCL, the typical key agreement protocol Otway-Rees ispresented. The defects and attacks are showed, one improved plan (amended Otway-Rees protocol, AOR） is proposed. The protocol is modelled and the keysecrecy is proved following the rule of modularity. The conclusion showes AORprotocol can satisfy the key secret attribute.(4) The security protocol designation is studied based on informal and formalmethods. The design philosophy is provided informally. The method of protocolderivation system PDS is introduced. However, PDS mailly derive the protocols whichuse public key cryptosystems without a third party. For the status quo, some newcomponents and operations are designed and current PDS system is extended. A seriesof security protocol are derived.