Paper 2023/1390

Comparse: Provably Secure Formats for Cryptographic Protocols

Théophile Wallez, Inria Paris
Jonathan Protzenko, Microsoft Research
Karthikeyan Bhargavan, Inria Paris, Cryspen
Abstract

Data formats used for cryptographic inputs have historically been the source of many attacks on cryptographic protocols, but their security guarantees remain poorly studied. One reason is that, due to their low-level nature, formats often fall outside of the security model. Another reason is that studying all of the uses of all of the formats within one protocol is too difficult to do by hand, and requires a comprehensive, automated framework. We propose a new framework, “Comparse”, that specifically tackles the security analysis of data formats in cryptographic protocols. Comparse forces the protocol analyst to systematically think about data formats, formalize them precisely, and show that they enjoy strong enough properties to guarantee the security of the protocol. Our methodology is developed in three steps. First, we introduce a high-level cryptographic API that lifts the traditional game-based cryptographic assumptions over bitstrings to work over high-level messages, using formats. This allows us to derive the conditions that secure formats must obey in order for their usage to be secure. Second, equipped with these security criteria, we implement a framework for specifying and verifying secure formats in the F* proof assistant. Our approach is based on format combinators, which enable compositional and modular proofs. In many cases, we relieve the user of having to write those combinators by hand, using compile-time term synthesis via Meta-F*. Finally, we show that our F* implementation can replace the symbolic notion of message formats previously implemented in the DY* protocol analysis framework. Our newer, bit-level precise accounting of formats closes the modeling gap, and allows DY* to reason about concrete messages and identify protocol flaws that it was previously oblivious to. We evaluate Comparse over several classic and real-world protocols. Our largest case studies use Comparse to formalize and provide security proofs for the formats used in TLS 1.3, as well as upcoming protocols like MLS and Compact TLS 1.3 (cTLS), providing confidence and feedback in the design of these protocols.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. ACM CCS
DOI
10.1145/3576915.3623201
Keywords
cryptographic protocolsformal verificationsecure formatsparser combinatorscross-protocol attacksTLSMLS
Contact author(s)
theophile wallez @ inria fr
protz @ microsoft com
karthikeyan bhargavan @ inria fr
History
2023-09-18: approved
2023-09-17: received
See all versions
Short URL
https://ia.cr/2023/1390
License
Creative Commons Attribution-NonCommercial-NoDerivs
CC BY-NC-ND

BibTeX

@misc{cryptoeprint:2023/1390,
      author = {Théophile Wallez and Jonathan Protzenko and Karthikeyan Bhargavan},
      title = {Comparse: Provably Secure Formats for Cryptographic Protocols},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/1390},
      year = {2023},
      doi = {10.1145/3576915.3623201},
      url = {https://eprint.iacr.org/2023/1390}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.