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

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

Cite

Cite as @gancher-2023-owl (helia, typst) · \cite{gancher-2023-owl} (LaTeX)

BibTeX

bibtex · 1 line

@inproceedings{gancher-2023-owl, title={Owl: Compositional Verification of Security Protocols via an Information-Flow Type System}, url={http://dx.doi.org/10.1109/sp46215.2023.10179477}, DOI={10.1109/sp46215.2023.10179477}, booktitle={2023 IEEE Symposium on Security and Privacy (SP)}, publisher={IEEE}, author={Gancher, Joshua and Gibson, Sydney and Singh, Pratap and Dharanikota, Samvid and Parno, Bryan}, year={2023}, month=May, pages={1130–1147} }

hayagriva YAML (typst)

yaml · 18 lines

gancher-2023-owl:
  type: article
  title: 'Owl: Compositional Verification of Security Protocols via an Information-Flow Type System'
  author:
  - Gancher, Joshua
  - Gibson, Sydney
  - Singh, Pratap
  - Dharanikota, Samvid
  - Parno, Bryan
  date: 2023-05
  page-range: 1130-1147
  url: http://dx.doi.org/10.1109/sp46215.2023.10179477
  serial-number:
    doi: 10.1109/sp46215.2023.10179477
  parent:
    type: proceedings
    title: 2023 IEEE Symposium on Security and Privacy (SP)
    publisher: IEEE

Download: gancher-2023-owl.bib · gancher-2023-owl.yml

Cites 69 works (0 here)

External (69)

Owl: Compositional verification of security protocols via an information-flow type system (full version, Cryptology ePrint Archive) (2023)
Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations (2022)
The Rust programming language (2022)
An Interactive Prover for Protocol Verification in the Computational Model (2021)
SoK: Computer-Aided Cryptography (2021)
$\textDY^ \star $: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (2021)
A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (2021)
Refinement Types: A Tutorial (2021)
EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security (2019)
A method for unbounded verification of privacy-type properties (2019)
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol (2019)
Composition Theorems for CryptoVerif and Application to TLS (2018)
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (2017)
Prf-odh: Relations, instantiations, and impossibility results (2017)
A Formal Security Analysis of the Signal Messaging Protocol (2017)
A Comprehensive Symbolic Analysis of TLS (2017)
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach (2017)
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (2016)
Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication (2016)
Dependent types and multi-monadic effects in F* (2016)
Imperfect Forward Secrecy (2015)
Flow-Limited Authorization (2015)
A Messy State of the Union: Taming the Composite State Machines of TLS (2015)
The Foundational Cryptography Framework (2015)
A Computationally Complete Symbolic Attacker for Equivalence Properties (2014)
EasyCrypt: A Tutorial (2014)
Proving the TLS Handshake Secure (As It Is) (2014)
Implementing TLS with Verified Cryptographic Security (2013)
The TAMARIN Prover for the Symbolic Analysis of Security Protocols (2013)
Towards Unconditional Soundness: Computationally Complete Symbolic Attacker (2012)
Security Protocol Verification: Symbolic and Computational Models (2012)
Computer-Aided Security Proofs for the Working Cryptographer (2011)
Modular code-based cryptographic verification (2011)
Information-flow types for homomorphic encryptions (2011)
Tag Size Does Matter: Attacks and Proofs for the TLS Record Protocol (2011)
Analysing Unlinkability and Anonymity Using the Applied Pi Calculus (2010)
Formal Verification of Privacy for RFID Systems (2010)
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems (2010)
Dafny: An Automatic Program Verifier for Functional Correctness (2010)
Plaintext Recovery Attacks against SSH (2009)
Formal certification of code-based cryptographic proofs (2009)
Defining strong privacy for RFID (2009)
Cryptographically-masked flows (2008)
A Computationally Sound Mechanized Prover for Security Protocols (2008)
Z3: An Efficient SMT Solver (2008)
On the computational soundness of cryptographically masked flows (2008)
The Secure Shell (SSH) Transport Layer Protocol (2006)
Another Look at "Provable Security" (2005)
Breaking and provably repairing the SSH authenticated encryption scheme (2004)
Strong Authentication for RFID Systems Using the AES Algorithm (2004)
The Security and Performance of the Galois/Counter Mode (GCM) of Operation (2004)
Privacy and security in library RFID (2004)
Language-based information-flow security (2003)
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption) (2002)
Key-Privacy in Public-Key Encryption (2001)
Universally Composable Commitments (2001)
The Order of Encryption and Authentication for Protecting Communications (or: How Secure Is SSL?) (2001)
Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm (2000)
The Kerberos Network Authentication Service (V5) (1993)
A logic of authentication (1989)
Efficient and timely mutual authentication (1987)
On the security of public key protocols (1983)
Timestamps in key distribution protocols (1981)
Using encryption for authentication in large networks of computers (1978)
New directions in cryptography (1976)
Implementing and proving the TLS 1.3 record layer
Owl code repository
A tutorial introduction to CryptHOL
The joy of cryptography