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

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

Peng Zhang

Publication date: 4 January 2018

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

zbMATH Keywords

cryptography; formal verification; oblivious transfer; simulation-based proof

Mathematics Subject Classification ID

68Q10: Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

94A60: Cryptography

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

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