Effective model checking of IKEv2 protocol based on SPIN
Xiao Mei-hua · Computer Engineering and Applications Journal · 2008
This paper first gives a simple introduction of the Internet Key Exchange Protocol IKEv2,then conducts a modeling and analysis of the protocol by using the famous model checking tool SPIN.The author finds the existing modeling method hardly applicable because of the highly complex structure of IKEv2 protocol,and that it can only be used for some simple protocols due to its poor readability,low automatization and verification efficiency.Thus the paper proposes another method of modeling which overcomes all the above mentioned disadvantages and which is particularly useful for complicated protocols.At last,the verification of the IKEv2 protocol model based on SPIN shows that this protocol is incapable of resisting initiative attack.Based on this discovery,two charts are given describing the attack and a personal view is presented to improve IKEv2 protocol’s ability to protect the identity of initiator.