Model Checking of IKEv2 Protocol via SPIN
Tianlong Gu · Jisuanji gongcheng · 2006
As one of the model checking tools,SPIN is applied to model and evaluate the IKEv2 protocol,where the Promela model is developed,and LTL(linear temporal logic) specifications of authentication and secrecy are given.The result shows that the tool works well.