| Abstract |
|
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.
|
 Additional Information
|
Citation:
Marcelo Fiore, MartÍn Abadi,
"Computing Symbolic Models for Verifying Cryptographic Protocols,"
csfw,
p. 0160,
14th IEEE Computer Security Foundations Workshop (CSFW'01),
2001
|
