Formalising Oblivious Transfer in CryptHOL
summary
Formalisation proves semi-honest security of a classic oblivious transfer construction inside Isabelle/HOL using the CryptHOL/Crypto probabilistic-programming framework, showing perfect security for the sender and a reduction that bounds the receiver's advantage by twice the hardcore-predicate advantage. The work formalises extended trapdoor permutations, instantiates the proof for RSA, reuses a module to cut about half the proof, and notes polynomial-time reasoning and the malicious model remain unfinished and significantly harder.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:41What is multiparty computation
- 2:26Motivation
- 3:41Formal Methods
- 4:54Overview
- 5:49Semihonest Model
- 7:16Paper Definitions
- 8:45What do we fix
- 10:02Extended Trapdoor Permutations
- 11:21General Assumptions
- 12:17The Protocol
- 15:24The RSA Instantiation
- 16:00The RSA Proof
- 16:38What have we learnt
- 18:45Language
- 19:51Automation
- 21:05Questions
related talks
17mModular Verification of Probabilistic Constant-Time
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
14mNon-interference Preserving Optimising Compilation
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
30mFormalization of Differential Privacy in Isabelle/HOL
23mImpredicative Observational Equality
20mFSLH: Flexible Mechanized Speculative Load Hardening
26mSecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn