3.2. CKA from DDH🔗

Definition3.2.1

Group: CKA from DDH. (3)

Group member previews

Preview

Definition 3.2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

\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

Lean code for Definition3.2.1●1 definition

inductive(2 constructors, 2 parameters)defined in SecureMessaging/CKA/FromDDH/Construction.lean

complete

inductive DDH.CKAState (F G : Type) : Type

inductive DDH.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

DDH.CKAState.sendReady {F G : Type} : G → DDH.CKAState F G

Holds the peer's current DH public value and is ready to send.

DDH.CKAState.recvReady {F G : Type} : F → DDH.CKAState F G

Holds the party's sampled scalar and is ready to receive.

Definition3.2.2

Group: CKA from DDH. (3)

Group member previews

Preview

Definition 3.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 3.2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

GitHub#8

\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

Lean code for Definition3.2.2●1 definition

defdefined in SecureMessaging/CKA/FromDDH/Construction.lean

complete

def DDH.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) (DDH.CKAState F G) G G F

def DDH.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)
    (DDH.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)

Group member previews

Preview

Definition 3.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

GitHub#9

\todo

\Pr[\,\textsf{correctnessExp} = \mathsf{true}\,] = 1

theorem correctness [DecidableEq G] (adv : CKACorrectnessAdversary G G) :
  Pr[= true | correctnessExp (ddhCKA F G gen) adv] = 1

Lean code for Theorem3.2.3●1 theorem

theoremdefined in SecureMessaging/CKA/FromDDH/Correctness.lean

complete

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 | (DDH.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 |
      (DDH.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)

Group member previews

Preview

Definition 3.2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

GitHub#10

\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)

Lean code for Theorem3.2.4●1 theorem

theoremdefined in SecureMessaging/CKA/FromDDH/Security.lean

complete

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 (DDH.CKAState F G) G G F) :
  (DDH.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
      (DDH.CKAState F G) G G F) :
  (DDH.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, ℬ)`