Probabilistic relational verification for cryptographic implementations
From MaRDI portal
Publication:5408416
DOI10.1145/2535838.2535847zbMath1284.68380OpenAlexW2170528665MaRDI QIDQ5408416
Gilles Barthe, Nikhil Swamy, Santiago Zanella Béguelin, Benjamin Grégoire, Pierre-Yves Strub, Cédric Fournet
Publication date: 10 April 2014
Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2535838.2535847
Cryptography (94A60) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Product programs and relational program logics ⋮ Translation certification for smart contracts ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ A higher-order language for Markov kernels and linear operators ⋮ Program synthesis for interactive-security systems ⋮ Toward automatic verification of quantum programs ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs ⋮ Relational cost analysis in a functional-imperative setting
Uses Software
