Efficient model checking of network authentication protocol based on SPIN

Zhi-hua Tan; Da-fang Zhang; Li Miao; Dan Zhao

doi:10.1117/12.2010605

Translator Disclaimer

14 March 2013 Efficient model checking of network authentication protocol based on SPIN

Zhi-hua Tan, Da-fang Zhang, Li Miao, Dan Zhao

Author Affiliations +

Proceedings Volume 8768, International Conference on Graphic and Image Processing (ICGIP 2012); 87680C (2013) https://doi.org/10.1117/12.2010605
Event: 2012 International Conference on Graphic and Image Processing, 2012, Singapore, Singapore

Abstract

Model checking is a very useful technique for verifying the network authentication protocols. In order to improve the efficiency of modeling and verification on the protocols with the model checking technology, this paper first proposes a universal formalization description method of the protocol. Combined with the model checker SPIN, the method can expediently verify the properties of the protocol. By some modeling simplified strategies, this paper can model several protocols efficiently, and reduce the states space of the model. Compared with the previous literature, this paper achieves higher degree of automation, and better efficiency of verification. Finally based on the method described in the paper, we model and verify the Privacy and Key Management (PKM) authentication protocol. The experimental results show that the method of model checking is effective, which is useful for the other authentication protocols.

Citation Download Citation

Zhi-hua Tan, Da-fang Zhang, Li Miao, and Dan Zhao "Efficient model checking of network authentication protocol based on SPIN", Proc. SPIE 8768, International Conference on Graphic and Image Processing (ICGIP 2012), 87680C (14 March 2013); https://doi.org/10.1117/12.2010605

ACCESS THE FULL ARTICLE