Laurent Mazare
Decidability Of Opacity With Non-Atomic Keys (2004)
Decidability Of Opacity With Non-Atomic Keys (2004)
TR-2004-23.ps
Keywords: Opacity, Security, Formal Verification, Dolev-Yao Constraints, Rewriting Systems, Decidability
Abstract: The most studied property, secrecy, is not always sufficient to prove the security of a protocol. Other properties such as anonymity, privacy or opacity could be useful. Here, we use a simple definition of opacity which works by looking at the possible traces of the protocol using a new property over messages called similarity. The opacity property becomes a logical constraint involving both similarities and syntactic equalities. The main theorem proves that satisfiability of these constraints and thus opacity are decidable without having to make the hypothesis of atomic keys. Moreover, we use syntactic equalities to model some deductions an intruder could make by performing bit-to-bit comparisons (i.e. known-ciphertext attack)
