Modular verification of security protocol code by typing

DOI10.1145/1706299.1706350zbMath1312.68052OpenAlexW2152845220MaRDI QIDQ5255101

Karthikeyan Bhargavan, Andrew D. Gordon, Cédric Fournet

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706350

zbMATH Keywords

refinement typeF7

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Compositional System Security with Interface-Confined Adversaries ⋮ A tutorial-style introduction to \(\mathsf{DY}^{\star}\) ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Cryptographic Verification by Typing for a Sample Protocol Implementation

This page was built for publication: Modular verification of security protocol code by typing