14 March 2013 Efficient model checking of network authentication protocol based on SPIN
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.
© (2013) COPYRIGHT Society of Photo-Optical Instrumentation Engineers (SPIE). Downloading of the abstract is permitted for personal use only.
Zhi-hua Tan, Zhi-hua Tan, Da-fang Zhang, Da-fang Zhang, Li Miao, Li Miao, Dan Zhao, 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); doi: 10.1117/12.2010605; https://doi.org/10.1117/12.2010605
PROCEEDINGS
9 PAGES


SHARE
Back to Top