Probabilistic Functions and Cryptographic Oracles in Higher Order Logic

DOI10.1007/978-3-662-49498-1_20zbMath1335.68033OpenAlexW2467040566MaRDI QIDQ2802495

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

Mathematics Subject Classification ID

Cryptography (94A60) Functional programming and lambda calculus (68N18)

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

• Coq
• Isabelle/HOL
• EasyCrypt
• Locales
• Autoref
• pGCL
• Transfer
• Lifting
• CoSP
• F*
• Zoo Probabilistic Systems

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