Coin Tossing Protocol

This file formalizes a two-party coin tossing protocol over ZMod p and proves its output uniformity via an additive bijection argument.

Protocol

Two parties each sample a random element from ZMod p and output their sum. The result is uniformly distributed, because for any fixed a, the map b ↦ a + b is a bijection on ZMod p.

Main definitions

• coinTossReal — real protocol: sample two elements and output their sum
• coinTossIdeal — ideal functionality: sample one uniform element

Main results

• add_uniform_eq_uniform — adding a constant to a uniform sample is uniform
• coinToss_eq — real and ideal coin toss produce identical distributions

Additive bijection on ZMod p

noncomputable def CatCryptCore.Examples.CoinToss.addEquiv (p : ℕ) (a : ZMod p) : ZMod p ≃ ZMod p

Addition by a fixed element is a bijection on ZMod p.

Equations

• CatCryptCore.Examples.CoinToss.addEquiv p a = Equiv.addLeft a

instance CatCryptCore.Examples.CoinToss.instNeZeroNat_catCryptCore (p : ℕ) [hp : Fact (Nat.Prime p)] : NeZero p

Protocol Definitions

noncomputable def CatCryptCore.Examples.CoinToss.coinTossReal (p : ℕ) [hp : Fact (Nat.Prime p)] : Unit → CatCrypt.Core.SPComp (ZMod p)

Real coin toss: both parties sample, output the sum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCryptCore.Examples.CoinToss.coinTossIdeal (p : ℕ) [hp : Fact (Nat.Prime p)] : Unit → CatCrypt.Core.SPComp (ZMod p)

Ideal coin toss: sample a single uniform element.

Equations

• CatCryptCore.Examples.CoinToss.coinTossIdeal p x✝ = CatCrypt.Core.SPComp.sample (ZMod p)

Helper Lemmas

theorem CatCryptCore.Examples.CoinToss.add_uniform_eq_uniform (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ZMod p) (h : CatCrypt.Core.Heap) : (CatCrypt.Core.SPComp.sample (ZMod p)).bind (fun (b : ZMod p) => CatCrypt.Core.SPComp.pure (a + b)) h = CatCrypt.Core.SPComp.sample (ZMod p) h

Sampling uniformly and adding a constant gives the same distribution as sampling uniformly. This is the key step: a + b for uniform b is uniform.

Main Theorem

theorem CatCryptCore.Examples.CoinToss.inner_eq (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ZMod p) : ((CatCrypt.Core.SPComp.sample (ZMod p)).bind fun (b : ZMod p) => CatCrypt.Core.SPComp.pure (a + b)) = CatCrypt.Core.SPComp.sample (ZMod p)

The inner computation: sampling b and returning a + b equals just sampling.

theorem CatCryptCore.Examples.CoinToss.coinToss_eq (p : ℕ) [hp : Fact (Nat.Prime p)] : coinTossReal p = coinTossIdeal p

The real coin toss protocol is distributionally equivalent to the ideal functionality. Both produce a uniform element of ZMod p.