A method for proving observational equivalence

Véronique Cortier 1 Stéphanie Delaune 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy (expressed as a reachability property) or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require the notion of observational equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography. In this paper, we consider the applied pi calculus and we show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. Then, for simple processes without replication nor else branch, we reduce the decidability of trace equivalence to deciding an equivalence relation introduced by M. Baudet. Altogether, this yields the first decidability result of observational equivalence for a general class of equational theories.
Type de document :
Communication dans un congrès
22nd IEEE Computer Security Foundations Symposium - CSF'09, Jul 2009, Port Jefferson, United States. IEEE Computer Society Press, pp.266-276, 2009
Liste complète des métadonnées

https://hal.inria.fr/inria-00426622
Contributeur : Véronique Cortier <>
Soumis le : mardi 27 octobre 2009 - 09:40:41
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00426622, version 1

Citation

Véronique Cortier, Stéphanie Delaune. A method for proving observational equivalence. 22nd IEEE Computer Security Foundations Symposium - CSF'09, Jul 2009, Port Jefferson, United States. IEEE Computer Society Press, pp.266-276, 2009. 〈inria-00426622〉

Partager

Métriques

Consultations de la notice

163