3.2. CKA from DDH
Definition3.2.1
\todo
inductive CKAState (F G : Type) where
/-- Holds the peer's current DH public value and is ready to send. -/
| sendReady : G → CKAState F G
/-- Holds the party's sampled scalar and is ready to receive. -/
| recvReady : F → CKAState F G
deriving DecidableEq, Fintype, Repr
uses Definition 3.1.1
Lean code for Definition3.2.1●1 definition
Associated Lean declarations
-
CKAState[complete]
Associated Lean declarations
-
CKAState[complete]
-
inductivedefined in SecureMessaging/CKA/FromDDH/Construction.leancomplete
inductive CKAState (F G : Type) : Type
inductive CKAState (F G : Type) : Type
Phase-tagged CKA state for the DDH construction. `sendReady h` means the party holds the peer's current DH public value `h : G` and can produce the next epoch key by sampling a scalar. `recvReady x` means the party holds its previously sampled scalar `x : F` and can receive the next DH public value.
Constructors
CKAState.sendReady {F G : Type} : G → CKAState F G
Holds the peer's current DH public value and is ready to send.
CKAState.recvReady {F G : Type} : F → CKAState F G
Holds the party's sampled scalar and is ready to receive.
Definition3.2.2
Group: CKA from DDH. (3)
Statement uses 2
Used by 2
Associated Lean declarations
-
ddhCKA[complete]
\todo
def ddhCKA (F G : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F]
[AddCommGroup G] [Module F G] [SampleableType G]
(gen : G) : CKAScheme ProbComp (G × F) (CKAState F G) G G F where
initKeyGen := do
let x ← $ᵗ F
return (x • gen, x)
initA := fun (h, _) => return .sendReady h
initB := fun (_, x) => return .recvReady x
sendA := send gen
sendArleak := sendRleak gen
sendB := send gen
sendBrleak := sendRleak gen
recvA := recv
recvB := recv
uses Definition 3.1.1 · Definition 3.2.1 · github #8
Lean code for Definition3.2.2●1 definition
Associated Lean declarations
-
ddhCKA[complete]
Associated Lean declarations
-
ddhCKA[complete]
-
defdefined in SecureMessaging/CKA/FromDDH/Construction.leancomplete
def ddhCKA (F G : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] [AddCommGroup G] [Module F G] [SampleableType G] (gen : G) : CKAScheme ProbComp (G × F) (CKAState F G) G G F
def ddhCKA (F G : Type) [Field F] [Fintype F] [DecidableEq F] [SampleableType F] [AddCommGroup G] [Module F G] [SampleableType G] (gen : G) : CKAScheme ProbComp (G × F) (CKAState F G) G G F
CKA from DDH over a module `Module F G` with generator `gen : G`. - `initKeyGen`: `x₀ ← $ᵗ F`; return `(x₀ • gen, x₀)`. - `initA (h, x₀)`: store `h : G`. `initB (h, x₀)`: store `x₀ : F`. - `sendA(h: G)` and `sendB(h: G)`: defined as `send(h: G)` above. - `recvA(x: F, ρ: G)` and `recvB(x: F, ρ: G)` defined as `recv(x: F, ρ: G)` above.
Theorem3.2.3
Group: CKA from DDH. (3)
Statement uses 2
Associated Lean declarations
-
ddhCKA.correctness[complete]
\todo
\Pr[\,\textsf{correctnessExp} = \mathsf{true}\,] = 1
theorem correctness [DecidableEq G] (adv : CKACorrectnessAdversary G G) :
Pr[= true | correctnessExp (ddhCKA F G gen) adv] = 1
uses Definition 3.2.2 · Definition 3.1.3 · github #9
Lean code for Theorem3.2.3●1 theorem
Associated Lean declarations
-
ddhCKA.correctness[complete]
Associated Lean declarations
-
ddhCKA.correctness[complete]
-
theoremdefined in SecureMessaging/CKA/FromDDH/Correctness.leancomplete
theorem ddhCKA.correctness {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType G] {gen : G} [DecidableEq G] (adv : CKAScheme.CKACorrectnessAdversary G G) : Pr[= true | (ddhCKA F G gen).correctnessExp adv] = 1
theorem ddhCKA.correctness {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType G] {gen : G} [DecidableEq G] (adv : CKAScheme.CKACorrectnessAdversary G G) : Pr[= true | (ddhCKA F G gen).correctnessExp adv] = 1
**DDH-CKA correctness**: for any adversary `𝒜` with access to send/receive oracles, `Pr[= true | Expᶜᵒʳʳ(ddhCKA, 𝒜)] = 1`. The experiment `exp := correctnessExp (ddhCKA F G gen) adv : ProbComp Bool` has three mutually exclusive outcomes summing to `1`: `Pr[= true | exp] + Pr[= false | exp] + Pr[⊥ | exp] = 1`. So `Pr[= true | exp] = 1` reduces to: * `nofail` — `Pr[⊥ | exp] = 0` (never fails); * `always_correct` — `Pr[= false | exp] = 0` (never returns `false`).
Theorem3.2.4
Group: CKA from DDH. (3)
Statement uses 2
Associated Lean declarations
-
ddhCKA.security[complete]
\todo
theorem security (gp : GameParams)
(hΔFS : gp.ΔFS = 1) (hΔPCS : gp.ΔPCS = 2)
(hg : Function.Bijective (· • gen : F → G))
(adversary : CKAAdversary (CKAState F G) G G F) :
ckaGuessAdvantage (ddhCKA F G gen) adversary gp ≤
ddhGuessAdvantage gen (securityReduction gp adversary)
uses Definition 3.2.2 · Definition 3.1.4 · github #10
Lean code for Theorem3.2.4●1 theorem
Associated Lean declarations
-
ddhCKA.security[complete]
Associated Lean declarations
-
ddhCKA.security[complete]
-
theoremdefined in SecureMessaging/CKA/FromDDH/Security.leancomplete
theorem ddhCKA.security {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType G] {gen : G} [DecidableEq G] (gp : CKAScheme.GameParams) (hΔFS : gp.ΔFS = 1) (hΔPCS : gp.ΔPCS = 2) (hg : Function.Bijective fun x ↦ x • gen) (adversary : CKAScheme.CKAAdversary (CKAState F G) G G F) : (ddhCKA F G gen).ckaGuessAdvantage adversary gp ≤ DiffieHellman.ddhGuessAdvantage gen (ddhCKA.securityReduction gp adversary)
theorem ddhCKA.security {F : Type} [Field F] [Fintype F] [DecidableEq F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G] [SampleableType G] {gen : G} [DecidableEq G] (gp : CKAScheme.GameParams) (hΔFS : gp.ΔFS = 1) (hΔPCS : gp.ΔPCS = 2) (hg : Function.Bijective fun x ↦ x • gen) (adversary : CKAScheme.CKAAdversary (CKAState F G) G G F) : (ddhCKA F G gen).ckaGuessAdvantage adversary gp ≤ DiffieHellman.ddhGuessAdvantage gen (ddhCKA.securityReduction gp adversary)
**Main theorem: security of CKA-from-DDH reduced to the DDH security assumption** For any CKA adversary `𝒜`, the CKA advantage of `𝒜` is bounded by the DDH advantage of the reduction `ℬ = securityReduction gp 𝒜`: `ckaGuessAdvantage(ddhCKA, 𝒜, gp) ≤ ddhGuessAdvantage(gen, ℬ)`