State space pruning in automatic verification of security protocol
Xuefeng Liu · Jisuanji gongcheng · 2004
Strand Space Model (SSM) is a practical, intuitive and strict formal method for security protocol analysis. Based on SSM, we presented the frame of an automatic verification system of security protocol, AVSP, combined with theorem proving and model checking. We emphasized pruning methods of the state space in it. The experiment results got by authentic property verification of Needham-Schroeder show that these pruning methods can perfectly reduce state search space and prevent state explosion.