Probabilistic functions and cryptographic oracles in higher order logic
From MaRDI portal
Publication:2802495
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
- scientific article; zbMATH DE number 1231637 (Why is no real title available?)
- scientific article; zbMATH DE number 1927425 (Why is no real title available?)
- A Formal Language for Cryptographic Pseudocode
- A formalized hierarchy of probabilistic system types. Proof pearl
- A general framework for probabilistic characterizing formulae
- A public key cryptosystem and a signature scheme based on discrete logarithms
- A survey of symbolic methods in computational analysis of cryptographic systems
- Automatic Data Refinement
- Bisimulation through probabilistic testing
- Computer-Aided Security Proofs for the Working Cryptographer
- EasyCrypt
- Formal certification of code-based cryptographic proofs
- Formalization of Shannon's theorems
- Foundational extensible corecursion: a proof assistant perspective
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Locales: a module system for mathematical theories
- Probabilistic relational verification for cryptographic implementations
- Proofs of randomized algorithms in Coq
- Reconciling two views of cryptography (The computational soundness of formal encryption)
- Secure distributed programming with value-dependent types
- The Max-Flow Min-Cut theorem for countable networks
- The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
- Truly modular (co)datatypes for Isabelle/HOL
Cited in
(13)- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Effect polymorphism in higher-order logic (proof pearl)
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Equational Reasoning with Applicative Functors
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Formalising Semantics for Expected Running Time of Probabilistic Programs
- Comprehending Isabelle/HOL’s Consistency
- CryptHOL: game-based proofs in higher-order logic
- Effect polymorphism in higher-order logic (proof pearl)
- On the key dependent message security of the Fujisaki-Okamoto constructions
- Verified analysis of random binary tree structures
- Markov chains and Markov decision processes in Isabelle/HOL
Describes a project that uses
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)
