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

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.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. IEEE Symposium on Security and Privacy 2023
Security protocolstype systemscomputational security
Contact author(s)
jgancher @ andrew cmu edu
2023-04-24: last of 2 revisions
2023-03-31: received
See all versions
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.