Paper 2025/2022
Formal Verification of Privacy Pass
, University of Surrey, University of Surrey, University of SurreyAbstract
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 with which a user must solve CAPTCHAs, Privacy Pass (Davidson et al. 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 symbolic 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 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 computational proofs to show our scheme also maintains cryptographic security. Moreover, our work also highlights the complementary nature of analysing protocols in both symbolic and computational models.
Note: Updates to Tamarin models and new security proofs.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Preprint.
- Keywords
- Formal VerificationPrivacyUnforgeability
- Contact author(s)
-
k ivanova @ surrey ac uk
daniel gardham @ surrey ac uk
s wesemeyer @ surrey ac uk - History
- 2026-02-02: last of 2 revisions
- 2025-10-30: received
- See all versions
- Short URL
- https://ia.cr/2025/2022
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2025/2022,
author = {Kristiana Ivanova and Daniel Gardham and Stephan Wesemeyer},
title = {Formal Verification of Privacy Pass},
howpublished = {Cryptology {ePrint} Archive, Paper 2025/2022},
year = {2025},
url = {https://eprint.iacr.org/2025/2022}
}
