Using Partial-Order Method in the Verification of Security Protocols
This paper compares functions and performances of several special-purpose model checkers, and selects an automatic security protocol analysis system SPFA to verify security protocols. We find there is a respectable sum of redundant nodes in the state space. Analyzing the formation of these redundant states, we try to introduce the idea of partial order reduction to reduce the number of states that need to be analyzed. After improving SPFA by the above approach, we verify the NSPK protocol, and the experimental result clearly implies that the partialorder method we adopted is effective.
partial order reduction independent stutter- equivalent redundant successor
Yanan Ma Nan Liu Yuefei Zhu Zongli Hu
Zhengzhou Information Science and Technology Institute P.O.Box 1001-774, Zhengzhou, Henan 450002, China
国际会议
桂林
英文
351-353
2010-11-17（万方平台首次上网日期，不代表论文的发表时间）