Probabilistic functions and cryptographic oracles in higher order logic
From MaRDI portal
Publication:2802495
DOI10.1007/978-3-662-49498-1_20zbMATH Open1335.68033OpenAlexW2467040566MaRDI QIDQ2802495FDOQ2802495
Authors: Andreas Lochbihler 
Publication date: 26 April 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-49498-1_20
Recommendations
- Programming language techniques for cryptographic proofs
- A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
- Probabilistic relational verification for cryptographic implementations
- Formal certification of code-based cryptographic proofs
- Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic
Cites Work
- EasyCrypt
- Formal certification of code-based cryptographic proofs
- Automatic Data Refinement
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- A formalized hierarchy of probabilistic system types. Proof pearl
- Secure distributed programming with value-dependent types
- Isabelle/HOL. A proof assistant for higher-order logic
- A public key cryptosystem and a signature scheme based on discrete logarithms
- Bisimulation through probabilistic testing
- The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
- Locales: a module system for mathematical theories
- Computer-Aided Security Proofs for the Working Cryptographer
- Formalization of Shannon's theorems
- Title not available (Why is that?)
- Proofs of randomized algorithms in Coq
- A Formal Language for Cryptographic Pseudocode
- Reconciling two views of cryptography (The computational soundness of formal encryption)
- Probabilistic relational verification for cryptographic implementations
- A survey of symbolic methods in computational analysis of cryptographic systems
- The Max-Flow Min-Cut theorem for countable networks
- Title not available (Why is that?)
- Truly modular (co)datatypes for Isabelle/HOL
- Foundational extensible corecursion: a proof assistant perspective
- A general framework for probabilistic characterizing formulae
Cited In (13)
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- CryptHOL: game-based proofs in higher-order logic
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Verified analysis of random binary tree structures
- Equational Reasoning with Applicative Functors
- On the key dependent message security of the Fujisaki-Okamoto constructions
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Effect polymorphism in higher-order logic (proof pearl)
- Effect polymorphism in higher-order logic (proof pearl)
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- Markov chains and Markov decision processes in Isabelle/HOL
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Comprehending Isabelle/HOL’s Consistency
Uses Software
This page was built for publication: Probabilistic functions and cryptographic oracles in higher order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802495)
