International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News item: 01 April 2023

Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno
ePrint Report ePrint Report
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.
Expand

Additional news items may be found on the IACR news page.