Personal tools
You are here: Home Events Abstract Archives 2001 Computing Symbolic Models for Verifying Cryptographic Protocols

Computing Symbolic Models for Verifying Cryptographic Protocols

Marcelo Fiore Cambridge Computing Laboratory 4pm, Thursday 15 February 2001 Room 2511, JCMB, King's Buildings


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.


Document Actions