Formal analysis of cryptographic protocols in a knowledge algorithm logic framework

Logics for security protocol analysis require the formalization of an intruder model that specifies the capabilities of intruders. In this paper, we present a logic for security protocol analysis using knowledge algorithm under the Dolev-Yao model. Intruders are assumed to use algorithms to compute explicitly their knowledge, as well as intruder capabilities are captured by suitable restrictions on the algorithms used. The knowledge completeness of intruder capabilities is proved for model checking of cryptographic protocols. To reduce the model checking complexity, we develop some novel analysis strategies to simplify the intruder knowledge representation in this framework. For illustration purposes, we explore the use of SPIN for the security properties verification of BAN-Yahalom protocol and Helsinki protocol. Three attacks are found in only one general model about BAN-Yahalom protocol, and the Horng-Hsu attack to Helsinki protocol is exposed too. The experimental results show the verification validity and effectiveness.