More Web Proxy on the site http://driver.im/

research-article

ILC: a calculus for composable, computational cryptography

Authors:

Matthew A. Hammer,

Andrew MillerAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 640 - 654

https://doi.org/10.1145/3314221.3314607

Published: 08 June 2019 Publication History

Abstract

The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness.

In this paper, we lay the groundwork for building a concrete, executable implementation of the UC framework. Our main contribution is a process calculus, dubbed the Interactive Lambda Calculus (ILC). ILC faithfully captures the computational model underlying UC—interactive Turing machines (ITMs)—by adapting ITMs to a subset of the π-calculus through an affine typing discipline. In other words, well-typed ILC programs are expressible as ITMs. In turn, ILC’s strong confluence property enables reasoning about cryptographic security reductions. We use ILC to develop a simplified implementation of UC called SaUCy.

Supplementary Material

WEBM File (p640-liao.webm)

Download
80.26 MB

MP4 File (3314221.3314607.mp4)

Video Presentation

Download
46.98 MB

References

[1]

Martín Abadi and Cédric Fournet. 2001. Mobile values, new names, and secure communication. In ACM Sigplan Notices, Vol. 36. ACM, 104–115.

Digital Library

[2]

Martın Abadi and Andrew D Gordon. 1999. A calculus for cryptographic protocols: The spi calculus. Information and computation 148, 1 (1999), 1–70.

Digital Library

[3]

Michael Backes, Birgit Pfitzmann, and Michael Waidner. 2007. The reactive simulatability (RSIM) framework for asynchronous systems. Information and Computation 205, 12 (2007), 1685–1720.

Digital Library

[4]

G. Barthe, B. Grégoire, S. Heraud, and S. Béguelin. 2011. Computeraided security proofs for the working cryptographer. In Proceedings of the International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT).

Digital Library

[5]

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. ACM SIG-PLAN Notices 44, 1 (2009), 90–101.

Digital Library

[6]

Martin Berger, Kohei Honda, and Nobuko Yoshida. 2001. Sequentiality and the π -calculus. In International Conference on Typed Lambda Calculi and Applications. Springer, 29–45.

Digital Library

[7]

Bruno Blanchet. 2007. CryptoVerif: Computationally sound mechanized prover for cryptographic protocols. In Dagstuhl seminar “Formal Protocol Verification Applied. 117.

[8]

Bruno Blanchet. 2012. Security protocol verification: Symbolic and computational models. In Proceedings of the First international conference on Principles of Security and Trust. Springer-Verlag, 3–29.

Digital Library

[9]

Bruno Blanchet, V Cheval, X Allamigeon, and B Smyth. 2010. Proverif: Cryptographic protocol verifier in the formal model. URL http://prosecco. gforge. inria. fr/personal/bblanche/proverif (2010).

[10]

Florian Böhl and Dominique Unruh. 2016. Symbolic universal composability. Journal of Computer Security 24, 1 (2016), 1–38.

[11]

Gilles Brassard, David Chaum, and Claude Crépeau. 1988. Minimum disclosure proofs of knowledge. J. Comput. System Sci. 37, 2 (1988), 156–189.

Digital Library

[12]

Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2015. Affine refinement types for secure distributed programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 37, 4 (2015), 11.

Digital Library

[13]

Jan Camenisch, Robert R Enderlein, Stephan Krenn, Ralf Küsters, and Daniel Rausch. 2016. Universal composition with responsive environments. In International Conference on the Theory and Application of Cryptology and Information Security. Springer, 807–840.

Digital Library

[14]

R. Canetti. 2001. Universally composable security: A new paradigm for cryptographic protocols. In Proceedings of the Symposium on Foundations of Computer Science (FOCS).

Digital Library

[15]

Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, and Roberto Segala. 2008. Analyzing security protocols using time-bounded task-PIOAs. Discrete Event Dynamic Systems 18, 1 (2008), 111–159.

Digital Library

[16]

Ran Canetti, Asaf Cohen, and Yehuda Lindell. 2015. A simpler variant of universally composable security for standard multiparty computation. In Annual Cryptology Conference. Springer, 3–22.

Digital Library

[17]

Ran Canetti and Marc Fischlin. 2001. Universally composable commitments. In Annual International Cryptology Conference. Springer, 19–40.

Digital Library

[18]

Ran Canetti and Tal Rabin. 2003. Universal composition with joint state. In Annual International Cryptology Conference. Springer, 265–281.

[19]

Stefan Dziembowski, Sebastian Faust, and Kristina Hostáková. 2018. General State Channel Networks. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. ACM, 949–966.

Digital Library

[20]

Santiago Escobar, Catherine Meadows, and José Meseguer. 2009. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V. Springer, 1–50.

Digital Library

[21]

Simon Fowler, Sam Lindley, J Garrett Morris, and Sára Decova. 2018. Session Types without Tiers. (2018).

[22]

Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to play any mental game. In Proceedings of the nineteenth annual ACM symposium on Theory of computing. ACM, 218–229.

Digital Library

[23]

Dennis Hofheinz and Victor Shoup. 2015. GNUC: A new universal composability framework. Journal of Cryptology 28, 3 (2015), 423–508.

Digital Library

[24]

Dennis Hofheinz, Dominique Unruh, and Jörn Müller-Quade. 2013. Polynomial runtime and composability. Journal of Cryptology 26, 3 (2013), 375–441.

Digital Library

[25]

Jonathan Katz. 2007. Universally composable multi-party computation using tamper-proof hardware. In Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 115–128.

Digital Library

[26]

Naoki Kobayashi, Benjamin C Pierce, and David N Turner. 1999. Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems (TOPLAS) 21, 5 (1999), 914–947.

Digital Library

[27]

Ahmed Kosba, Andrew Miller, Elaine Shi, Zikai Wen, and Charalampos Papamanthou. 2016. Hawk: The blockchain model of cryptography and privacy-preserving smart contracts. In 2016 IEEE symposium on security and privacy (SP). IEEE, 839–858.

[28]

Ralf Kusters. 2006. Simulation-based security with inexhaustible interactive turing machines. In Computer Security Foundations Workshop, 2006. 19th IEEE. IEEE, 12–pp.

Digital Library

[29]

Peeter Laud. 2005. Secrecy types for a simulatable cryptographic library. In Proceedings of the 12th ACM conference on Computer and communications security. ACM, 26–35.

Digital Library

[30]

Jeffrey R Lewis and Brad Martin. 2003. Cryptol: High assurance, retargetable crypto development and validation. In Military Communications Conference, 2003. MILCOM’03. 2003 IEEE, Vol. 2. IEEE, 820–825.

Digital Library

[31]

Kevin Liao, Matthew A. Hammer, and Andrew Miller. 2019. ILC: A Calculus for Composable, Computational Cryptography (Extended Version). https://eprint.iacr.org/2019/402 . (2019).

[32]

Patrick Lincoln, John Mitchell, Mark Mitchell, and Andre Scedrov. 1998. A probabilistic poly-time framework for protocol analysis. In Proceedings of the 5th ACM conference on Computer and communications security. ACM, 112–121.

Digital Library

[33]

Yehuda Lindell. 2017. How to simulate it–a tutorial on the simulation proof technique. In Tutorials on the Foundations of Cryptography. Springer, 277–346.

[34]

Yehuda Lindell and Jonathan Katz. 2014. Introduction to modern cryptography. Chapman and Hall/CRC.

[35]

Paulo Mateus, J Mitchell, and Andre Scedrov. 2003. Composition of cryptographic protocols in a probabilistic polynomial-time process calculus. In International Conference on Concurrency Theory. Springer, 327–349.

[36]

Ueli Maurer. 2011. Constructive cryptography–a new paradigm for security definitions and proofs. In Theory of Security and Applications. Springer, 33–56.

Digital Library

[37]

Ueli Maurer and Renato Renner. 2011. Abstract cryptography. In In Innovations in Computer Science. Citeseer.

[38]

Catherine Meadows. 1996. The NRL protocol analyzer: An overview. The Journal of Logic Programming 26, 2 (1996), 113–131.

[39]

Andrew Miller, Iddo Bentov, Ranjit Kumaresan, and Patrick McCorry. 2017. Sprites: Payment channels that go faster than lightning. CoRR abs/1702.05812 (2017).

[40]

Robin Milner. 1999. Communicating and mobile systems: the pi calculus. Cambridge university press.

Digital Library

[41]

Birgit Pfitzmann and Michael Waidner. 2001. A model for asynchronous reactive systems and its application to secure message transmission. In Security and Privacy, 2001. S&P 2001. Proceedings. 2001 IEEE Symposium on. IEEE, 184–200.

Digital Library

[42]

N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, et al. 2016. Dependent types and multimonadic effects in F ∗ . In Proceedings of the Symposium on Principles of Programming Languages (POPL).

Digital Library

Cited By

Künnemann RPatrignani MCecchetti E(2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00024
Acay CGancher JRecto RMyers A(2024)Secure Synthesis of Distributed Cryptographic Applications2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00021(433-448)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00021
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Show More Cited By

Index Terms

ILC: a calculus for composable, computational cryptography
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models

Recommendations

A Universally Composable Group Key Exchange Protocol with Minimum Communication Effort
SCN '08: Proceedings of the 6th international conference on Security and Cryptography for Networks

The universal composability (UC) framework by Canetti [15] is a general-purpose framework for designing secure protocols. It ensures the security of UC-secure protocols under arbitrary compositions. As key exchange protocols (KEs) belong to the most ...
On the Limitations of Universally Composable Two-Party Computation Without Set-Up Assumptions

The recently proposed universally composable security framework for analyzing security of cryptographic protocols provides very strong security guarantees. In particular, a protocol proven secure in this framework is guaranteed to maintain its security ...
Universally composable three-party password-authenticated key exchange with contributiveness

Three-party password-authenticated key exchange 3PAKE allows two clients, each sharing a password with a trusted server, to establish a session key with the help of the server. It is a quite practical mechanism for establishing secure channels in a large ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Copyright © 2019 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 ACM 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
323
Total Downloads

Downloads (Last 12 months)31
Downloads (Last 6 weeks)3

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Künnemann RPatrignani MCecchetti E(2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00024
Acay CGancher JRecto RMyers A(2024)Secure Synthesis of Distributed Cryptographic Applications2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00021(433-448)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00021
Haselwarter PRivas EVan Muylder AWinterhalter TAbate CSidorenco NHriţcu CMaillard KSpitters B(2023)SSProve: A Foundational Framework for Modular Cryptographic Proofs in CoqACM Transactions on Programming Languages and Systems10.1145/359473545:3(1-61)Online publication date: 20-Jul-2023
https://dl.acm.org/doi/10.1145/3594735
Barbosa MBarthe GGrégoire BKoutsos AStrub P(2023)Mechanized Proofs of Adversarial Complexity and Application to Universal ComposabilityACM Transactions on Privacy and Security10.1145/358996226:3(1-34)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1145/3589962
Gancher JSojakova KFan XShi EMorrisett G(2023)A Core Calculus for Equational Proofs of Cryptographic ProtocolsProceedings of the ACM on Programming Languages10.1145/35712237:POPL(866-892)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571223
Broadbent AKarvonen M(2022)Categorical composable cryptographyFoundations of Software Science and Computation Structures10.1007/978-3-030-99253-8_9(161-183)Online publication date: 4-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99253-8_9
Barbosa MBarthe GGrégoire BKoutsos AStrub PKim YKim JVigna GShi E(2021)Mechanized Proofs of Adversarial Complexity and Application to Universal ComposabilityProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484548(2541-2563)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484548
Barbosa MBarthe GBhargavan KBlanchet BCremers CLiao KParno B(2021)SoK: Computer-Aided Cryptography2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00008(777-795)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00008
Abate CHaselwarter PRivas EMuylder AWinterhalter THriţcu CMaillard KSpitters B(2021)SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00048(1-15)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00048
Zhang Zde Amorim AJia LPăsăreanu C(2021)Learning Assumptions for Verifying Cryptographic Protocols CompositionallyFormal Aspects of Component Software10.1007/978-3-030-90636-8_1(3-23)Online publication date: 28-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-90636-8_1

View Options

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