A logical language for specifying cryptographic protocol requirements
Open Access
- 31 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 165-177
- https://doi.org/10.1109/risp.1993.287634
Abstract
A formal language is presented for specifying and reasoning about cryptographic protocol requirements. Examples of simple sets of requirements in that language are given. The authors examine two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. They also show how to map one of the sets of formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that one version of the protocol meets those requirements. The Analyzer is used as a model checker to assess the validity of the formulas that make up the requirements.Keywords
This publication has 13 references indexed in Scilit:
- On message integrity in cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A system for the specification and analysis of key management protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- The use of logic in the analysis 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
- The Logic of TimePublished by Springer Nature ,1991
- A critique of the Burrows, Abadi and Needham logicACM SIGOPS Operating Systems Review, 1990
- Rejoinder to NessettACM SIGOPS Operating Systems Review, 1990
- A logic of authenticationACM Transactions on Computer Systems, 1990
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983