Knowledge based approach for mechanical lyverifying security protocols
Xiaoqi Ma, Xiaochun Cheng, Rachel McCrindle · 2005
A new knowledge-based security protocol verification approach is proposed in this paper. A number of predicates, functions, assumptions and rules are used to infer the knowledge of participating principals. These items are implemented with Isabelle, which enables mechanical proving. This approach can prove protocols concerning interleaving protocol sessions and can prove the correctness of a medium-sized security protocol in a couple of seconds. The mechanical proofs of a number of important secure properties and then of the correctness of the Needham-Schroeder-Lowe protocol are given as examples to show the effectiveness of this method. 1