Safe Equivalences for Security Properties

Abstract. In the field of Security, process equivalences have been used to characterize 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 versions of these equivalences. We then show safe bisimulation is still a congruence. We conclude showing how to use safe equivalences to characterize informationhiding properties.

• Type: Journal
• Year: 2010
• Where: IFIPTCS
• Authors: Mário S. Alvim, Miguel E. Andrés, Catuscia Palamidessi, Peter van Rossum
• Keywords: IFIPTCS 2010, Non-safe Equivalences, Safe, Theoretical Computer Science, Various Information-hiding Properties