Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
From MaRDI portal
Publication:2802495
DOI10.1007/978-3-662-49498-1_20zbMath1335.68033OpenAlexW2467040566MaRDI QIDQ2802495
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
Related Items
Program logic for higher-order probabilistic programs in Isabelle/HOL ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ 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 ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Verified analysis of random binary tree structures ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Equational Reasoning with Applicative Functors ⋮ Formalising Semantics for Expected Running Time of Probabilistic Programs ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- EasyCrypt
- A survey of symbolic methods in computational analysis of cryptographic systems
- The Max-Flow Min-Cut theorem for countable networks
- Proofs of randomized algorithms in Coq
- Bisimulation through probabilistic testing
- Isabelle/HOL. A proof assistant for higher-order logic
- Reconciling two views of cryptography (The computational soundness of formal encryption)
- Locales: a module system for mathematical theories
- Formalization of Shannon's theorems
- Truly Modular (Co)datatypes for Isabelle/HOL
- A General Framework for Probabilistic Characterizing Formulae
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- A Formalized Hierarchy of Probabilistic System Types
- Foundational extensible corecursion: a proof assistant perspective
- The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
- A public key cryptosystem and a signature scheme based on discrete logarithms
- Computer-Aided Security Proofs for the Working Cryptographer
- Formal certification of code-based cryptographic proofs
- Automatic Data Refinement
- Secure distributed programming with value-dependent types
- Probabilistic relational verification for cryptographic implementations
- A Formal Language for Cryptographic Pseudocode
