使用组合协议逻辑PCL验证Amended Needham-Schroeder协议

Verification of the Amended Needham-Schroeder Protocol Using Protocol Composition Logic PCL

安全协议的形式化分析和验证一直是信息安全领域的一个重要问题。本文介绍了组合式验证方法以及面向安全协议验证的组合式验证工具PCL,并采用PCL对Amended Needham-Schroeder协议进行了验证,证明该协议满足保密性。在验证中将完整的协议划分为三个子协议,对子协议分别做性质描述和验证,最后将三个子协议组合成完整的协议,通过三个子协议之间前置断言和后置断言的一致性,证明了组合之后的协议满足保密性。

Forraal 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.