Verifying authentication protocols: methodology and example
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The authors present a new approach to the analysis of authentication protocols. The approach consists of several elements: a specification language for formally specifying authentication protocols, a semantic model for characterizing protocol executions, an assertion language for stating secrecy and correspondence properties, and procedures for verifying these properties. The main emphasis of this paper is on the assertion language, its semantics, and verification procedures. In particular, the authors present a set of proof rules. An example is given to illustrate the approach.Keywords
This publication has 15 references indexed in Scilit:
- A semantic model for authentication protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verifying authentication protocols: methodology and examplePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A logic of communication in hostile environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal semantics for logics of cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Applying Formal Methods to the Analysis of a Key Management ProtocolJournal of Computer Security, 1992
- A critique of the Burrows, Abadi and Needham logicACM SIGOPS Operating Systems Review, 1990
- Reasoning about belief in cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1990
- Analyzing encryption protocols using formal verification techniquesIEEE Journal on Selected Areas in Communications, 1989
- Authentication revisitedACM SIGOPS Operating Systems Review, 1987
- A key distribution protocol using event markersACM Transactions on Computer Systems, 1983