Using Unification For Opacity Properties

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 give a simple definition of opacity by looking at the possible traces of the protocol. Our approach draws on a new property over messages called similarity. Then, using rewriting methods close to those used in unification, we demonstrate the decidability of our opacity property. This is only achieved in the case of atomic keys using a method called Key Quantification.