research-article

A Type System for Privacy Properties

Authors:

Véronique Cortier,

Joseph Lallemand,

Matteo MaffeiAuthors Info & Claims

CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

Pages 409 - 423

https://doi.org/10.1145/3133956.3133998

Published: 30 October 2017 Publication History

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.

Supplemental Material

MP4 File

Download
2417.61 MB

References

[1]

Martín Abadi. 2000. Security Protocols and their Properties. In Foundations of Secure Computation, F Bauer and R Steinbriiggen (Eds.). NATO Science Series, Vol. for the 20th International Summer School on Foundations of Secure Computation held in Marktoberdorf Germany. IOS Press, 39--60.

[2]

Martín Abadi and Cédric Fournet. 2001. Mobile Values, New Names, and Secure Communication. In 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01). ACM, 104--115.

Digital Library

[3]

Martín Abadi and Cédric Fournet. 2004. Private Authentication. Theoretical Computer Science 322, 3 (2004), 427--476.

Digital Library

[4]

Martín Abadi and Phillip Rogaway. 2000. Reconciling Two Views of Cryptography. In International Conference on Theoretical Computer Science (IFIP TCS2000). Springer, 3--22.

[5]

Ben Adida. 2008. Helios: Web-based Open-Audit Voting. In 17th USENIX Security symposium (SS'08). USENIX Association, 335--348.

[6]

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017. Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels. In 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017. ACM, 362--375.

Digital Library

[7]

Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. 2009. Untraceability in the Applied Pi Calculus. In 1st International Workshop on RFID Security and mCryptography. IEEE, 1--6.

[8]

Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. 2010. Analysing Unlinkability and Anonymity Using the Applied Pi Calculus. In 2nd IEEE Computer Security Foundations Symposium (CSF'10). IEEE Computer Society Press, 107--121.

Digital Library

[9]

Myrto Arapinis, Véronique Cortier, and Steve Kremer. 2016. When Are Three Voters Enough for Privacy Properties?. In 21st European Symposium on Research in Computer Security (ESORICS'16) (Lecture Notes in Computer Science). Springer, Heraklion, Crete, 241--260.

[10]

Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. 2005. The AVISPA Tool for the automated validation of internet security protocols and applications. In 17th International Conference on Computer Aided Verification, CAV'2005 (Lecture Notes in Computer Science), Vol. 3576. Springer, Edinburgh, Scotland, 281--285.

Digital Library

[11]

Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2008. Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus. In 21st IEEE Computer Security Foundations Symposium (CSF '08). IEEE Computer Society, Washington, DC, USA, 195--209.

Digital Library

[12]

Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2014. Union, Intersection and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations. Journal of Computer Security 22, 2 (March 2014), 301--353.

[13]

David Baelde, Stéphanie Delaune, and Lucca Hirschi. 2015. Partial Order Reduction for Security Protocols. In 26th International Conference on Concurrency Theory (CONCUR'15) (LIPIcs), Vol. 42. Leibniz-Zentrum für Informatik, 497--510.

[14]

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Béguelin. 2014. Probabilistic Relational Verification for Cryptographic Implementations. In 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, 193--206.

Digital Library

[15]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal certification of code-based cryptographic proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM, 90--101.

Digital Library

[16]

David Basin, Jannik Dreier, and Ralf Sasse. 2015. Automated Symbolic Proofs of Observational Equivalence. In 22nd ACM SIGSAC Conference on Computer and Communications Security (ACM CCS 2015). ACM, ACM, 1144--1155.

Digital Library

[17]

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2011. Refinement Types for Secure Implementations. ACM Transactions on Programming Languages and Systems 33, 2 (2011), 8:1--8:45.

Digital Library

[18]

Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '04). ACM, New York, NY, USA, 14--25.

Digital Library

[19]

Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14). IEEE Computer Society, Cape Breton, Nova Scotia, Canada, 82--96.

[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.

Digital Library

[21]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. 2008. Automated Verification of Selected Equivalences for Security Protocols. Journal of Logic and Algebraic Programming 75, 1 (Feb.-March 2008), 3--51.

[22]

Michele Boreale, Rocco de Nicola, and Rosario Pugliese. 2002. Proof Techniques for Cryptographic Processes. SIAM J. Comput. 31, 3 (2002), 947--986.

Digital Library

[23]

Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2011. Resource-Aware Authorization Policies for Statically Typed Cryptographic Protocols. In 24th IEEE Computer Security Foundations Symposium (CSF '11). IEEE Computer Society, Washington, DC, USA, 83--98.

Digital Library

[24]

Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2013. Logical Foundations of Secure Resource Management in Protocol Implementations. In 2nd International Conference on Principles of Security and Trust (POST 2013). Springer Berlin Heidelberg, Berlin, Heidelberg, 105--125.

Digital Library

[25]

Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2015. Affine Refinement Types for Secure Distributed Programming. ACM Transactions on Programming Languages and Systems 37, 4, Article 11 (Aug. 2015), 66 pages.

Digital Library

[26]

Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2004. Authenticity by Tagging and Typing. In 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE '04). ACM, New York, NY, USA, 1--12.

Digital Library

[27]

Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2005. Analysis of Typed Analyses of Authentication Protocols. In 18th IEEE Workshop on Computer Security Foundations (CSFW '05). IEEE Computer Society, Washington, DC, USA, 112--125.

Digital Library

[28]

Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2007. Dynamic Types for Authentication. Journal of Computer Security 15, 6 (Dec. 2007), 563--617.

[29]

Ştefan Ciobâcă, Dorel Lucanu, Vlad Rusu, and Grigore Rosu. 2016. A language-independent proof system for full program equivalence. Formal Asp. Comput. 28, 3 (2016), 469--497.

Digital Library

[30]

Rohit Chadha, Stefan >Ştefan Ciobâcă, and Steve Kremer. 2012. Automated Verification of Equivalence Properties of Cryptographic Protocols. In Programming Languages and Systems -- 21th European Symposium on Programming (ESOP'12) (Lecture Notes in Computer Science), Vol. 7211. Springer, Tallinn, Estonia, 108--127.

[31]

Vincent Cheval. 2014. APTE: an Algorithm for Proving Trace Equivalence. In 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14) (Lecture Notes in Computer Science), Vol. 8413. Springer, Grenoble, France, 587--592.

[32]

Vincent Cheval, Véronique Cortier, and Antoine Plet. 2013. Lengths May Break Privacy -- or How to Check for Equivalences With Length. In 25th International Conference on Computer Aided Verification (CAV'13) (Lecture Notes in Computer Science), Vol. 8043. Springer, St Petersburg, Russia, 708--723.

[33]

John Clark and Jeremy Jacob. 1997. A Survey of Authentication Protocol Literature: Version 1.0. (1997).

[34]

Hubert Comon-Lundh and Véronique Cortier. 2008. Computational Soundness of Observational Equivalence. In 15th ACM Conference on Computer and Communications Security (CCS'08). ACM Press, Alexandria, Virginia, USA, 109--118.

Digital Library

[35]

Véronique Cortier, Stéphanie Delaune, and Antoine Dallon. 2017. SAT-Equiv: an efficient tool for equivalence properties. In 30th IEEE Computer Security Foundations Symposium (CSF'17). IEEE Computer Society Press.

[36]

Véronique Cortier, Fabienne Eigner, Steve Kremer, Matteo Maffei, and Cyrille Wiedling. 2015. Type-Based Verification of Electronic Voting Protocols. In 4th International Conference on Principles of Security and Trust - Volume 9036. Springer-Verlag New York, Inc., New York, NY, USA, 303--323.

Digital Library

[37]

Veronique Cortier, Alicia Filipiak, Said Gharout, and Jacques Traore. 2017. Designing and Proving an EMV-compliant Payment Protocol for Mobile Devices. In 2nd IEEE European Symposium on Security and Privacy (EuroS&P'17). IEEE Computer Society, 467--480.

[38]

Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. 2017. A Type System for Privacy Properties (Technical Report). arXiv:1708.08340. (Aug. 2017). https://arxiv.org/abs/1708.08340

Digital Library

[39]

Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. 2017. TypeEQ. Source Code. (Aug. 2017). https://secpriv.tuwien.ac.at/tools/typeeq

[40]

Véronique Cortier, Michaël Rusinowitch, and Eugen Zălinescu. 2006. Relating Two Standard Notions of Secrecy. Springer Berlin Heidelberg, 303--318.

[41]

Véronique Cortier and Ben Smyth. 2011. Attacking and Fixing Helios: An Analysis of Ballot Secrecy. In 24th IEEE Computer Security Foundations Symposium (CSF'11). IEEE Computer Society Press, 297--311.

Digital Library

[42]

Cas J. F. Cremers. 2008. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, USA (Lecture Notes in Computer Science), Vol. 5123/2008. Springer, 414--418.

[43]

Jeremy Dawson and Alwen Tiu. 2010. Automating Open Bisimulation Checking for the Spi Calculus. In 23rd IEEE Computer Security Foundations Symposium (CSF 2010). IEEE Computer Society, 307--321.

[44]

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. 2009. Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security 17, 4 (2009), 435--487.

Digital Library

[45]

Fabienne Eigner and Matteo Maffei. 2013. Differential Privacy by Typing in Security Protocols. In 26th IEEE Computer Security Foundations Symposium (CSF'13). IEEE Computer Society, Washington, DC, USA, 272--286.

Digital Library

[46]

Riccardo Focardi and Matteo Maffei. 2011. Types for Security Protocols. In Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, Vol. 5. IOS Press, Chapter 7, 143--181.

[47]

Andrew D. Gordon and Alan Jeffrey. 2003. Authenticity by Typing for Security Protocols. Journal of Computer Security 11, 4 (July 2003), 451--519.

[48]

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. 2017. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations. arXiv:1703.00055. (July 2017). https://arxiv.org/abs/1703.00055

[49]

Gavin Lowe. 1996. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96) (Lecture Notes in Computer Science), Vol. 1055. Springer-Verlag, 147--166.

[50]

Dorel Lucanu and Vlad Rusu. 2015. Program equivalence by circular reasoning. Formal Asp. Comput. 27, 4 (2015), 701--726.

Digital Library

[51]

Matteo Maffei, Kim Pecina, and Manuel Reinert. 2013. Security and Privacy by Declarative Design. In 26th IEEE Computer Security Foundations Symposium (CSF'13). IEEE Computer Society, Washington, DC, USA, 81--96.

Digital Library

[52]

Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification, 25th International Conference, CAV 2013, Princeton, USA (Lecture Notes in Computer Science), Vol. 8044. Springer, 696--701.

Digital Library

[53]

Peter Roenne. 2016. Private communication. (2016).

[54]

Sonia Santiago, Santiago Escobar, Catherine A. Meadows, and José Meseguer. 2014. A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA. In STM 2014 (Lecture Notes in Computer Science). IEEE Computer Society, 162--177.

[55]

Benedikt Schmidt, Simon Meier, Cas J. F. Cremers, and David A. Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 24th IEEE Computer Security Foundations Symposium (CSF'12). IEEE Computer Society, 78--94.

Digital Library

[56]

Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare Logic for Verifying k-Safety Properties. In 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016. ACM, 57--69.

Digital Library

[57]

Hongseok Yang. 2007. Relational Separation Logic. Theorertical Compututer Science 375, 1--3 (2007), 308--334.

Digital Library

Cited By

Sotiropoulos TChaliasos SSu Z(2024)API-Driven Program Synthesis for Testing Static Typing ImplementationsProceedings of the ACM on Programming Languages10.1145/36329048:POPL(1850-1881)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632904
Zakhour GWeisenburger PSalvaneschi G(2023)Type-Checking CRDT ConvergenceProceedings of the ACM on Programming Languages10.1145/35912767:PLDI(1365-1388)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591276
Agrawal AFirst EKaufman ZReichel TZhang SZhou TSanchez-Stern ARinger TBrun YGrundy J(2023)Proofster: Automated Formal VerificationProceedings of the 45th International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion58688.2023.00018(26-30)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE-Companion58688.2023.00018
Show More Cited By

Index Terms

A Type System for Privacy Properties
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models
    2. Logic and verification

Recommendations

Privacy and identity management for everyone
DIM '05: Proceedings of the 2005 workshop on Digital identity management
The shift from a paper-based to an electronic-based society has dramatically reduced the cost of collecting, storing and processing individuals' personal information. As a result, it is becoming more common for businesses to "profile" individuals in ...
Privacy-Friendly Authentication in RFID Systems: On Sublinear Protocols Based on Symmetric-Key Cryptography

The recent advent of ubiquitous technologies has raised an important concern for citizens: the need to protect their privacy. So far, this wish was not heard of industrials, but national and international regulation authorities, as the European ...
SIPPA-2.0 - Secure information processing with privacy assurance (version 2.0)
PST '12: Proceedings of the 2012 Tenth Annual International Conference on Privacy, Security and Trust (PST)

We present a two-party secure information processing protocol referred to as SIPPA-2.0 - targeted towards privacy preserving biometric data comparison and reconstruction. The original intention of SIPPA as reported previously is to enable private data ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

October 2017

2682 pages

ISBN:9781450349468

DOI:10.1145/3133956

General Chair:
Bhavani Thuraisingham
The University of Texas at Dallas, USA
,
Program Chairs:
David Evans
University of Virginia
,
Tal Malkin
Columbia University
,
Dongyan Xu
Purdue University

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 October 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council (ERC)

Conference

CCS '17

Sponsor:

SIGSAC

CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security

October 30 - November 3, 2017

Texas, Dallas, USA

Acceptance Rates

CCS '17 Paper Acceptance Rate 151 of 836 submissions, 18%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '24

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 14 - 18, 2024

Salt Lake City , UT , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
415
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sotiropoulos TChaliasos SSu Z(2024)API-Driven Program Synthesis for Testing Static Typing ImplementationsProceedings of the ACM on Programming Languages10.1145/36329048:POPL(1850-1881)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632904
Zakhour GWeisenburger PSalvaneschi G(2023)Type-Checking CRDT ConvergenceProceedings of the ACM on Programming Languages10.1145/35912767:PLDI(1365-1388)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591276
Agrawal AFirst EKaufman ZReichel TZhang SZhou TSanchez-Stern ARinger TBrun YGrundy J(2023)Proofster: Automated Formal VerificationProceedings of the 45th International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion58688.2023.00018(26-30)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE-Companion58688.2023.00018
Cheval VRakotonirina I(2023)Indistinguishability Beyond Diff-Equivalence in ProVerif2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00036(184-199)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00036
Baloglu SBursuc SMauw SPang J(2023)Election Verifiability in Receipt-Free Voting Protocols2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00005(59-74)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00005
Gondron SMödersheim SViganò L(2022)Privacy as Reachability2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919668(130-146)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919668
Mödersheim S(2022)Rewriting PrivacyRewriting Logic and Its Applications10.1007/978-3-031-12441-9_2(22-41)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-031-12441-9_2
Cheval VKremer SRakotonirina I(2020)The Hitchhiker’s Guide to Decidability and Complexity of Equivalence Properties in Security ProtocolsLogic, Language, and Security10.1007/978-3-030-62077-6_10(127-145)Online publication date: 28-Oct-2020
https://doi.org/10.1007/978-3-030-62077-6_10
Barthe GEilers RGeorgiou PGleiss BKovacs LMaffei M(2019)Verifying Relational Properties using Trace Logic2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894277(170-178)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894277
Mödersheim SViganò L(2019)Alpha-Beta PrivacyACM Transactions on Privacy and Security10.1145/328925522:1(1-35)Online publication date: 22-Jan-2019
https://dl.acm.org/doi/10.1145/3289255
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents