Computing symbolic models for verifying cryptographic protocols

Abstract

We consider the problem of automatically verifing 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.