Verifying Privacy by Little Interaction and No Process Equivalence

Denis Butin, Giampaolo Bella

2012

Abstract

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.

Paper Citation

in Harvard Style

Butin D. and Bella G. (2012). Verifying Privacy by Little Interaction and No Process Equivalence . In Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012) ISBN 978-989-8565-24-2, pages 251-256. DOI: 10.5220/0004043502510256

in Bibtex Style

@conference{secrypt12,
author={Denis Butin and Giampaolo Bella},
title={Verifying Privacy by Little Interaction and No Process Equivalence},
booktitle={Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)},
year={2012},
pages={251-256},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004043502510256},
isbn={978-989-8565-24-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Security and Cryptography - Volume 1: SECRYPT, (ICETE 2012)
TI - Verifying Privacy by Little Interaction and No Process Equivalence
SN - 978-989-8565-24-2
AU - Butin D.
AU - Bella G.
PY - 2012
SP - 251
EP - 256
DO - 10.5220/0004043502510256