Formal Analysis Approach for a Kind of Open-ended Protocols
一类具有“开端”结构的安全协议分析方法研究

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 ...