Computing symbolic models for verifying cryptographic protocols
- 1 January 2001
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10636900,p. 160-173
- https://doi.org/10.1109/csfw.2001.930144
Abstract
We consider the problem of automatically verifying infinite-state cryptographic protocols. Specifically, we present an algorithm that given a finite process describing a protocol in a hostile environment (trying to force the system into a "bad" state) computes a model of traces on which security properties can be checked. Because of unbounded inputs from the environment, even finite processes have an infinite set of traces; the main focus of our approach is the reduction of this infinite set to a finite set by a symbolic analysis of the knowledge of the environment. Our algorithm is sound (and we conjecture complete) for protocols with shared-key encryption/decryption that use arbitrary messages as keys; further it is complete in the common and important case in which the cryptographic keys are messages of bounded size.Keywords
This publication has 12 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- A semantic model for authentication protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient finite-state analysis for large security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On the Reachability Problem in Cryptographic ProtocolsPublished by Springer Nature ,2000
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- The inductive approach to verifying cryptographic protocolsJournal of Computer Security, 1998
- Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security ProtocolsPublished by Springer Nature ,1998
- Security properties and CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1996
- The NRL Protocol Analyzer: An OverviewThe Journal of Logic Programming, 1996
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983