Paper 2023/473
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System
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
-
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},
note = {\url{https://eprint.iacr.org/2023/473}},
url = {https://eprint.iacr.org/2023/473}
}
