A type system for privacy properties
Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. A type system for privacy properties. In 24th ACM Conference on Computer and Communications Security (CCS'17), pp. 409–423, ACM, Dallas, USA, October 2017.
doi:10.1145/3133956.3133998
Download
Abstract
Mature push button tools have emerged for checking trace properties (e.g. secrecy or authentication) of security protocols. The case of indistinguishability-based privacy properties (e.g. ballot privacy or anonymity) is more complex and constitutes an active research topic with several recent propositions of techniques and tools. We explore a novel approach based on type systems and provide a (sound) type system for proving equivalence of protocols, for a bounded or an unbounded number of sessions. The resulting prototype implementation has been tested on various protocols of the literature. It provides a significant speed-up (by orders of magnitude) compared to tools for a bounded number of sessions and complements in terms of expressiveness other state-of-the-art tools, such as ProVerif and Tamarin: e.g., we show that our analysis technique is the first one to handle a faithful encoding of the Helios e-voting protocol in the context of an untrusted ballot box.
BibTeX
@InProceedings{CGLM-ccs17,
abstract = {Mature push button tools have emerged for checking
trace properties (e.g. secrecy or authentication) of
security protocols. The case of
indistinguishability-based privacy properties
(e.g. ballot privacy or anonymity) is more complex
and constitutes an active research topic with
several recent propositions of techniques and
tools. We explore a novel approach based on type
systems and provide a (sound) type system for
proving equivalence of protocols, for a bounded or
an unbounded number of sessions. The resulting
prototype implementation has been tested on various
protocols of the literature. It provides a
significant speed-up (by orders of magnitude)
compared to tools for a bounded number of sessions
and complements in terms of expressiveness other
state-of-the-art tools, such as ProVerif and
Tamarin: e.g., we show that our analysis technique
is the first one to handle a faithful encoding of
the Helios e-voting protocol in the context of an
untrusted ballot box. },
author = {V\'eronique Cortier and Niklas Grimm and Joseph
Lallemand and Matteo Maffei},
title = {A type system for privacy properties},
booktitle = {24th ACM Conference on Computer and Communications
Security (CCS'17)},
year = 2017,
pages = {409--423},
month = {October},
address = {Dallas, USA},
publisher = {ACM},
doi = {10.1145/3133956.3133998},
}