Welcome to the resource topic for 2023/473
Title:
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System
Authors: Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno
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.
ePrint: https://eprint.iacr.org/2023/473
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .