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.

URL: http://www.cl.cam.ac.uk/~mpf23/papers/Concurrency/symbmod.ps.gz