¡¡Chinese Journal of Computers   Full Text
  TitleThe Approaches and Technologies for Formal Verification of Security Protocols
  AuthorsXUE Rui FENG Deng-Guo
  Address(State Key Laboratory of Information Security, Institute of Software, Chinese Academy of Sciences, Beijing 100080)
  Year2006
  IssueNo.1(1¡ª20)
  Abstract &
  Background 		The formal methods for verifying security protocols are classified and analyzed from technological points of view. Authors survey the developing history of analyzing approaches and techniques on security protocols; describe the current status, as well as point out the tendency of them. This work comes from authors¡¯ personal research interesting, and it processes in two different lines: The first line follows the trace of emergence and developments of formal methods in verification of security protocols. The other line is to analyze the features when concrete systems are used during verification. The most popular methods and systems are briefly introduced by examples.

keywords secure protocol; formal analysis; security goal; Dolev-Yao model; cryptographic reliability

background This work is supported by the National Natural Science Foundation of China (grant Noª±60373048).
This project is managed to make up the incompleteness and unreliability in the current formal models for analysis of cryptographic protocols, and to complement hardness in operation and intricacy of provable security. To find and design a more advanced formal model for analysis of protocols in which ingredients and concepts of computational complexity should be borrowed so as to bridge the analysis approach of provable security and formal one. It will constitute of three phases. The first phase is to investigate current formal models and find out a succinct and powerful enough model with flexible extensibility so that it is used as the potential candidate. The second phase lies at explorations how to relax the requirement during the implementation of real protocols in the ideal model. The last phase will tend to combine the precedent results to form a securely, easy to operate model for analysis of cryptographic protocols. The results would be of helpful to protocol designers and motivated further development.