Analvsis And Development On Formal Method Of Secruity Protocol Based On Strand Space Model

The network technology is a double-edged sword, which not only providesconvenient communication to people, but also brings serious threat to informationsecurity. The security of information mainly relies on good encryption/decryptionalgorithm to realize at the early stage. However, with the increasement of networkopen nature and enhancement of application diversity, other methods are needed tosolve this problem well. With the aid of cryptographic algorithm and protocol logic,security protocols achieved the goal providing many kinds of security service, andhave been the foundation of network security. The formal analysis of securityprotocol refers to using a kind of formal language or model, constructing models forthe entities and environment of security protocol, and proving the security ofprotocol in accordance with stipulated hypothesis, analysis and proof technique.Through nearly three decades of development, formal analysis of security protocol isimmature yet. The emergence of strand space theory sets off a new upsurge ofsecurity protocols formal analysis. In strand space model, the partial structureconcept reflecting cause relation between nodes is introduced to effectively resolvethe state-explosion problem universal existed in model check methods. Furthermore,the progress of protocol implement can be indicated with graphic, so graphic theoryand algorithms can be used to analyze the security protocol.Strand space model is originally designed to analyze static protocols or protocolswith less participating entities, such as authentication protocols. As to dynamic ormore participating entities protocols, strand space model cannot analyze thoseprotocols effectively, therefore it is necessary to study it further. This thesis makes anin-depth research on strand space model, then extends it and gets some new researchresults. Related efforts result in following major innovative achievements：(1) Anonymity formal analysis based on strand space mode is an importantcomponent of anonymity analysis field. However, research in this area hasjust begun. Based on equivalent bundles and combined view angle withanonymity, each kind of anonymity is defined in different view angles,and then anonymity degrees among them are compared. Thus, ananonymity formalization framework based on strand space model wasextended and completed. In addition, a zone-based k-anonymity routing protocol is taken as an example to verify that new framework can be usedto point out the shortcoming of the protocol with less anonymity degreeand guide researchers to improve it.(2) Strand space model is extended to analyze more complex protocol: Adhoc secure routing protocol. The consistency condition and arbitraryintermediator credibility condition of ad hoc secure routing protocol arebrought up, and then an attack which leads to SRP returning a nonexistentroute is taken as an example to verify the correctness of the arbitraryintermediator credibility condition.(3) Strand space model is mainly used to prove the correctness of a protocol,and it is difficult to apply it directly to find the protocol leaks and get thecause of the leaks or how to improve it. During the progress of analysis onsecurity routing protocol, strand space model only formalize messagesequence of each route node, ignoring message verification progress ofthem. All kinds of attacking means of adversary node are researched indetail and inverse thinking is used, then an analysis model for protocolattacks, which leads to a nonexistent route accepted by protocol, isdesigned.