Cryptology ePrint Archive: Report 2019/1393
SoK: Computer-Aided Cryptography
Manuel Barbosa and Gilles Barthe and Karthik Bhargavan and Bruno Blanchet and Cas Cremers and Kevin Liao and Bryan Parno
Abstract: 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 and scope of analysis, 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.
Category / Keywords: implementation / computer-aided cryptography, formal methods, verification, security analysis, implementation, side-channel resistance
Date: received 2 Dec 2019
Contact author: kliao6 at illinois edu
Available format(s): PDF | BibTeX Citation
Version: 20191204:081915 (All versions of this report)
Short URL: ia.cr/2019/1393
[ Cryptology ePrint archive ]