Safe Equivalences for Security Properties - Theoretical Computer Science
Conference Papers Year : 2010

Safe Equivalences for Security Properties

Abstract

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
main.pdf (297.2 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

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

Identifiers

Cite

Mário S. Alvim, Miguel E. Andrés, Catuscia Palamidessi, Peter van Rossum. Safe Equivalences for Security Properties. 6th IFIP International Conference on Theoretical Computer Science (TCS 2010), Sep 2010, Brisbane, Australia. pp.55-70, ⟨10.1007/978-3-642-15240-5_5⟩. ⟨inria-00479674v2⟩
419 View
198 Download

Altmetric

Share

More