关键词: Floyd-Hoare逻辑 PCL 安全协议

Abstract:

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 verif ications are composed according to the correspondence of their preconditions and postconditions, thus the secrecy property of the Amended Needham-Schroe der protocol is proved compositionally.

Key words: Floyd-Hoare logic, PCL, security protocol