On the Symbolic Reduction of Processes with Cryptographic Functions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2001

On the Symbolic Reduction of Processes with Cryptographic Functions

Denis Lugiez
  • Fonction : Auteur
Vincent Vanackère
  • Fonction : Auteur

Résumé

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].

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4147.pdf (809.53 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00072478 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00072478 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More