On the Symbolic Reduction of Processes with Cryptographic Functions

We study the reachability problem for cryptographic protocols represented as processes relying on perfect cryptographic functions. We introduce a symbolic reduction system that can handle hashing functions, symmetric keys, and public keys. Desirable properties such as secrecy or authenticity are specified by inserting logical assertions in the processes.We show that the symbolic reduction system provides a flexible decision procedure for finite processes and a reference for sound implementations. The symbolic reduction system can be regarded as a variant of syntactic unification which is compatible with certain set-membership constraints. For a significant fragment of our formalism, we argue that a dag implementation of the symbolic reduction system leads to an algorithm running in nptime thus matching the lower bound of the problem.In the case of iterated or finite control processes, we show that the problem is undecidable in general and in ptime for a subclass of iterated processes that do not rely on pairing. Our technique is based on rational transductions of regular languages and it applies to a class of processes containing the ping-pong protocols studied in 1982 by Dolev, Even and Karp.