Probabilistic relational verification for cryptographic implementations

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

zbMATH Keywords

probabilistic programmingprogram logics

Mathematics Subject Classification ID

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

• Coq
• z3
• EasyCrypt
• Ynot