Share Email Print

Proceedings Paper

Efficient model checking of network authentication protocol based on SPIN
Author(s): Zhi-hua Tan; Da-fang Zhang; Li Miao; Dan Zhao
Format Member Price Non-Member Price
PDF $17.00 $21.00

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

Paper Details

Date Published: 14 March 2013
PDF: 9 pages
Proc. SPIE 8768, International Conference on Graphic and Image Processing (ICGIP 2012), 87680C (14 March 2013); doi: 10.1117/12.2010605
Show Author Affiliations
Zhi-hua Tan, Hunan Univ. (China)
Da-fang Zhang, Hunan Univ. (China)
Li Miao, Hunan Univ. (China)
Dan Zhao, Hunan Univ. (China)

Published in SPIE Proceedings Vol. 8768:
International Conference on Graphic and Image Processing (ICGIP 2012)
Zeng Zhu, Editor(s)

© SPIE. Terms of Use
Back to Top
Sign in to read the full article
Create a free SPIE account to get access to
premium articles and original research
Forgot your username?