The concept of layered proving trees and its application to the automation of security protocol verification

Security protocols are one of the most critical elements in enabling the secure communication and processing of information. The presence of flaws in published protocols highlights the complexity of security protocol design. Only formal verification can provide strong confidence in the correctness of security protocols and is considered an imperative step in their design. This paper presents a new theoretical concept, called Layered Proving Trees, for automatically applying logical postulates in logic-based security protocol verification. An algorithm for the new concept is introduced and the soundness and completeness of the technique is proved. Empirical results on the performance of the algorithm are presented. The presented proofs and empirical results demonstrate the feasibility and effectiveness of the Layered Proving Tree approach.