Design And Parse Of Formal Specification Language For Security Protocols

With the speedily development of network technology, the importance of security protocolsis increasing steadily and formal analysis of security protocols has become a hotspot in the areaof network security. Formal specification is the base of formal analysis. Formal specificationtechnology of security protocols is summarized first in this thesis based on which the design offormal specification language for security protocols and the design and implement of a parser isdeeply researched, as follows:Firstly, MSR for security protocol is researched after which MSR is extended to introducesecurity properties predicates to message predicates for the deficiency of MSR in automatedanalysis of security protocols. The low level specification language of security protocols IL isdesigned based on the extended MSR and the whole definition is brought forward. IL can specifythe implement of protocol and its security properties accurately in theory and practice and it iseasy to translate IL into initialization input of back end analysis program.Next, for the reason that IL is neither readable nor easy for common users to specifysecurity protocols, TLA+ is studied as a language for writing TLA specification. PSL is designedas a high level specification language of security protocols and the whole definition is putforward referring to its modularization specification format and the semantic of temporal logic ofactions. PSL is in a manner of role-based specification format and is similar to messagealternation, for which it meets the needs of common users. Further more, PSL has a relationshipwith IL, which ensures that PSL specification of security protocols can be translated into ILspecification of protocols uniquely.Subsequently, for the demand of automated analysis of security protocols, PSL specificationof security protocols should be translated into IL specification. As the IL specification can't berecognized by back end analysis program, it should be also translated into initialization input ofanalysis program. Therefore, a PSL parser and a IL parser are designed and implemented invirtue of Flex and Bison which is the base of translation between the two specification languageand the initialization of analysis program.Further more, to verify the correctness of formal specification and parse system for securityprotocols and to prove the availability of analysis program, a test collection is constructedcomposed of PSL specification for security protocols, then three protocols of different types arechosen from the collection to test the correctness of the automated analysis system for securityprotocols. The results show the system can checks out the attacks of protocols which have beenknown. Besides, the function of parsers is test for error found and parsing time and the resultsshow they can meet the basic needs of the whole system.Finally, the contents of this thesis are concluded and expectation is brought forword for thework in the next stage.