How to simulate it in Isabelle: towards formal proof for secure multi-party computation

DOI10.1007/978-3-319-66107-0_8zbMath1483.68486arXiv1805.12482OpenAlexW2748077663MaRDI QIDQ1687724

Peng Zhang

Publication date: 4 January 2018

Full work available at URL: https://arxiv.org/abs/1805.12482

zbMATH Keywords

cryptographyformal verificationoblivious transfersimulation-based proof

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Cryptography (94A60) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

CryptHOL: game-based proofs in higher-order logic ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Sharemind
• CryptHOL
• ObliVM
• ABY

Cites Work

• A proof of security of Yao's protocol for two-party computation
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Efficient Constant Round Multi-party Computation Combining BMR and SPDZ
• New directions in cryptography
• On the security of public key protocols
• How to Simulate It – A Tutorial on the Simulation Proof Technique
• Computer-Aided Security Proofs for the Working Cryptographer
• Formal certification of code-based cryptographic proofs
• Unnamed Item
• Unnamed Item

This page was built for publication: How to simulate it in Isabelle: towards formal proof for secure multi-party computation