TY - GEN
T1 - Safe equivalences for Security properties
AU - Alvim, Mario S.
AU - Andres, Miguel E.
AU - Palamidessi, Catuscia
AU - van Rossum, Peter
PY - 2010/1/1
Y1 - 2010/1/1
N2 - 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 complete-trace equivalence and bisimulation. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe versions of these equivalences. We prove that safe bisimulation is still a congruence. Finally, we show that safe equivalences can be used to establish information-hiding properties.
AB - 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 complete-trace equivalence and bisimulation. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe versions of these equivalences. We prove that safe bisimulation is still a congruence. Finally, we show that safe equivalences can be used to establish information-hiding properties.
U2 - 10.1007/978-3-642-15240-5_5
DO - 10.1007/978-3-642-15240-5_5
M3 - Conference contribution
AN - SCOPUS:79959752910
SN - 3642152392
SN - 9783642152399
T3 - IFIP Advances in Information and Communication Technology
SP - 55
EP - 70
BT - Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Proceedings
PB - Springer New York LLC
T2 - 6th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, TCS 2010, Held as Part of 21st IFIP World Computer Congress, WCC 2010
Y2 - 20 September 2010 through 23 September 2010
ER -