Safe Equivalences for Security Properties - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2010

Safe Equivalences for Security Properties

Résumé

In the field of Security, process equivalences have been used to char- acterize various information-hiding properties (for instance secrecy, anonymity and non-interference) based on the principle that a protocol P with a variable x satisfies such property if and only if, for every pair of secrets s1 and s2 , P [s1 /x ] is equivalent to P [s2 /x ]. We argue that, in the presence of nondeterminism, the above principle relies on the assumption that the scheduler “works for the benefit of the protocol”, and this is usually not a safe assumption. Non-safe equivalences, in this sense, include trace equivalence and bisimulation. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe ver- sions of these equivalences. We then show safe bisimulation is still a congruence. We conclude showing how to use safe equivalences to characterize information- hiding properties.
Fichier principal
Vignette du fichier
paper2.pdf (486.35 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00479674 , version 1 (01-05-2010)
inria-00479674 , version 2 (19-12-2010)

Identifiants

  • HAL Id : inria-00479674 , version 1

Citer

Mário S. Alvim, Miguel E. Andrés, Catuscia Palamidessi, Peter van Rossum. Safe Equivalences for Security Properties. [Research Report] 2010. ⟨inria-00479674v1⟩
375 Consultations
176 Téléchargements

Partager

Gmail Facebook X LinkedIn More