9.4. Opp-UniKEM-CKA🔗

Definition9.4.1

Group: Opp-UniKEM-CKA. (2)

Group member previews

Preview

Theorem 9.4.2

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 9.4.2

Loading preview

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

✓L∃∀N

Figure 16 of Auerbach et al. (2025). In the receive algorithms,

t is the epoch index of the receiver's state,
t' is the epoch index of the delivered message.

We make two corrections to these algorithms, marked with surrounding boxes:

\mathsf{Rec}\text{-}\A and \mathsf{Rec}\text{-}\B record received acknowledgements only if t=t';
\mathsf{Rec}\text{-}\B returns t'-1 rather than t-1.

\textsf{Initialisation}

\mathsf{CKA}\text{-}\mathsf{InitKeyGen}(): \quad I_{\mathsf{CKA}}\gets\bot;\quad \mathsf{return}\;I_{\mathsf{CKA}}

def initKeyGen : m Unit := pure ()

\begin{array}{l} \mathsf{CKA}\text{-}\InitA(\bot): \\ \quad(\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack) \gets(\bot,\bot,\bot,1,0,\emptyset,(\mathsf{false},\mathsf{false})); \\ \quad\stA\gets(\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack); \\ \quad\mathsf{return}\;\stA \end{array}

def initA (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (_ik : Unit) : m (StA onoff Sym) :=
  pure { dkA := none, ekA := none, ct0 := none, t := 1, ich := 0, lch := ∅,
         ack := { ekRec := false, ctRec := false } }

\begin{array}{l} \mathsf{CKA}\text{-}\InitB(\bot): \\ \quad(\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack) \gets(\bot,\bot,\bot,\bot,1,0,\emptyset,(\mathsf{false},\mathsf{false})); \\ \quad\stB\gets(\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack); \\ \quad\mathsf{return}\;\stB \end{array}

def initB (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (_ik : Unit) : m (StB onoff Sym) :=
  pure { ekA := none, ct0 := none, ct1 := none, stCt := none, t := 1, ich := 0,
         lch := ∅, ack := { ekRec := false, ctRec := false } }

\textsf{Vulnerable epochs}

\stA.\mathsf{vuln}: \quad \mathsf{return}\;\{t\}\;\mathsf{if}\;\dkA\ne\bot\;\mathsf{else}\;\emptyset

def vulnA (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (stA : StA onoff Sym) : Finset ℕ :=
  if stA.dkA.isSome then {stA.t} else ∅

\stB.\mathsf{vuln}: \quad \mathsf{return}\;\{t\}\;\mathsf{if}\;\stct\ne\bot\;\mathsf{else}\;\emptyset

def vulnB (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (stB : StB onoff Sym) : Finset ℕ :=
  if stB.stCt.isSome then {stB.t} else ∅

\mathsf{CKA}\text{-}\SendA(\stA)

\begin{array}{l} (\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack)\gets\stA, \chunk\gets\bot \\ \mathsf{if}\;\dkA=\bot\;\mathsf{then}\pcomment{\text{first message of epoch}} \\ \quad (\ekA,\dkA)\sample\KeyGen \\ \quad \ich\gets0 \\ \mathsf{if}\;\neg\ack.\ekrec\;\mathsf{then} \pcomment{\ekA\ \text{not acknowledged by }\B} \\ \quad \ich\gets\ich+1 \\ \quad \chunk\gets\mathsf{Encode}(\ekA,\ich) \\ \rho\gets(\chunk,\ack,t,\bot) \\ \stA\gets(\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack) \\ \mathsf{return}\;((\bot,\bot),\rho,t-1,\stA) \end{array}

def sendA (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
  (ecEk : ErasureCodePayload PK Sym) (stA : StA onoff Sym) :
    m (Option (Option (ℕ × K) × Message Sym × ℕ × StA onoff Sym)) := do
  let (dkA, ekA, ich) ←
    match stA.dkA with
    | none => do
        let (ekA, dkA) ← kem.keygen
        pure (some dkA, some ekA, 0)
    | some dkA =>
        pure (some dkA, stA.ekA, stA.ich)
  let ich := if stA.ack.ekRec then ich else ich + 1
  let ch? : Option (ℕ × Sym) :=
    if stA.ack.ekRec then
      none
    else
      match ekA with
      | none => none
      | some ekA =>
          some (ecEk.encode ekA ich)
  let msg := (ch?, stA.ack, stA.t, none)
  let stA' := { stA with dkA := dkA, ekA := ekA, ich := ich }
  pure (some (none, msg, stA.t - 1, stA'))

rleak version leaking key generation coins

def sendArleak (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (ecEk : ErasureCodePayload PK Sym)
  (leak : KEMScheme.OnOffRandLeak kem onoff) (stA : StA onoff Sym) :
  m (Option (Option (ℕ × K) × Message Sym × ℕ × StA onoff Sym ×
    SendRand leak.KeygenRand leak.OffRand leak.OnRand)) := do
    let (dkA, ekA, ich, rand) ←
      match stA.dkA with
      | none => do
        -- First epoch send: run the leaking KeyGen and remember its coins.
          let ((ekA, dkA), rKeygen) ← leak.keygenRleak
          pure (some dkA, some ekA, 0, SendRand.keygen rKeygen)
      | some dkA =>
        -- Subsequent chunk sends are deterministic, so no primitive coins leak.
          pure (some dkA, stA.ekA, stA.ich, SendRand.none)
    let ich := if stA.ack.ekRec then ich else ich + 1
    let ch? : Option (ℕ × Sym) :=
      if stA.ack.ekRec then
        none
      else
        match ekA with
        | none => none
        | some ekA =>
            some (ecEk.encode ekA ich)
    let msg := (ch?, stA.ack, stA.t, none)
    let stA' := { stA with dkA := dkA, ekA := ekA, ich := ich }
    -- normal send output plus randomness-leakage
    pure (some (none, msg, stA.t - 1, stA', rand))

\mathsf{CKA}\text{-}\RecA(\stA,\rho)

\begin{array}{l} (\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack)\gets\stA \\ (\chunk,\ack',t',b)\gets\rho \\ I_{\B}\gets\bot, t_{I_{\B}}\gets\bot \\ \mathsf{if}\;t=t'\;\mathsf{then} \\ \quad \mathsf{if}\;\ctzero=\bot\wedge b=0\;\mathsf{then} \pcomment{\ctzero\ \text{not received yet}} \\ \qquad \Lch\gets\Lch\cup\{\chunk\} \\ \qquad \ctzero\gets\mathsf{Decode}(\Lch) \\ \qquad \mathsf{if}\;\ctzero\ne\bot\;\mathsf{then} \\ \qquad\quad \ack.\ctrec\gets\mathsf{true}, \Lch\gets\emptyset \\ \quad \mathsf{else}\;\mathsf{if}\;b=1\;\mathsf{then} \pcomment{\ctone\ \text{not received yet}} \\ \qquad \Lch\gets\Lch\cup\{\chunk\} \\ \qquad \ctone\gets\mathsf{Decode}(\Lch) \\ \qquad \mathsf{if}\;\ctone\ne\bot\;\mathsf{then} \pcomment{\ctone\ \text{recovered from chunk}} \\ \qquad\quad I_{\B}\gets\Decaps(\dkA,(\ctzero,\ctone)) \\ \qquad\quad t_{I_{\B}}\gets t, t\gets t+1, \Lch\gets\emptyset \\ \qquad\quad (\dkA,\ekA,\ctzero)\gets(\bot,\bot,\bot) \\ \qquad\quad (\ack.\ekrec,\ack.\ctrec) \gets(\mathsf{false},\mathsf{false}) \\ \mathsf{if}\;\ack'.\ekrec\;\boxed{\wedge\;t=t'}\;\mathsf{then} \pcomment{\text{incorporate }\B\text{'s acknowledgment}} \\ \quad \ack.\ekrec\gets\mathsf{true} \\ \stA\gets(\dkA,\ekA,\ctzero,t,\ich,\Lch,\ack) \\ \mathsf{return}\;((t_{I_{\B}},I_{\B}),t'-1,\stA) \end{array}

def recvA (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    [DecidableEq Sym]
  (hDet : kem.DeterministicDecaps)
    (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
    (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (stA : StA onoff Sym) (ρ : Message Sym) :
    Option (Option (ℕ × K) × ℕ × StA onoff Sym) :=
  let (ch?, ack', t', b?) := ρ
  let (key?, stA') :=
    if stA.t = t' then
      let (key?, stA') :=
        match stA.ct0, b?, ch? with
        | none, some 0, some ch =>
            -- `ct_0` not received yet
            let lch := insert ch stA.lch
            match ecCt0.decode lch with
            -- still not received enough chunks to decode `ct_0`
            | none => (none, { stA with ct0 := none, lch := lch })
            -- decoded `ct_0` successfully
            | some ct0 =>
                (none,
                  { stA with
                    ct0 := some ct0
                    lch := ∅
                    ack := { stA.ack with ctRec := true } })
        | _, some 1, some ch =>
        -- processing `ct_1` chunks; without `dk_A` or `ct_0`, output no key
        -- and leave state unchanged
            match stA.dkA, stA.ct0 with
            | some dkA, some ct0 =>
                let lch := insert ch stA.lch
                match ecCt1.decode lch with
                | none => (none, { stA with lch := lch })
                | some ct1 =>
                -- decoded `ct_1` successfully; decapsulate (ct_0, ct_1) to get an epoch key
                  match hDet.decapsDet dkA (onoff.split.symm (ct0, ct1)) with
                  | none => (none, stA)
                  | some key =>
                      (some (stA.t, key),
                        { stA with
                          dkA := none
                          ekA := none
                          ct0 := none
                          t := stA.t + 1
                          lch := ∅
                          ack := { ekRec := false, ctRec := false } })
            | _, _ => (none, stA)
        | _, _, _ => (none, stA)
      -- Incorporate B's acknowledgement only if this receive did not advance A
      -- to the next epoch; otherwise a final `ct_1` message would carry the old
      -- epoch's ack into the fresh epoch.
      let stA' :=
        if ack'.ekRec && stA'.t == t' then
          { stA' with ack := { stA'.ack with ekRec := true } }
        else
          stA'
      (key?, stA')
    else
      (none, stA)
  some (key?, t' - 1, stA')

\mathsf{CKA}\text{-}\SendB(\stB)

\begin{array}{l} (\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack)\gets\stB \\ I_{\B}\gets\bot, t_{I_{\B}}\gets\bot, \chunk\gets\bot \\ \mathsf{if}\;\ctzero=\bot\;\mathsf{then}\pcomment{\text{first message of epoch}} \\ \quad (\stct,\ctzero)\sample\Encaps.\mathsf{Off} \\ \quad \ich\gets0 \\ \mathsf{if}\;\neg\ack.\ctrec\;\mathsf{then} \pcomment{\ctzero\ \text{not acknowledged by }\A} \\ \quad \ich\gets\ich+1 \\ \quad \chunk\gets\mathsf{Encode}(\ctzero,\ich) \\ \quad b\gets0 \\ \mathsf{else}\;\mathsf{if}\;\ekA\ne\bot\;\mathsf{then} \pcomment{\ekA\ \text{received}} \\ \quad \mathsf{if}\;\ctone=\bot\;\mathsf{then} \\ \qquad (\ctone,I_{\B})\sample \Encaps.\mathsf{On}(\stct,\ekA) \\ \qquad t_{I_{\B}}\gets t, \ich\gets0 \\ \quad \ich\gets\ich+1 \\ \quad \chunk\gets\mathsf{Encode}(\ctone,\ich) \\ \quad b\gets1 \\ \rho\gets(\chunk,\ack,t,b) \\ \stB\gets(\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack) \\ \mathsf{return}\;((t_{I_{\B}},I_{\B}),\rho,t-1,\stB) \end{array}

def sendB (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
    (ecCt1 : ErasureCodePayload onoff.C₁ Sym) (stB : StB onoff Sym) :
    m (Option (Option (ℕ × K) × Message Sym × ℕ × StB onoff Sym)) := do
  let (stB, ct0, ich) ←
  match stB.ct0 with
  | none => do -- first message of the epoch: run offline encapsulation
    let (stCt, ct0) ← onoff.encapsOff
    pure ({ stB with stCt := some stCt, ct0 := some ct0 }, ct0, 0)
  | some ct0 =>
    pure (stB, ct0, stB.ich)
  if !stB.ack.ctRec then -- `ct_0` not yet acknowledged by A: send chunks of `ct_0`
  let ich := ich + 1
  let ch? := some (ecCt0.encode ct0 ich)
  let msg := (ch?, stB.ack, stB.t, some 0)
  let stB' := { stB with ich := ich }
  pure (some (none, msg, stB.t - 1, stB'))
  else
  match stB.ekA with
  | none =>  -- `ek_A` not yet received
    let msg := (none, stB.ack, stB.t, none)
    pure (some (none, msg, stB.t - 1, stB))
  | some ekA => -- `ek_A` received
    match stB.ct1 with
    | none =>
      match stB.stCt with
      | none =>
        let msg := (none, stB.ack, stB.t, some 1)
        pure (some (none, msg, stB.t - 1, stB))
      | some stCt => do
        let (ct1, key) ← onoff.encapsOn stCt ekA
        let ich := 1
        let ch? := some (ecCt1.encode ct1 ich)
        let msg := (ch?, stB.ack, stB.t, some 1)
        let stB' := { stB with ct1 := some ct1, ich := ich }
        pure (some (some (stB.t, key), msg, stB.t - 1, stB'))
    | some ct1 =>
      let ich := stB.ich + 1
      let ch? := some (ecCt1.encode ct1 ich)
      let msg := (ch?, stB.ack, stB.t, some 1)
      let stB' := { stB with ich := ich }
      pure (some (none, msg, stB.t - 1, stB'))

rleak version leaking encapsulation coins

def sendBrleak (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
    (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
    (leak : KEMScheme.OnOffRandLeak kem onoff) (stB : StB onoff Sym) :
    m (Option (Option (ℕ × K) × Message Sym × ℕ × StB onoff Sym ×
      SendRand leak.KeygenRand leak.OffRand leak.OnRand)) :=
  do
    let (stB, ct0, ich, rOff?) ←
      match stB.ct0 with
      | none => do
        -- First `ct_0` send: run leaking offline encapsulation.
        let ((stCt, ct0), rOff) ← leak.encapsOffRleak
        pure ({ stB with stCt := some stCt, ct0 := some ct0 }, ct0, 0, some rOff)
      | some ct0 =>
        -- Re-sending existing `ct_0` is deterministic.
        pure (stB, ct0, stB.ich, none)
    let offRand :=
      match rOff? with
      | none => SendRand.none
      | some rOff => SendRand.off rOff
    if !stB.ack.ctRec then
      let ich := ich + 1
      let ch? := some (ecCt0.encode ct0 ich)
      let msg := (ch?, stB.ack, stB.t, some 0)
      let stB' := { stB with ich := ich }
      pure (some (none, msg, stB.t - 1, stB', offRand))
    else
      match stB.ekA with
      | none =>
        let msg := (none, stB.ack, stB.t, none)
        pure (some (none, msg, stB.t - 1, stB, offRand))
      | some ekA =>
        match stB.ct1 with
        | none =>
          match stB.stCt with
          | none =>
            let msg := (none, stB.ack, stB.t, some 1)
            pure (some (none, msg, stB.t - 1, stB, offRand))
          | some stCt => do
            -- First `ct_1` send: run leaking online encapsulation.
            let ((ct1, key), rOn) ← leak.encapsOnRleak stCt ekA
            let rand :=
              match rOff? with
              | none => SendRand.on rOn
              | some rOff => SendRand.offOn rOff rOn
            let ich := 1
            let ch? := some (ecCt1.encode ct1 ich)
            let msg := (ch?, stB.ack, stB.t, some 1)
            let stB' := { stB with ct1 := some ct1, ich := ich }
            pure (some (some (stB.t, key), msg, stB.t - 1, stB', rand))
        | some ct1 =>
          -- Re-sending existing `ct_1` is deterministic.
          let ich := stB.ich + 1
          let ch? := some (ecCt1.encode ct1 ich)
          let msg := (ch?, stB.ack, stB.t, some 1)
          let stB' := { stB with ich := ich }
          pure (some (none, msg, stB.t - 1, stB', offRand))

\mathsf{CKA}\text{-}\RecB(\stB,\rho)

\begin{array}{l} (\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack)\gets\stB \\ (\chunk,\ack',t',\_)\gets\rho \\ \mathsf{if}\;t<t'\;\mathsf{then}\pcomment{\text{first message of next epoch}} \\ \quad t\gets t+1 \\ \quad (\ctzero,\ctone,\stct)\gets(\bot,\bot,\bot) \\ \quad (\ekA,\Lch)\gets(\bot,\emptyset) \\ \quad (\ack.\ekrec,\ack.\ctrec) \gets(\mathsf{false},\mathsf{false}) \\ \mathsf{if}\;t=t'\wedge\ekA=\bot\;\mathsf{then} \\ \quad \Lch\gets\Lch\cup\{\chunk\} \\ \quad \ekA\gets\mathsf{Decode}(\Lch) \\ \quad \ack.\ekrec\gets(\ekA\ne\bot) \\ \mathsf{if}\;\ack'.\ctrec\;\boxed{\wedge\;t=t'}\;\mathsf{then} \pcomment{\text{incorporate }\A\text{'s acknowledgment}} \\ \quad \ack.\ctrec\gets\mathsf{true} \\ \stB\gets(\ekA,\ctzero,\ctone,\stct,t,\ich,\Lch,\ack) \\ \mathsf{return}\;((\bot,\bot),\boxed{t'-1},\stB) \end{array}

def recvB (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
    [DecidableEq Sym]
    (ecEk : ErasureCodePayload PK Sym) (stB : StB onoff Sym) (ρ : Message Sym) :
    Option (Option (ℕ × K) × ℕ × StB onoff Sym) :=
  let (ch?, ack', t', _b?) := ρ
  -- first message of the next epoch: advance and reset the per-epoch state
  let stB :=
    if stB.t < t' then
      { stB with
        t := stB.t + 1
        ct0 := none, ct1 := none, stCt := none
        ekA := none, lch := ∅
        ack := { ekRec := false, ctRec := false } }
    else
      stB
  -- collect chunks of `ek_A` for the current epoch
  let stB :=
    if stB.t = t' ∧ stB.ekA.isNone then
      let lch :=
        match ch? with
        | none => stB.lch
        | some ch => insert ch stB.lch
      let ekA? := ecEk.decode lch
      { stB with ekA := ekA?, lch := lch, ack := { stB.ack with ekRec := ekA?.isSome } }
    else
      stB
  -- incorporate A's acknowledgement only for messages of the current epoch
  let stB :=
    if ack'.ctRec && stB.t == t' then
      { stB with ack := { stB.ack with ctRec := true } }
    else
      stB
  -- Return the delivered message's sending epoch `t' - 1`.
  some (none, t' - 1, stB)

SCKA scheme instance

def scheme (kem : KEMScheme m K PK SK C) (onoff : kem.OnOffStructure)
  [DecidableEq Sym]
    (hDet : kem.DeterministicDecaps)
    (ecEk : ErasureCodePayload PK Sym)
    (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
    (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
    (leak : KEMScheme.OnOffRandLeak kem onoff) :
    SCKAScheme m Unit (StA onoff Sym) (StB onoff Sym) K (Message Sym)
      (SendRand leak.KeygenRand leak.OffRand leak.OnRand) where
  initKeyGen := initKeyGen
  initA := initA kem onoff
  initB := initB kem onoff
  sendA := sendA kem onoff ecEk
  sendArleak := sendArleak kem onoff ecEk leak
  recvA := recvA kem onoff hDet ecCt0 ecCt1
  sendB := sendB kem onoff ecCt0 ecCt1
  sendBrleak := sendBrleak kem onoff ecCt0 ecCt1 leak
  recvB := recvB kem onoff ecEk

uses Definition 9.1.1 · Definition 4.1.1 · Definition 6.3.1 · Definition 6.3.5 · github #106

Lean code for Definition9.4.1●12 definitions

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.initKeyGen.{u} {m : Type → Type u} [Monad m] : m Unit

def oppUniKemCKA.initKeyGen.{u}
  {m : Type → Type u} [Monad m] : m Unit

`CKA-Init-KeyGen`: `I_CKA := ⊥` (there is no shared initial key).

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.initA.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (_ik : Unit) :
  m (oppUniKemCKA.StA onoff Sym)

def oppUniKemCKA.initA.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (_ik : Unit) :
  m (oppUniKemCKA.StA onoff Sym)

`CKA-Init-A`: `st_A ← (⊥, ⊥, ⊥, 1, 0, ∅, (false, false))`.

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.initB.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (_ik : Unit) :
  m (oppUniKemCKA.StB onoff Sym)

def oppUniKemCKA.initB.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (_ik : Unit) :
  m (oppUniKemCKA.StB onoff Sym)

`CKA-Init-B`: `st_B ← (⊥, ⊥, ⊥, ⊥, 1, 0, ∅, (false, false))`.

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.vulnA.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (stA : oppUniKemCKA.StA onoff Sym) :
  Finset ℕ

def oppUniKemCKA.vulnA.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (stA : oppUniKemCKA.StA onoff Sym) :
  Finset ℕ

A's vulnerable epoch set (Fig. 16: `{t}` iff `dk_A ≠ ⊥`).

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.vulnB.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (stB : oppUniKemCKA.StB onoff Sym) :
  Finset ℕ

def oppUniKemCKA.vulnB.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (stB : oppUniKemCKA.StB onoff Sym) :
  Finset ℕ

B's vulnerable epoch set (Fig. 16: `{t}` iff `st_ct ≠ ⊥`).

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.sendA.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (ecEk : ErasureCodePayload PK Sym)
  (stA : oppUniKemCKA.StA onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym × ℕ × oppUniKemCKA.StA onoff Sym))

def oppUniKemCKA.sendA.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (ecEk : ErasureCodePayload PK Sym)
  (stA : oppUniKemCKA.StA onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ × oppUniKemCKA.StA onoff Sym))

`CKA-Send-A`.

```text
parse (dk_A, ek_A, ct_0, t, i_ch, L_ch, ack) <- st_A
ch <- ⊥
if dk_A = ⊥ then
  (ek_A, dk_A) <- KeyGen
  i_ch <- 0
if ¬ack.ek-rec then
  i_ch <- i_ch + 1
  ch <- Encode(ek_A, i_ch)
rho <- (ch, ack, t, ⊥)
st_A <- (dk_A, ek_A, ct_0, t, i_ch, L_ch, ack)
return ((⊥, ⊥), rho, t - 1, st_A)
```

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.sendArleak.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (ecEk : ErasureCodePayload PK Sym)
  (leak : kem.OnOffRandLeak onoff) (stA : oppUniKemCKA.StA onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ ×
            oppUniKemCKA.StA onoff Sym ×
              oppUniKemCKA.SendRand leak.KeygenRand leak.OffRand
                leak.OnRand))

def oppUniKemCKA.sendArleak.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (ecEk : ErasureCodePayload PK Sym)
  (leak : kem.OnOffRandLeak onoff)
  (stA : oppUniKemCKA.StA onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ ×
            oppUniKemCKA.StA onoff Sym ×
              oppUniKemCKA.SendRand
                leak.KeygenRand
                leak.OffRand leak.OnRand))

Randomness-leaking `CKA-Send-A`, also returning the send coins.

The only randomized primitive in `CKA-Send-A` is `KeyGen`, and it is used only
on the first message of an epoch. Later sends only repeat deterministic chunk
encoding, so they leak `SendRand.none`.

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.recvA.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) [DecidableEq Sym]
  (hDet : kem.DeterministicDecaps)
  (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (stA : oppUniKemCKA.StA onoff Sym) (ρ : oppUniKemCKA.Message Sym) :
  Option (Option (ℕ × K) × ℕ × oppUniKemCKA.StA onoff Sym)

def oppUniKemCKA.recvA.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  [DecidableEq Sym]
  (hDet : kem.DeterministicDecaps)
  (ecCt0 :
    ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 :
    ErasureCodePayload onoff.C₁ Sym)
  (stA : oppUniKemCKA.StA onoff Sym)
  (ρ : oppUniKemCKA.Message Sym) :
  Option
    (Option (ℕ × K) ×
      ℕ × oppUniKemCKA.StA onoff Sym)

`CKA-Rec-A`.

```text
parse (dk_A, ek_A, ct_0, t, i_ch, L_ch, ack) <- st_A
parse (ch, ack', t', b) <- rho
I_B <- ⊥, t_IB <- ⊥
  if t = t' then
  if ct_0 = ⊥ ∧ b = 0 then
    L_ch <- L_ch ∪ {ch}
    ct_0 <- Decode(L_ch)
    if ct_0 ≠ ⊥ then
      ack.ct_0-rec <- true
      L_ch <- ∅
  elseif b = 1 then
    L_ch <- L_ch ∪ {ch}
    ct_1 <- Decode(L_ch)
    if ct_1 ≠ ⊥ then
      I_B <- Dec(dk_A, (ct_0, ct_1))
      t_IB <- t
      t <- t + 1
      L_ch <- ∅
      (dk_A, ek_A, ct_0) <- (⊥, ⊥, ⊥)
      (ack.ek-rec, ack.ct_0-rec) <- (false, false)
  if ack'.ek-rec and t = t' then
    ack.ek-rec <- true
st_A <- (dk_A, ek_A, ct_0, t, i_ch, L_ch, ack)
return ((t_IB, I_B), t' - 1, st_A)
```

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.sendB.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (stB : oppUniKemCKA.StB onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym × ℕ × oppUniKemCKA.StB onoff Sym))

def oppUniKemCKA.sendB.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (ecCt0 :
    ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 :
    ErasureCodePayload onoff.C₁ Sym)
  (stB : oppUniKemCKA.StB onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ × oppUniKemCKA.StB onoff Sym))

`CKA-Send-B`.

```text
parse (ek_A, ct_0, ct_1, st_ct, t, i_ch, L_ch, ack) <- st_B
I_B <- ⊥, t_IB <- ⊥, ch <- ⊥
if ct_0 = ⊥ then  -- first message of the epoch: run offline encapsulation
  (st_ct, ct_0) <- Enc.Off
  i_ch <- 0
if ¬ack.ct_0-rec then -- `ct_0` not yet acknowledged by A: send chunks of `ct_0`
  i_ch <- i_ch + 1
  ch <- Encode(ct_0, i_ch)
  b <- 0
elseif ek_A ≠ ⊥ then -- `ek_A` received: run online encapsulation and send chunks of `ct_1`
  if ct_1 = ⊥ then
    (ct_1, I_B) <- Enc.On(st_ct, ek_A)
    t_IB <- t
    i_ch <- 0
  i_ch <- i_ch + 1
  ch <- Encode(ct_1, i_ch)
  b <- 1
rho <- (ch, ack, t, b)
st_B <- (ek_A, ct_0, ct_1, st_ct, t, i_ch, L_ch, ack)
return ((t_IB, I_B), rho, t - 1, st_B)
```

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.sendBrleak.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (leak : kem.OnOffRandLeak onoff) (stB : oppUniKemCKA.StB onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ ×
            oppUniKemCKA.StB onoff Sym ×
              oppUniKemCKA.SendRand leak.KeygenRand leak.OffRand
                leak.OnRand))

def oppUniKemCKA.sendBrleak.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  (ecCt0 :
    ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 :
    ErasureCodePayload onoff.C₁ Sym)
  (leak : kem.OnOffRandLeak onoff)
  (stB : oppUniKemCKA.StB onoff Sym) :
  m
    (Option
      (Option (ℕ × K) ×
        oppUniKemCKA.Message Sym ×
          ℕ ×
            oppUniKemCKA.StB onoff Sym ×
              oppUniKemCKA.SendRand
                leak.KeygenRand
                leak.OffRand leak.OnRand))

Randomness-leaking `CKA-Send-B`: follows `sendB` branch-for-branch, also
returning the coins of the encapsulation phases run by this send.

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.recvB.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) [DecidableEq Sym]
  (ecEk : ErasureCodePayload PK Sym) (stB : oppUniKemCKA.StB onoff Sym)
  (ρ : oppUniKemCKA.Message Sym) :
  Option (Option (ℕ × K) × ℕ × oppUniKemCKA.StB onoff Sym)

def oppUniKemCKA.recvB.{u} {m : Type → Type u}
  [Monad m] {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  [DecidableEq Sym]
  (ecEk : ErasureCodePayload PK Sym)
  (stB : oppUniKemCKA.StB onoff Sym)
  (ρ : oppUniKemCKA.Message Sym) :
  Option
    (Option (ℕ × K) ×
      ℕ × oppUniKemCKA.StB onoff Sym)

`CKA-Rec-B`.

```text
parse (ek_A, ct_0, ct_1, st_ct, t, i_ch, L_ch, ack) <- st_B
parse (ch, ack', t', _) <- rho
if t < t' then  -- first message of next epoch
  t <- t + 1
  (ct_0, ct_1, st_ct) <- (⊥, ⊥, ⊥)
  (ek_A, L_ch) <- (⊥, ∅)
  (ack.ek-rec, ack.ct_0-rec) <- (false, false)
if t = t' ∧ ek_A = ⊥ then
  L_ch <- L_ch ∪ {ch}
  ek_A <- Decode(L_ch)
  ack.ek-rec <- (ek_A ≠ ⊥)
if ack'.ct_0-rec and t = t' then  -- incorporate A's acknowledgment
  ack.ct_0-rec <- true
st_B <- (ek_A, ct_0, ct_1, st_ct, t, i_ch, L_ch, ack)
return ((⊥, ⊥), t' - 1, st_B)
```

defdefined in SecureMessaging/SCKA/OppUniKEM/Construction.lean

complete

def oppUniKemCKA.scheme.{u} {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type} (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure) [DecidableEq Sym]
  (hDet : kem.DeterministicDecaps) (ecEk : ErasureCodePayload PK Sym)
  (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (leak : kem.OnOffRandLeak onoff) :
  SCKAScheme m Unit (oppUniKemCKA.StA onoff Sym)
    (oppUniKemCKA.StB onoff Sym) K (oppUniKemCKA.Message Sym)
    (oppUniKemCKA.SendRand leak.KeygenRand leak.OffRand leak.OnRand)

def oppUniKemCKA.scheme.{u}
  {m : Type → Type u} [Monad m]
  {K PK SK C Sym : Type}
  (kem : KEMScheme m K PK SK C)
  (onoff : kem.OnOffStructure)
  [DecidableEq Sym]
  (hDet : kem.DeterministicDecaps)
  (ecEk : ErasureCodePayload PK Sym)
  (ecCt0 :
    ErasureCodePayload onoff.C₀ Sym)
  (ecCt1 :
    ErasureCodePayload onoff.C₁ Sym)
  (leak : kem.OnOffRandLeak onoff) :
  SCKAScheme m Unit
    (oppUniKemCKA.StA onoff Sym)
    (oppUniKemCKA.StB onoff Sym) K
    (oppUniKemCKA.Message Sym)
    (oppUniKemCKA.SendRand leak.KeygenRand
      leak.OffRand leak.OnRand)

The Opp-UniKEM-CKA protocol as an `SCKAScheme` instance.

Theorem9.4.2

Group: Opp-UniKEM-CKA. (2)

Group member previews

Preview

Definition 9.4.1

Loading preview

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

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.4

Loading preview

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

used by 0✓L∃∀N

Assume that:

\adv is any SCKA correctness adversary making at most q send-oracle queries;
the underlying KEM has deterministic decapsulation, and has correctness error at most \varepsilon;
and the three erasure codes are correct.

Then \Pr\bigl[\Exp{\textsf{cor}}{\textsf{Opp-UniKEM-CKA}}(\adv)=1\bigr] \ge 1-q\varepsilon, i.e., the Opp-UniKEM-CKA protocol is correct with probability at least 1-q\varepsilon.

theorem correctness_true_ge [DecidableEq K] [DecidableEq Sym]
    (kem : KEMScheme ProbComp K PK SK C) (onoff : kem.OnOffStructure)
    (hDet : DeterministicDecaps kem)
    (ecEk : ErasureCodePayload PK Sym) (hEkCorrect : ecEk.ec.Correct)
    (ecCt0 : ErasureCodePayload onoff.C₀ Sym) (hCt0Correct : ecCt0.ec.Correct)
    (ecCt1 : ErasureCodePayload onoff.C₁ Sym) (hCt1Correct : ecCt1.ec.Correct)
    (leak : KEMScheme.OnOffRandLeak kem onoff)
    (adv : SCKAScheme.SCKACorrectnessAdversary (Message Sym))
    (q : ℕ) (hq : SendQueryBound adv q) :
    Pr[= true |
      SCKAScheme.correctnessExp
        (scheme kem onoff hDet ecEk ecCt0 ecCt1 leak) adv] ≥
      1 - (q : ℝ≥0∞) * kem.correctnessError ProbCompRuntime.probComp

uses Definition 9.4.1 · Definition 9.1.3 · Definition 4.1.4 · Definition 6.3.1 · Definition 6.3.5 · github #107

Lean code for Theorem9.4.2●1 theorem

theoremdefined in SecureMessaging/SCKA/OppUniKEM/Correctness.lean

complete

theorem oppUniKemCKA.correctness_true_ge {K PK SK C Sym : Type} [DecidableEq K]
  [DecidableEq Sym] (kem : KEMScheme ProbComp K PK SK C)
  (onoff : kem.OnOffStructure) (hDet : kem.DeterministicDecaps)
  (ecEk : ErasureCodePayload PK Sym) (hEkCorrect : ecEk.ec.Correct)
  (ecCt0 : ErasureCodePayload onoff.C₀ Sym)
  (hCt0Correct : ecCt0.ec.Correct)
  (ecCt1 : ErasureCodePayload onoff.C₁ Sym)
  (hCt1Correct : ecCt1.ec.Correct) (leak : kem.OnOffRandLeak onoff)
  (adv : SCKAScheme.SCKACorrectnessAdversary (oppUniKemCKA.Message Sym))
  (q : ℕ) (hq : oppUniKemCKA.SendQueryBound adv q) :
  Pr[= true |
      (oppUniKemCKA.scheme kem onoff hDet ecEk ecCt0 ecCt1
            leak).correctnessExp
        adv] ≥
    1 - ↑q * kem.correctnessError ProbCompRuntime.probComp

theorem oppUniKemCKA.correctness_true_ge
  {K PK SK C Sym : Type} [DecidableEq K]
  [DecidableEq Sym]
  (kem : KEMScheme ProbComp K PK SK C)
  (onoff : kem.OnOffStructure)
  (hDet : kem.DeterministicDecaps)
  (ecEk : ErasureCodePayload PK Sym)
  (hEkCorrect : ecEk.ec.Correct)
  (ecCt0 :
    ErasureCodePayload onoff.C₀ Sym)
  (hCt0Correct : ecCt0.ec.Correct)
  (ecCt1 :
    ErasureCodePayload onoff.C₁ Sym)
  (hCt1Correct : ecCt1.ec.Correct)
  (leak : kem.OnOffRandLeak onoff)
  (adv :
    SCKAScheme.SCKACorrectnessAdversary
      (oppUniKemCKA.Message Sym))
  (q : ℕ)
  (hq :
    oppUniKemCKA.SendQueryBound adv q) :
  Pr[= true |
      (oppUniKemCKA.scheme kem onoff hDet
            ecEk ecCt0 ecCt1
            leak).correctnessExp
        adv] ≥
    1 -
      ↑q *
        kem.correctnessError
          ProbCompRuntime.probComp

Assume:

* `kem` has deterministic decapsulation;
* `onoff` splits encapsulation into an offline and an online part;
* `ecEk`, `ecCt0`, and `ecCt1` are correct erasure codes;
* `adv` makes at most `q` `SendA` and `SendB` queries combined.

Then the Opp-UniKEM-CKA correctness game succeeds with probability at least
`1 - q · kem.correctnessError`.

Theorem9.4.3

Group: Opp-UniKEM-CKA. (2)

Group member previews

Preview

Definition 9.4.1

Loading preview

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

Statement uses 5

Statement dependency previews

Preview

Definition 4.1.1

Loading preview

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

used by 0XL∃∀N

\todo

LeanLean anchor pending

uses Definition 9.4.1 · Definition 9.1.4 · Definition 4.1.1 · Definition 6.3.1 · Definition 6.3.5 · github #108