Verification of the Amended Needham-Schroeder Protocol Using Protocol Composition Logic PCL
Mengjun Li · Computer Engineering and Science · 2008
Formal analysis and verification is an essential problem in information security.In this paper,we introduce a compositional verification method and the tool PCL for security protocol verification.The Amended Needham-Schroeder protocol is verified via PCL and proved to satisfy secrecy property.In the verification,the whole protocol is divided into three sub-protocols,which are separately described and verified.Finally,the three separate verifications are composed according to the correspondence of their preconditions and postconditions,thus the secrecy property of the Amended Needham-Schroeder protocol is proved compositionally.