Verifying privacy by little interaction and no process equivalence
Butin, Denis Frédéric and Bella, Giampaolo (2012) Verifying privacy by little interaction and no process equivalence. In: SECRYPT 2012, 24-27 Jul 2012, Rome, Italy.
Full text available as:
While machine-assisted verification of classical security goals such as confidentiality and authentication is
well-established, it is less mature for recent ones. Electronic voting protocols claim properties such as voter
privacy. The most common modelling involves indistinguishability, and is specified via trace equivalence in cryptographic extensions of process calculi. However, it has shown restrictions. We describe a novel model, based on unlinkability between two pieces of information. Specifying it as an extension to the Inductive Method allows us to establish voter privacy without the need for approximation or session bounding. The two
models and their latest specifications are contrasted.
Archive Staff Only: edit this record