05/07/2001: Marcelo Fiore (Univ. Cambridge)
Computing Symbolic Models for Verifying Cryptographic Protocols.
Résumé
(Marcelo Fiore and Martin Abadi)
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.