A Type System for Privacy Properties (Technical Report)

TL;DR

This paper introduces a novel type system for verifying privacy properties like anonymity in security protocols, offering significant speed improvements and enhanced expressiveness over existing tools, including handling complex protocols like Helios e-voting.

Contribution

A sound type system for proving protocol equivalence that works for both bounded and unbounded sessions, with a prototype demonstrating superior performance and expressiveness.

Findings

Significant speed-up over existing tools for bounded sessions

First to encode Helios e-voting protocol faithfully in this context

Prototype tested successfully on various literature protocols

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.