Paper 2023/473

Owl: Compositional Verification of Security Protocols via an Information-Flow Type System

Joshua Gancher, Carnegie Mellon University
Sydney Gibson, Carnegie Mellon University
Pratap Singh, Carnegie Mellon University
Samvid Dharanikota, Carnegie Mellon University
Bryan Parno, Carnegie Mellon University
Abstract

Computationally sound protocol verification tools promise to deliver full-strength cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity or automation. We propose a new approach based on a novel use of information flow and refinement types for sound cryptographic proofs. Our framework, Owl, allows type-based modular descriptions of security protocols, wherein disjoint subprotocols can be programmed and automatically proved secure separately. We give a formal security proof for Owl via a core language which supports standard symmetric and asymmetric primitives, Diffie-Hellman operations, and hashing via random oracles. We also implement a type checker for Owl along with a prototype extraction mechanism to Rust, and evaluate it on 14 case studies, including (simplified forms of) SSH key exchange and Kerberos.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. IEEE Symposium on Security and Privacy 2023
Keywords
Security protocolstype systemscomputational security
Contact author(s)
jgancher @ andrew cmu edu
History
2023-04-24: last of 2 revisions
2023-03-31: received
See all versions
Short URL
https://ia.cr/2023/473
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2023/473,
      author = {Joshua Gancher and Sydney Gibson and Pratap Singh and Samvid Dharanikota and Bryan Parno},
      title = {Owl: Compositional Verification of Security Protocols via an Information-Flow Type System},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/473},
      year = {2023},
      url = {https://eprint.iacr.org/2023/473}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.