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

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

Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, Bryan Parno

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 …

automation bryan current descriptions eprint report flow framework information modular novel protocol protocols report security sound strength sydney system tools types verification