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 :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072478
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:04:30 AM
Last modification on : Wednesday, December 18, 2019 - 5:30:30 PM
Long-term archiving on: Sunday, April 4, 2010 - 11:09:36 PM

Identifiers

  • HAL Id : inria-00072478, version 1

Citation

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

Share

Metrics

Record views

230

Files downloads

323