Skip to Main content Skip to Navigation
Conference papers

Safe Equivalences for Security Properties

Mário Alvim 1 Miguel Andrés 2 Catuscia Palamidessi 1 Peter van Rossum 2
1 COMETE - Concurrency, Mobility and Transactions
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
Contributor : Catuscia Palamidessi <>
Submitted on : Sunday, December 19, 2010 - 12:22:28 PM
Last modification on : Thursday, March 5, 2020 - 6:25:28 PM
Long-term archiving on: : Saturday, December 3, 2016 - 12:29:05 AM


Files produced by the author(s)




Mário Alvim, Miguel 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⟩



Record views


Files downloads