Verifying Indistinguishability of Privacy-Preserving Protocols
Article No.: 273, Pages 1442 - 1469
Abstract
Internet users rely on the protocols they use to protect their private information including their identity and the websites they visit. Formal verification of these protocols can detect subtle bugs that compromise these protections at design time, but is a challenging task as it involves probabilistic reasoning about random sampling, cryptographic primitives, and concurrent execution. Existing approaches either reason about symbolic models of the protocols that sacrifice precision for automation, or reason about more precise computational models that are harder to automate and require cryptographic expertise. In this paper we propose a novel approach to verifying privacy-preserving protocols that is more precise than symbolic models yet more accessible than computational models. Our approach permits direct-style proofs of privacy, as opposed to indirect game-based proofs in computational models, by formalizing privacy as indistinguishability of possible network traces induced by a protocol. We ease automation by leveraging insights from the distributed systems verification community to create sound synchronous models of concurrent protocols. Our verification framework is implemented in F* as a library we call Waldo. We describe two large case studies of using Waldo to verify indistinguishability; one on the Encrypted Client Hello (ECH) extension of the TLS protocol and another on a Private Information Retrieval (PIR) protocol. We uncover subtle flaws in the TLS ECH specification that were missed by other models.
References
[1]
Martin Abadi. 1999. Secrecy by typing in security protocols. Journal of the ACM (JACM), 46, 5 (1999), 749–786. https://doi.org/10.1145/324133.324266
[2]
Nadhem J. Al Fardan and Kenneth G. Paterson. 2013. Lucky Thirteen: Breaking the TLS and DTLS Record Protocols. In 2013 IEEE Symposium on Security and Privacy. 526–540. https://doi.org/10.1109/SP.2013.42
[3]
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Gregoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran. 2019. A Machine-Checked Proof of Security for AWS Key Management Service. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS ’19). Association for Computing Machinery, New York, NY, USA. 63–78. isbn:9781450367479 https://doi.org/10.1145/3319535.3354228
[4]
Nimrod Aviram, Sebastian Schinzel, Juraj Somorovsky, Nadia Heninger, Maik Dankel, Jens Steube, Luke Valenta, David Adrian, J Alex Halderman, and Viktor Dukhovni. 2016. DROWN: Breaking TLS using sslv2. In 25th USENIX Security Symposium (USENIX Security 16). 689–706.
[5]
Michael Backes and Birgit Pfitzmann. 2002. Computational Probabilistic Non-interference. In Computer Security — ESORICS 2002, Dieter Gollmann, Günther Karjoth, and Michael Waidner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–23. isbn:978-3-540-45853-1 https://doi.org/10.1007/s10207-004-0039-7
[6]
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In 2021 IEEE Symposium on Security and Privacy (SP). 777–795. https://doi.org/10.1109/SP40001.2021.00008
[7]
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology – CRYPTO 2011, Phillip Rogaway (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 71–90. isbn:978-3-642-22792-9 https://doi.org/10.1007/978-3-642-22792-9_5
[8]
Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. SIGPLAN Not., 44, 1 (2009), jan, 90–101. issn:0362-1340 https://doi.org/10.1145/1594834.1480894
[9]
David Basin, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, and Vincent Stettler. 2018. A Formal Analysis of 5G Authentication. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS ’18). Association for Computing Machinery, New York, NY, USA. 1383–1396. isbn:9781450356930 https://doi.org/10.1145/3243734.3243846
[10]
Donald Beaver and Joan Feigenbaum. 1990. Hiding instances in multioracle queries. In STACS 90, Christian Choffrut and Thomas Lengauer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 37–48. isbn:978-3-540-46945-2 https://doi.org/10.1007/3-540-52282-4_30
[11]
Amos Beimel, Yuval Ishai, Eyal Kushilevitz, and Ilan Orlov. 2012. Share Conversion and Private Information Retrieval. In 2012 IEEE 27th Conference on Computational Complexity. 258–268. https://doi.org/10.1109/CCC.2012.23
[12]
Yves Bertot and Pierre Castran. 2010. Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions (1st ed.). Springer Publishing Company, Incorporated. isbn:3642058809
[13]
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoue. 2017. A Messy State of the Union: Taming the Composite State Machines of TLS. Commun. ACM, 60, 2 (2017), jan, 99–107. issn:0001-0782 https://doi.org/10.1145/3023357
[14]
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. 2021. DY^⋆ : A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P). 523–542. https://doi.org/10.1109/EuroSP51992.2021.00042
[15]
Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified models and reference implementations for the TLS 1.3 standard candidate. In 2017 IEEE Symposium on Security and Privacy (SP). 483–502. https://doi.org/10.1109/SP.2017.26
[16]
Karthikeyan Bhargavan, Vincent Cheval, and Christopher Wood. 2022. A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS ’22). Association for Computing Machinery, New York, NY, USA. 365–379. isbn:9781450394505 https://doi.org/10.1145/3548606.3559360
[17]
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with Verified Cryptographic Security. In 2013 IEEE Symposium on Security and Privacy. 445–459. https://doi.org/10.1109/SP.2013.37
[18]
Karthikeyan Bhargavan, Antoine Delignat Lavaud, Cédric Fournet, Alfredo Pironti, and Pierre Yves Strub. 2014. Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. In 2014 IEEE Symposium on Security and Privacy. 98–113. https://doi.org/10.1109/SP.2014.14
[19]
Bruno Blanchet. 2008. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Transactions on Dependable and Secure Computing, 5, 4 (2008), 193–207. https://doi.org/10.1109/TDSC.2007.1005
[20]
Bruno Blanchet. 2016. Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends® in Privacy and Security, 1, 1-2 (2016), 1–135. https://doi.org/10.1561/3300000004
[21]
Niklas Broberg, Bart van Delft, and David Sands. 2013. Paragon for practical programming with information-flow control. In Asian Symposium on Programming Languages and Systems. 217–232. https://doi.org/10.1007/978-3-319-03542-0_16
[22]
Zimo Chai, Amirhossein Ghafari, and Amir Houmansadr. 2019. On the importance of encrypted-SNI (ESNI) to censorship circumvention. In 9th USENIX Workshop on Free and Open Communications on the Internet (FOCI 19).
[23]
Benny Chor, Eyal Kushilevitz, Oded Goldreich, and Madhu Sudan. 1998. Private Information Retrieval. J. ACM, 45, 6 (1998), nov, 965–981. issn:0004-5411 https://doi.org/10.1145/293347.293350
[24]
Veronique Cortier, David Galindo, and Mathieu Turuani. 2018. A Formal Analysis of the Neuchatel e-Voting Protocol. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P). 430–442. https://doi.org/10.1109/EuroSP.2018.00037
[25]
Véronique Cortier and Cyrille Wiedling. 2017. A formal analysis of the Norwegian E-voting protocol. Journal of Computer Security, 25, 1 (2017), 21–57. https://doi.org/10.3233/JCS-15777
[26]
Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. A comprehensive symbolic analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 1773–1788. https://doi.org/10.1145/3133956.3134063
[27]
Cas Cremers, Marko Horvat, Sam Scott, and Thyla van der Merwe. 2016. Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication. In 2016 IEEE Symposium on Security and Privacy (SP). 470–485. https://doi.org/10.1109/SP.2016.35
[28]
Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Beguelin, Karthikeyan Bhargavan, Jianyang Pan, and Jean Karim Zinzindohoue. 2017. Implementing and Proving the TLS 1.3 Record Layer. In 2017 IEEE Symposium on Security and Privacy (SP). 463–482. https://doi.org/10.1109/SP.2017.58
[29]
Giovanni Di Crescenzo, Tal Malkin, and Rafail Ostrovsky. 2000. Single Database Private Information Retrieval Implies Oblivious Transfer. In Advances in Cryptology — EUROCRYPT 2000, Bart Preneel (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 122–138. isbn:978-3-540-45539-4 https://doi.org/10.1007/3-540-45539-6_10
[30]
Danny Dolev and Andrew Yao. 1983. On the security of public key protocols. IEEE Transactions on Information Theory, 29, 2 (1983), 198–208. https://doi.org/10.1109/TIT.1983.1056650
[31]
Cédric Fournet and Tamara Rezk. 2008. Cryptographically sound implementations for typed information-flow security. ACM SIGPLAN Notices, 43, 1 (2008), 323–335. https://doi.org/10.1145/1328897.1328478
[32]
Sergiu Gatlan. 2019. South Korea is Censoring the Internet by Snooping on SNI Traffic. Bleeping Computer, 13 Feb, https://www.bleepingcomputer.com/news/security/south-korea-is-censoring-the-internet-by-snooping-on-sni-traffic/
[33]
Yael Gertner, Yuval Ishai, Eyal Kushilevitz, and Tal Malkin. 1998. Protecting data privacy in private information retrieval schemes. In Proceedings of the thirtieth annual ACM symposium on Theory of computing. 151–160. https://doi.org/10.1145/276698.276723
[34]
Jeremy Gibbons and Ralf Hinze. 2011. Just Do It: Simple Monadic Equational Reasoning. SIGPLAN Not., 46, 9 (2011), sep, 2–14. issn:0362-1340 https://doi.org/10.1145/2034574.2034777
[35]
Guillaume Girol, Lucca Hirschi, Ralf Sasse, Dennis Jackson, Cas Cremers, and David Basin. 2020. A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols. In 29th USENIX Security Symposium (USENIX Security 20). 1857–1874.
[36]
James W Gray III. 1992. Toward a mathematical foundation for information flow security. Journal of Computer Security, 1, 3-4 (1992), 255–294. https://doi.org/10.3233/JCS-1992-13-405
[37]
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin. 2018. A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. 130–145. https://doi.org/10.1145/3167090
[38]
Yuval Ishai, Eyal Kushilevitz, and Rafail Ostrovsky. 2005. Sufficient Conditions for Collision-Resistant Hashing. In Theory of Cryptography, Joe Kilian (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 445–456. isbn:978-3-540-30576-7 https://doi.org/10.1007/978-3-540-30576-7_24
[39]
Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In 2017 IEEE European symposium on security and privacy (EuroS&P). 435–450. https://doi.org/10.1109/EuroSP.2017.38
[40]
Nadim Kobeissi, Georgio Nicolas, and Karthikeyan Bhargavan. 2019. Noise Explorer: Fully automated modeling and verification for arbitrary Noise protocols. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P). 356–370. https://doi.org/10.1109/EuroSP.2019.00034
[41]
Elisavet Kozyri, Stephen Chong, and Andrew C. Myers. 2022. Expressing Information Flow Properties. Foundations and Trends® in Privacy and Security, 3, 1 (2022), 1–102. issn:2474-1558 https://doi.org/10.1561/3300000008
[42]
Peeter Laud. 2003. Handling encryption in an analysis for secure information flow. In European Symposium on Programming. 159–173. https://doi.org/10.1007/3-540-36575-3_12
[43]
Peng Li and Steve Zdancewic. 2010. Arrows for secure information flow. Theoretical computer science, 411, 19 (2010), 1974–1994. https://doi.org/10.1016/j.tcs.2010.01.025
[44]
Benjamin Lipp, Bruno Blanchet, and Karthikeyan Bhargavan. 2019. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P). 231–246. https://doi.org/10.1109/EuroSP.2019.00026
[45]
Richard J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM, 18, 12 (1975), dec, 717–721. issn:0001-0782 https://doi.org/10.1145/361227.361234
[46]
Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In International conference on computer aided verification. 696–701. https://doi.org/10.1007/978-3-642-39799-8_48
[47]
Bodo Möller, Thai Duong, and Krzysztof Kotowicz. 2014. This POODLE bites: exploiting the SSL 3.0 fallback. Security Advisory, 21 (2014), 34–58.
[48]
K.R. O’Neill, M.R. Clarkson, and S. Chong. 2006. Information-flow security for interactive programs. In 19th IEEE Computer Security Foundations Workshop (CSFW’06). 12 pp.–201. https://doi.org/10.1109/CSFW.2006.16
[49]
E. Rescorla, K. Oku, N. Sullivan, and C.A. Wood. 2022. TLS Encrypted Client Hello. IETF Secretariat. https://datatracker.ietf.org/doc/html/draft-ietf-tls-esni-15
[50]
Juliano Rizzo and Thai Duong. 2012. The CRIME Attack. In EKOparty Security Conference.
[51]
A. Sabelfeld and D. Sands. 2005. Dimensions and principles of declassification. In 18th IEEE Computer Security Foundations Workshop (CSFW’05). 255–269. https://doi.org/10.1109/CSFW.2005.15
[52]
B. Schwartz, M. Bishop, and E. Nygren. 2021. Service binding and parameter specification via the DNS (DNS SVCB and HTTPS RRs). IETF Secretariat. https://datatracker.ietf.org/doc/html/draft-ietf-dnsop-svcb-https-08
[53]
Adi Shamir. 1979. How to Share a Secret. Commun. ACM, 22, 11 (1979), nov, 612–613. issn:0001-0782 https://doi.org/10.1145/359168.359176
[54]
Geoffrey Smith and Rafael Alpízar. 2006. Secure information flow with random assignment and encryption. In Proceedings of the fourth ACM workshop on Formal methods in security. 33–44. https://doi.org/10.1145/1180337.1180341
[55]
Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, and Markulf Kohlweiss. 2016. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 256–270. https://doi.org/10.1145/2837614.2837655
[56]
The Coq Development Team. 2023. The Coq Proof Assistant. https://doi.org/10.5281/zenodo.1003420
[57]
U.S. CIO Council. 2016. HTTPS. https://https.cio.gov/ [Online; accessed 31-March-2023].
[58]
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019. Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs. Proc. ACM Program. Lang., 3, POPL (2019), Article 59, jan, 30 pages. https://doi.org/10.1145/3290372
[59]
D. Volpano. 2000. Secure introduction of one-way functions. In Proceedings 13th IEEE Computer Security Foundations Workshop. CSFW-13. 246–254. https://doi.org/10.1109/CSFW.2000.856941
[60]
Dennis Volpano and Geoffrey Smith. 2000. Verifying secrets and relative secrecy. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 268–276. https://doi.org/10.1145/325694.325729
[61]
W3C Technical Architecture Group. 2021. Web HTTPS. https://www.w3.org/2001/tag/doc/web-https [Online; accessed 31-March-2023].
[62]
Lucas Waye, Pablo Buiras, Owen Arden, Alejandro Russo, and Stephen Chong. 2017. Cryptographically secure information flow control on key-value stores. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. 1893–1907. https://doi.org/10.1145/3133956.3134036
Index Terms
- Verifying Indistinguishability of Privacy-Preserving Protocols
Recommendations
Privacy-Preserving OpenID Connect
ASIA CCS '20: Proceedings of the 15th ACM Asia Conference on Computer and Communications SecurityOpenID Connect is the most widely used Internet protocol for delegated authentication today. It provides single sign-on functionality for users who use their account with an identity provider to authenticate to different services, called relying ...
Specifying Privacy-Preserving Protocols in Typed MSR
Privacy-preserving protocols, such as electronic cash, electronic voting and selective disclosure protocols, use special message constructors that are not widely used in other types of protocols (for example, in authentication protocols). These message ...
Fair and privacy-preserving multi-party protocols for reconciling ordered input sets
ISC'10: Proceedings of the 13th international conference on Information securityIn this paper, we introduce the first protocols for multiparty, privacy-preserving, fair reconciliation of ordered sets. Our contributions are twofold. First, we show that it is possible to extend the round-based construction for fair, two-party privacy-...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
2250 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 October 2023
Published in PACMPL Volume 7, Issue OOPSLA2
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 341Total Downloads
- Downloads (Last 12 months)282
- Downloads (Last 6 weeks)64
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in