Research On Athena For Formal Verification Of Security Protocols Based On Strand Spaces

Among many formal methods for security protocol analysis, the approach based on strand spaces theory is one of the hotspot. There are two important events in the history of strand spaces, one is authentication tests proposed by Joshua D. Guttman, the other is Athena which is a new efficient automated approach for security protocol proposed by D. Song. The aim of this task is to analyze the Athena approach and to extend this approach according to analysis of Open-ended protocol and limitation of Athena. The main results obtained are as follows:(1) This paper discusses Athena systematically, introduces Athena's assumption, its syntax and semantics, and discusses merits and limitation of this Logic. We detailedly describe the core verification algorithm of Athena, analysis what actually makes Athena successful in fast and automatic verification of security protocol. We also point out the defects of this algorithm, discuss the reason and give the way to solve it. Finally, the future direction in this field is discussed.(2) Athena approach can not analyze some complex security protocols because of their poor cryptographic primitives. This paper extends theory of Athena approach according to IKEv2 protocol. The structure of Message terms is extended through adding cryptographic primitives, so it can deals with the problem of DH key agreement; interm relation is modified;So is the relevant propositions or theorems.(3) The formal analysis of Open-Ended Protocols is one of emerging areas of research. The IKEv2 protocol offers a complex example. Our work is based on Athena which is an efficient automatic checking approach. We introduce set theory to deal with Open-ended structure. The new notion of message terms, substitution and the penetrator model are given and the relevant propositions or theorem such as interm relation, goal and goal-binding are therefore modified and proved. A new relation is proposed which is used in order to keep the character of Athena approach. Based on the research, we analysis IKEv2 protocol, and find a new weakness of authentication. An amendment is given.