Welcome to the resource topic for 2025/2022
Title:
Formal Verification of Privacy Pass
Authors: Kristiana Ivanova, Daniel Gardham, Stephan Wesemeyer
Abstract:CAPTCHA is a ubiquitous challenge-response system for preventing spam (typically bots) on the internet. Requiring users to solve visual challenges, its design is inherently cumbersome, and can unfairly punish those using low reputation IP addresses, such as anonymous services e.g. TOR.
To minimise the frequency in which a user must solve CAPTCHAs, Privacy Pass (PETS 2018) allows users to collect and spend anonymous tokens instead of solving challenges. Despite 400,000 reported monthly users and standardisation efforts by the IETF, it has not been subject of formal verification, which has been proven to be a valuable tool in security analysis.
In this paper we perform the first analysis of Privacy Pass using formal verification tools, and verify standard security properties hold in the symbolic model. Motivated by concerns of Davidson et al. and the IETF contributors, we also explore a stronger attack model, where additional key leakage uncovers a potential token forgery. We present a new protocol, Privacy Pass Plus, in which we show the attack fails in the symbolic model and give new cryptographic reductions to show our scheme maintains the security properties. Moreover, our work also highlights the complementary nature of analysing protocols in both symbolic and computational models.
ePrint: https://eprint.iacr.org/2025/2022
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .