1. SoK: Computer-Aided Cryptography
- Author
-
Gilles Barthe, Karthikeyan Bhargavan, Bryan Parno, Bruno Blanchet, Kevin Liao, Manuel Barbosa, Cas Cremers, Institute for Systems and Computer Engineering, Technology and Science [Porto] (INESC TEC), Faculdade de Ciências da Universidade do Porto (FCUP), Universidade do Porto = University of Porto, Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Institute IMDEA Software [Madrid], Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Helmholtz Center for Information Security [Saarbrücken] (CISPA), Massachusetts Institute of Technology (MIT), Carnegie Mellon University [Pittsburgh] (CMU), Work by Manuel Barbosa was supported by National Funds through the Portuguese Foundation for Science and Technology (FCT) under project PTDC/CCI-INF/31698/2017. Work by Gilles Barthe was supported by the Office of Naval Research (ONR) under project N00014-15-1-2750. Work by Karthik Bhargavan was supported by the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme (grant agreement no.683032 - CIRCUS). Work by Bruno Blanchet was supported by the French National Research Agency (ANR) under project TECAP (decision no. ANR-17-CE39-0004-03). Work by Kevin Liao was supported by the National Science Foundation (NSF) through a Graduate Research Fellowship. Work by Bryan Parno was supported by a gift from Bosch, a fellowship from the Alfred P. Sloan Foundation, the NSF under Grant No.1801369, and the Department of the Navy, Office of Naval Research under Grant No. N00014-18-1-2892., ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), European Project: 683032,H2020 ERC,ERC-2015-CoG,CIRCUS(2016), Universidade do Porto, and Programming securely with cryptography (PROSECCO )
- Subjects
Focus (computing) ,Correctness ,Standardization ,Scope (project management) ,business.industry ,Computer science ,020207 software engineering ,Cryptography ,02 engineering and technology ,Data science ,[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] ,Taxonomy (general) ,0202 electrical engineering, electronic engineering, information engineering ,Computer-aided ,020201 artificial intelligence & image processing ,business - Abstract
International audience; Computer-aided cryptography is an active area of research that develops and applies formal, machine-checkable approaches to the design, analysis, and implementation of cryptography. We present a cross-cutting systematization of the computer-aided cryptography literature, focusing on three main areas: (i) design-level security (both symbolic security and computational security), (ii) functional correctness and efficiency, and (iii) implementation-level security (with a focus on digital side-channel resistance). In each area, we first clarify the role of computer-aided cryptography-how it can help and what the caveats are-in addressing current challenges. We next present a taxonomy of state-of-the-art tools, comparing their accuracy, scope, trustworthiness, and usability. Then, we highlight their main achievements, trade-offs, and research challenges. After covering the three main areas, we present two case studies. First, we study efforts in combining tools focused on different areas to consolidate the guarantees they can provide. Second, we distill the lessons learned from the computer-aided cryptography community's involvement in the TLS 1.3 standardization effort. Finally, we conclude with recommendations to paper authors, tool developers, and standardization bodies moving forward.
- Published
- 2021