Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol

In the quest for open systems, standardization of security mechanisms, framework, and protocols are becoming increasingly important. This puts high demands on the correctness of the standards. In this paper we use a formal logic-based approach to protocol analysis introduced by Burrows et al. [1]. We extend this logic to deal with protocols using public key cryptography, and with the notion of duration to capture some time-related aspects. The extended logic is used to analyse an important CCITT standard, the X.509 Authentication Framework. We conclude that protocol analysis can benefit from the use of the notation and that it highlights important aspects of the protocol analysed. Some aspects of the formalism need further study.This research was sponsored by the Royal Norwegian Council for Scientific and Industrial Research under Grant IT 0333.22222, and was performed while K. Gaarder was at Alcatel STK Research Centre.