inria-00479674, version 2
Safe Equivalences for Security Properties
Mário S. Alvim
1Miguel E. Andrés 2Catuscia Palamidessi
1Peter Van Rossum 2
6th IFIP International Conference on Theoretical Computer Science (TCS 2010) 323 (2010) 55-70
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.
- 1: COMETE (INRIA Saclay - Ile de France)
- INRIA – Polytechnique - X – CNRS : UMR7161
- 2: Computing Science Department (CS)
- Radboud university of Nijmegen
- Domain : Computer Science/Logic in Computer Science
- Available versions : v1 (2010-05-01) v2 (2010-12-19)
- inria-00479674, version 2
- http://hal.inria.fr/inria-00479674
- oai:hal.inria.fr:inria-00479674
- From: Catuscia Palamidessi
- Submitted on: Sunday, 19 December 2010 12:22:28
- Updated on: Monday, 27 December 2010 06:40:41






Associated documents
Export