| Title | A Type System for Privacy Properties |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Cortier, Veronique, Grimm, Niklas, Lallemand, Joseph, Maffei, Matteo |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | control theory, Human Behavior, human factor, privacy, Protocols, pubcrawl, resilience, Resiliency, Scalability, symbolic models, type systems |
| 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. |
| URL | http://doi.acm.org/10.1145/3133956.3133998 |
| DOI | 10.1145/3133956.3133998 |
| Citation Key | cortier_type_2017 |
A Type System for Privacy Properties