HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

On the Symbolic Reduction of Processes with Cryptographic Functions

Roberto M. Amadio 1 Denis Lugiez Vincent Vanackère
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : 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 NPTIME 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 presented in [DolevEK-IC82].
Document type :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:04:30 AM
Last modification on : Friday, February 4, 2022 - 3:19:52 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:09:36 PM


  • HAL Id : inria-00072478, version 1


Roberto M. Amadio, Denis Lugiez, Vincent Vanackère. On the Symbolic Reduction of Processes with Cryptographic Functions. RR-4147, INRIA. 2001. ⟨inria-00072478⟩



Record views


Files downloads