Formal Analysis Approach for a Kind of Open-ended Protocols
Tianlong Gu · 2008
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.We also introduce the ability on modeling the DH problem to Athena according to IKEv2 protocol,a new pruning theorem is given and proved.Based on the research,we analyze IKEv2 protocol,and find a new weakness of authentication.An amendment is given.