2017/08/28 by Véronique Cortier, Niklas Grimm, Cortier, Véronique +5
Computer Science · #Advanced Authentication Protocols Security #Cryptography and Data Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Programming Languages (cs.PL) #User Authentication and Security Systems
paper · pdf · doi:10.48550/arxiv.1708.08340
openalex publication_date 2017/08/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.