Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol |
| |
Authors: | Klaus Gaarder Einar Snekkenes |
| |
Affiliation: | (1) Norwegian Telecom Research Department, P.O. Box 83, N-2007 Kjeller, Norway;(2) Alcatel STK Research Centre, Secure Information Systems, Økern, P.O. Box 60, 5 Oslo, Norway |
| |
Abstract: | 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. |
| |
Keywords: | Formal methods Cryptographic protocols Authentication |
本文献已被 SpringerLink 等数据库收录! |
|