8.1. RKEM Definitions🔗

Definition8.1.1

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.2

Loading preview

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

uses 0

Used by 24

Reverse dependency previews

Preview

Definition 8.1.2

Loading preview

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

✓L∃∀N

GitHub#176

\todo

structure RKEMScheme (m : Type → Type u) [Monad m] (Par EK DK CT K : Type) where
  /-- `RSetup(1^λ) → par`: samples the public parameter shared by both parties. -/
  rsetup : m Par
  /-- `RKeyGen-A(par, ⊥) → (ekA, dkA)`: samples a fresh key pair for `A`. -/
  rkeygenAFresh : Par → m (EK × DK)
  /-- `RKeyGen-A(par, updated) → (ekA, dkA)`: samples an updated-distribution
  key pair for `A`. -/
  rkeygenAUpdated : Par → m (EK × DK)
  /-- `RKeyGen-B(par, ⊥) → (ekB, dkB)`: samples a fresh key pair for `B`. -/
  rkeygenBFresh : Par → m (EK × DK)
  /-- `RKeyGen-B(par, updated) → (ekB, dkB)`: samples an updated-distribution
  key pair for `B`. -/
  rkeygenBUpdated : Par → m (EK × DK)
  /-- `REnc-A(par, ekB, dkA) → (ctB, K, dk̂A)`: encapsulates towards `B`'s
  encapsulation key using `A`'s decapsulation key, producing a ciphertext for
  `B`, the shared key, and `A`'s updated decapsulation key. -/
  rencA : Par → EK → DK → m (CT × K × DK)
  /-- `RDec-A(par, dkA, ctA, ekB) → (K, ek̂B)`: decapsulates using `A`'s
  decapsulation key and `B`'s encapsulation key, producing the shared key and
  `B`'s updated encapsulation key. Never fails. -/
  rdecA : Par → DK → CT → EK → m (K × EK)
  /-- `REnc-B(par, ekA, dkB) → (ctA, K, dk̂B)`: as `rencA`, with the roles of
  `A` and `B` swapped. -/
  rencB : Par → EK → DK → m (CT × K × DK)
  /-- `RDec-B(par, dkB, ctB, ekA) → (K, ek̂A)`: as `rdecA`, with the roles of
  `A` and `B` swapped. -/
  rdecB : Par → DK → CT → EK → m (K × EK)

The algorithms of an RKEM do not expose their coins. Security notions that give the adversary some of these coins, such as ratchet simulatability, are stated relative to a randomness-leak package: fresh key generation and encapsulation algorithms that also return the coins they sampled, and agree with the RKEM's own algorithms on their other outputs.

RandLeak

structure RandLeak (rkem : RKEMScheme m Par EK DK CT K) where
  /-- Randomness space of one fresh key generation `RKeyGen-P(par, ⊥)`. -/
  KeygenRand : Type
  /-- Randomness space of one encapsulation `REnc-P`. -/
  EncRand : Type
  /-- `RKeyGen-A(par, ⊥)`, also returning its coins. -/
  rkeygenAFreshRleak : Par → m ((EK × DK) × KeygenRand)
  /-- `RKeyGen-B(par, ⊥)`, also returning its coins. -/
  rkeygenBFreshRleak : Par → m ((EK × DK) × KeygenRand)
  /-- `REnc-A(par, ekB, dkA)`, also returning its coins. -/
  rencARleak : Par → EK → DK → m ((CT × K × DK) × EncRand)
  /-- `REnc-B(par, ekA, dkB)`, also returning its coins. -/
  rencBRleak : Par → EK → DK → m ((CT × K × DK) × EncRand)
  /-- Ordinary fresh key generation for `A` is the first component of `rkeygenAFreshRleak`. -/
  rkeygenAFresh_fst : ∀ par,
    (do
      let out ← rkeygenAFreshRleak par
      pure out.1) = rkem.rkeygenAFresh par
  /-- Ordinary fresh key generation for `B` is the first component of `rkeygenBFreshRleak`. -/
  rkeygenBFresh_fst : ∀ par,
    (do
      let out ← rkeygenBFreshRleak par
      pure out.1) = rkem.rkeygenBFresh par
  /-- Ordinary encapsulation for `A` is the first component of `rencARleak`. -/
  rencA_fst : ∀ par ek dk,
    (do
      let out ← rencARleak par ek dk
      pure out.1) = rkem.rencA par ek dk
  /-- Ordinary encapsulation for `B` is the first component of `rencBRleak`. -/
  rencB_fst : ∀ par ek dk,
    (do
      let out ← rencBRleak par ek dk
      pure out.1) = rkem.rencB par ek dk

Lean code for Definition8.1.1●2 definitions

structure(9 fields)defined in SecureMessaging/RKEM/Defs.lean

complete

structure RKEMScheme.{u} (m : Type → Type u) [Monad m] (Par EK DK CT K : Type) :
  Type u

structure RKEMScheme.{u} (m : Type → Type u)
  [Monad m] (Par EK DK CT K : Type) :
  Type u

A forward-secure ratcheting key encapsulation mechanism (RKEM), as in
Definition 5.1 of [TripleRatchet]. Public-parameter space `Par`, encapsulation-
and decapsulation-key spaces `EK`, `DK`, ciphertext space `CT`, and shared-key
space `K`.

Fields

rsetup : m Par

`RSetup(1^λ) → par`: samples the public parameter shared by both parties.

rkeygenAFresh : Par → m (EK × DK)

`RKeyGen-A(par, ⊥) → (ekA, dkA)`: samples a fresh key pair for `A`.

rkeygenAUpdated : Par → m (EK × DK)

`RKeyGen-A(par, updated) → (ekA, dkA)`: samples an updated-distribution
key pair for `A`.

rkeygenBFresh : Par → m (EK × DK)

`RKeyGen-B(par, ⊥) → (ekB, dkB)`: samples a fresh key pair for `B`.

rkeygenBUpdated : Par → m (EK × DK)

`RKeyGen-B(par, updated) → (ekB, dkB)`: samples an updated-distribution
key pair for `B`.

rencA : Par → EK → DK → m (CT × K × DK)

`REnc-A(par, ekB, dkA) → (ctB, K, dk̂A)`: encapsulates towards `B`'s
encapsulation key using `A`'s decapsulation key, producing a ciphertext for
`B`, the shared key, and `A`'s updated decapsulation key.

rdecA : Par → DK → CT → EK → m (K × EK)

`RDec-A(par, dkA, ctA, ekB) → (K, ek̂B)`: decapsulates using `A`'s
decapsulation key and `B`'s encapsulation key, producing the shared key and
`B`'s updated encapsulation key. Never fails.

rencB : Par → EK → DK → m (CT × K × DK)

`REnc-B(par, ekA, dkB) → (ctA, K, dk̂B)`: as `rencA`, with the roles of
`A` and `B` swapped.

rdecB : Par → DK → CT → EK → m (K × EK)

`RDec-B(par, dkB, ctB, ekA) → (K, ek̂A)`: as `rdecA`, with the roles of
`A` and `B` swapped.

structure(10 fields)defined in SecureMessaging/RKEM/Defs.lean

complete

structure RKEMScheme.RandLeak.{u} {m : Type → Type u} [Monad m]
  {Par EK DK CT K : Type} (rkem : RKEMScheme m Par EK DK CT K) :
  Type (max 1 u)

structure RKEMScheme.RandLeak.{u}
  {m : Type → Type u} [Monad m]
  {Par EK DK CT K : Type}
  (rkem : RKEMScheme m Par EK DK CT K) :
  Type (max 1 u)

Randomness-leaking versions of fresh key generation `RKeyGen-P(par, ⊥)` and encapsulation
`REnc-P`, for both parties, as needed by security notions that expose these algorithms' coins,
such as the ratchet-simulatability distributions of [TripleRatchet, Figs. 11–12] (their
`D_RKeyGen-P{rand}` and `REnc-A(…; rand₂)` lines). Each returns the ordinary output together
with the coins it sampled; the `_fst` fields say that the ordinary algorithm is the first
component. The coins of updated key generation and of decapsulation are never exposed, so they
have no leaking version.

Fields

KeygenRand : Type

Randomness space of one fresh key generation `RKeyGen-P(par, ⊥)`.

EncRand : Type

Randomness space of one encapsulation `REnc-P`.

rkeygenAFreshRleak : Par → m ((EK × DK) × self.KeygenRand)

`RKeyGen-A(par, ⊥)`, also returning its coins.

rkeygenBFreshRleak : Par → m ((EK × DK) × self.KeygenRand)

`RKeyGen-B(par, ⊥)`, also returning its coins.

rencARleak : Par → EK → DK → m ((CT × K × DK) × self.EncRand)

`REnc-A(par, ekB, dkA)`, also returning its coins.

rencBRleak : Par → EK → DK → m ((CT × K × DK) × self.EncRand)

`REnc-B(par, ekA, dkB)`, also returning its coins.

rkeygenAFresh_fst : ∀ (par : Par),
  (do
      let out ← self.rkeygenAFreshRleak par
      pure out.1) =
    rkem.rkeygenAFresh par

Ordinary fresh key generation for `A` is the first component of `rkeygenAFreshRleak`.

rkeygenBFresh_fst : ∀ (par : Par),
  (do
      let out ← self.rkeygenBFreshRleak par
      pure out.1) =
    rkem.rkeygenBFresh par

Ordinary fresh key generation for `B` is the first component of `rkeygenBFreshRleak`.

rencA_fst : ∀ (par : Par) (ek : EK) (dk : DK),
  (do
      let out ← self.rencARleak par ek dk
      pure out.1) =
    rkem.rencA par ek dk

Ordinary encapsulation for `A` is the first component of `rencARleak`.

rencB_fst : ∀ (par : Par) (ek : EK) (dk : DK),
  (do
      let out ← self.rencBRleak par ek dk
      pure out.1) =
    rkem.rencB par ek dk

Ordinary encapsulation for `B` is the first component of `rencBRleak`.

Definition8.1.2

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1

Used by 6

Reverse dependency previews

Preview

Theorem 8.2.3

Loading preview

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

✓L∃∀N

GitHub#179

Adapted from Dodis et al. (2025), Definition 5.5 and Figures 10–12.

An RKEM is ratchet simulatable if there exist efficient simulators (\RSimKey\text{-}\mathsf{P}_1,\RSimKey\text{-}\mathsf{P}_2,\RSimCtxt\text{-}\mathsf{P})_{\mathsf{P}\in\{\A,\B\}} such that, for both parties \mathsf{P}, the real distribution \mathcal{D}_{\mathsf{P},0} and the simulated distribution \mathcal{D}_{\mathsf{P},1} of each of the three properties below are indistinguishable. Each property is shown for one party only, as in the paper; the other party's distributions swap the roles of \A and \B.

\textsf{Simulators}

For each party \mathsf{P}\in\{\A,\B\}, with peer \mathsf{\bar P}:

\RSimKey\text{-}\mathsf{P}_1(\ek_\mathsf{P},\dk_\mathsf{P})\to(\ekh{P},\dkh{P},\aux): from \mathsf{P}'s fresh key pair, simulate \mathsf{P}'s updated key pair, with auxiliary state \aux.

\RSimKey\text{-}\mathsf{P}_2(\ekh{\bar P},\dkh{\bar P},\aux)\to(\ct_{\mathsf{\bar P}},K,K',\rand): from the peer's updated key pair and \aux, simulate the rest of \mathsf{P}'s round: the ciphertext sent to the peer, both parties' shared keys, and coins explaining \REnc\text{-}\mathsf{P}.

\RSimCtxt\text{-}\mathsf{P}(\ekh{P},\ekh{\bar P},\dkh{\bar P})\to(\ct_{\mathsf{\bar P}},\ek_\mathsf{P},K,K'): from \mathsf{P}'s updated encapsulation key and the peer's updated key pair, simulate \mathsf{P}'s ciphertext, \mathsf{P}'s fresh encapsulation key and both shared keys, without \mathsf{P}'s decapsulation key.

RatchetSimulator

structure RatchetSimulator (rkem : RKEMScheme ProbComp Par EK DK CT K) (leak : rkem.RandLeak)
    where
  /-- Auxiliary state produced by `RSimKey-P₁` and consumed by `RSimKey-P₂`. -/
  Aux : Type
  /-- `RSimKey-A₁(par, ekA, dkA) → (ekÂ, dkÂ, aux)`: simulates `A`'s updated key pair from `A`'s
  fresh key pair. -/
  rsimKeyA1 : Par → EK → DK → ProbComp (EK × DK × Aux)
  /-- `RSimKey-A₂(par, ekB̂, dkB̂, aux) → (ctB, K, K', rand₂)`: completes `A`'s round from `B`'s
  updated key pair, producing the ciphertext to `B`, `A`'s and `B`'s shared keys, and coins
  explaining `REnc-A`. -/
  rsimKeyA2 : Par → EK → DK → Aux → ProbComp (CT × K × K × leak.EncRand)
  /-- `RSimCtxt-A(par, ekÂ, ekB̂, dkB̂) → (ctB, ekA, K, K')`: simulates `A`'s ciphertext and
  fresh encapsulation key from `A`'s updated encapsulation key and `B`'s updated key pair. -/
  rsimCtxtA : Par → EK → EK → DK → ProbComp (CT × EK × K × K)
  /-- `RSimKey-B₁`: as `rsimKeyA1`, with the roles of `A` and `B` swapped. -/
  rsimKeyB1 : Par → EK → DK → ProbComp (EK × DK × Aux)
  /-- `RSimKey-B₂`: as `rsimKeyA2`, with the roles of `A` and `B` swapped. -/
  rsimKeyB2 : Par → EK → DK → Aux → ProbComp (CT × K × K × leak.EncRand)
  /-- `RSimCtxt-B`: as `rsimCtxtA`, with the roles of `A` and `B` swapped. -/
  rsimCtxtB : Par → EK → EK → DK → ProbComp (CT × EK × K × K)

The updated-key and ciphertext distributions give the distinguisher the coins of some algorithms: \mathcal{D}\{\rand\} samples from \mathcal{D} with coins \rand, which are uniformly distributed unless a simulator outputs them. These coins come from the RKEM's randomness-leak package (see the RKEM scheme).

Base-key simulatability (\mathsf{KeyBaseSim}). A fresh key pair passed through \RSimKey\text{-}\mathsf{P}_1 is indistinguishable from an updated key pair. This captures the first keys shared between the parties in the CKA protocol.

\mathcal{D}^{\mathsf{KeyBaseSim}}_{\A,0}

\begin{array}{l} (\ekh{\A},\dkh{\A})\sample\DRKGup{\A} \\ \Return(\ekh{\A},\dkh{\A}) \end{array}

\mathcal{D}^{\mathsf{KeyBaseSim}}_{\A,1}

\begin{array}{l} (\ekA,\dkA)\sample\DRKG{\A} \\ (\ekh{\A},\dkh{\A},\_)\sample\RSimKey\text{-}\A_1(\ekA,\dkA) \\ \Return(\ekh{\A},\dkh{\A}) \end{array}

Base-key distributions

def keyBaseSimDistA (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) : ProbComp (EK × DK) :=
  if b = false then
    rkem.rkeygenAUpdated par
  else do
    let (ekA, dkA) ← rkem.rkeygenAFresh par
    let (ekAHat, dkAHat, _) ← sim.rsimKeyA1 par ekA dkA
    return (ekAHat, dkAHat)

Base-key experiment

def keyBaseSimExpA (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak) (adversary : KeyBaseSimAdversary Par EK DK) :
    ProbComp Bool := do
  let b ← $ᵗ Bool
  let par ← rkem.rsetup
  let x ← rkem.keyBaseSimDistA sim par b
  let b' ← adversary par x
  return b == b'

Base-key advantage

noncomputable def keyBaseSimAdvantageA (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversary : KeyBaseSimAdversary Par EK DK) : ℝ :=
  |(Pr[= true | rkem.keyBaseSimExpA sim adversary]).toReal - 1 / 2|

Base-key advantage, maximum over both parties

noncomputable def keyBaseSimAdvantage (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversaryA adversaryB : KeyBaseSimAdversary Par EK DK) : ℝ :=
  max (rkem.keyBaseSimAdvantageA sim adversaryA) (rkem.keyBaseSimAdvantageB sim adversaryB)

Updated-key simulatability (\mathsf{KeyUpdSim}). \mathsf{P}'s updated key pair can be simulated from \mathsf{P}'s fresh key pair alone, without the peer's encapsulation key that \REnc\text{-}\mathsf{P} needs. This breaks the dependence of the updated keys on the peer's keys, which drives the induction in the proof of CKA security from RKEM (Dodis et al. (2025), Theorem 5.6).

\mathcal{D}^{\mathsf{KeyUpdSim}}_{\A,0}

\begin{array}{l} (\ek_\B,\dk_\B)\sample\DRKG{\B}\{\rand_0\} \\ (\ekh{\B},\dkh{\B},\aux_0)\sample\RSimKey\text{-}\B_1(\ek_\B,\dk_\B) \\ (\ekA,\dkA)\sample\DRKG{\A}\{\rand_1\} \\ (\ct_\B,K,\dkh{\A})\getsval\REnc\text{-}\A(\ekh{\B},\dkA;\rand_2) \\ (K',\ekh{\A})\sample\RDec\text{-}\B(\dkh{\B},\ct_\B,\ekA) \\ \Return\big((\ekh{\B},\dkh{\B}),(\ekh{\A},\dkh{\A}),\ct_\B,K,K', \\ \qquad\aux_0,\rand_0,\rand_1,\rand_2\big) \end{array}

\mathcal{D}^{\mathsf{KeyUpdSim}}_{\A,1}

\begin{array}{l} (\ek_\B,\dk_\B)\sample\DRKG{\B}\{\rand_0\} \\ (\ekh{\B},\dkh{\B},\aux_0)\sample\RSimKey\text{-}\B_1(\ek_\B,\dk_\B) \\ (\ekA,\dkA)\sample\DRKG{\A}\{\rand_1\} \\ (\ekh{\A},\dkh{\A},\aux_1)\sample\RSimKey\text{-}\A_1(\ekA,\dkA) \\ (\ct_\B,K,K',\rand_2)\sample\RSimKey\text{-}\A_2(\ekh{\B},\dkh{\B},\aux_1) \\ \Return\big((\ekh{\B},\dkh{\B}),(\ekh{\A},\dkh{\A}),\ct_\B,K,K', \\ \qquad\aux_0,\rand_0,\rand_1,\rand_2\big) \end{array}

Updated-key distributions

def keyUpdSimDistA (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) :
    ProbComp (KeyUpdSimView EK DK CT K sim.Aux leak.KeygenRand leak.EncRand) := do
  let ((ekB, dkB), rand0) ← leak.rkeygenBFreshRleak par
  let (ekBHat, dkBHat, aux0) ← sim.rsimKeyB1 par ekB dkB
  let ((ekA, dkA), rand1) ← leak.rkeygenAFreshRleak par
  if b = false then
    let ((ctB, key, dkAHat), rand2) ← leak.rencARleak par ekBHat dkA
    let (key', ekAHat) ← rkem.rdecB par dkBHat ctB ekA
    return ((ekBHat, dkBHat), (ekAHat, dkAHat), ctB, key, key', aux0, rand0, rand1, rand2)
  else
    let (ekAHat, dkAHat, aux1) ← sim.rsimKeyA1 par ekA dkA
    let (ctB, key, key', rand2) ← sim.rsimKeyA2 par ekBHat dkBHat aux1
    return ((ekBHat, dkBHat), (ekAHat, dkAHat), ctB, key, key', aux0, rand0, rand1, rand2)

Updated-key experiment

def keyUpdSimExpA (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak)
    (adversary : KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand leak.EncRand) :
    ProbComp Bool := do
  let b ← $ᵗ Bool
  let par ← rkem.rsetup
  let x ← rkem.keyUpdSimDistA sim par b
  let b' ← adversary par x
  return b == b'

Updated-key advantage

noncomputable def keyUpdSimAdvantageA (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversary : KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand leak.EncRand) : ℝ :=
  |(Pr[= true | rkem.keyUpdSimExpA sim adversary]).toReal - 1 / 2|

Updated-key advantage, maximum over both parties

noncomputable def keyUpdSimAdvantage (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversaryA adversaryB :
      KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand leak.EncRand) : ℝ :=
  max (rkem.keyUpdSimAdvantageA sim adversaryA) (rkem.keyUpdSimAdvantageB sim adversaryB)

Ciphertext simulatability (\mathsf{CtxtSim}). The ciphertext that \mathsf{P} sends to its peer \mathsf{\bar P} can be simulated from \mathsf{\bar P}'s updated decapsulation key instead of \mathsf{P}'s own: together with \mathsf{\bar P}'s decapsulation key, it leaks nothing about \mathsf{P}'s decapsulation key. This is used to argue post-compromise security of the CKA.

\mathcal{D}^{\mathsf{CtxtSim}}_{\B,0}

\begin{array}{l} (\ekA,\dkA)\sample\DRKG{\A}\{\rand\} \\ (\ekh{\A},\dkh{\A},\aux)\sample\RSimKey\text{-}\A_1(\ekA,\dkA) \\ (\ek_\B,\dk_\B)\sample\DRKG{\B} \\ (\ct_\A,K,\dkh{\B})\sample\REnc\text{-}\B(\ekh{\A},\dk_\B) \\ (K',\ekh{\B})\sample\RDec\text{-}\A(\dkh{\A},\ct_\A,\ek_\B) \\ \Return\big(\aux,\rand,(\ekh{\A},\dkh{\A}),\ct_\A, \\ \qquad(\ek_\B,\ekh{\B}),(K,K')\big) \end{array}

\mathcal{D}^{\mathsf{CtxtSim}}_{\B,1}

\begin{array}{l} (\ekA,\dkA)\sample\DRKG{\A}\{\rand\} \\ (\ekh{\A},\dkh{\A},\aux)\sample\RSimKey\text{-}\A_1(\ekA,\dkA) \\ (\ekh{\B},\dkh{\B})\sample\DRKGup{\B} \\ (\ct_\A,\ek_\B,K,K')\sample\RSimCtxt\text{-}\B(\ekh{\B},\ekh{\A},\dkh{\A}) \\ \Return\big(\aux,\rand,(\ekh{\A},\dkh{\A}),\ct_\A, \\ \qquad(\ek_\B,\ekh{\B}),(K,K')\big) \end{array}

Ciphertext distributions

def ctxtSimDistB (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) :
    ProbComp (CtxtSimView EK DK CT K sim.Aux leak.KeygenRand) := do
  let ((ekA, dkA), rand) ← leak.rkeygenAFreshRleak par
  let (ekAHat, dkAHat, aux) ← sim.rsimKeyA1 par ekA dkA
  if b = false then
    let (ekB, dkB) ← rkem.rkeygenBFresh par
    let (ctA, key, _) ← rkem.rencB par ekAHat dkB
    let (key', ekBHat) ← rkem.rdecA par dkAHat ctA ekB
    return (aux, rand, (ekAHat, dkAHat), ctA, (ekB, ekBHat), (key, key'))
  else
    let (ekBHat, _) ← rkem.rkeygenBUpdated par
    let (ctA, ekB, key, key') ← sim.rsimCtxtB par ekBHat ekAHat dkAHat
    return (aux, rand, (ekAHat, dkAHat), ctA, (ekB, ekBHat), (key, key'))

Ciphertext experiment

def ctxtSimExpA (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (sim : rkem.RatchetSimulator leak)
    (adversary : CtxtSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand) :
    ProbComp Bool := do
  let b ← $ᵗ Bool
  let par ← rkem.rsetup
  let x ← rkem.ctxtSimDistA sim par b
  let b' ← adversary par x
  return b == b'

Ciphertext advantage

noncomputable def ctxtSimAdvantageA (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversary : CtxtSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand) : ℝ :=
  |(Pr[= true | rkem.ctxtSimExpA sim adversary]).toReal - 1 / 2|

Ciphertext advantage, maximum over both parties

noncomputable def ctxtSimAdvantage (rkem : RKEMScheme ProbComp Par EK DK CT K)
    {leak : rkem.RandLeak} (sim : rkem.RatchetSimulator leak)
    (adversaryA adversaryB : CtxtSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand) : ℝ :=
  max (rkem.ctxtSimAdvantageA sim adversaryA) (rkem.ctxtSimAdvantageB sim adversaryB)

For each property \mathsf{X}\in\{\mathsf{KeyBaseSim},\mathsf{KeyUpdSim},\mathsf{CtxtSim}\} and party \mathsf{P}, the advantage of a distinguisher \adv is

\mathsf{Adv}^{\mathsf{X}\text{-}\mathsf{P}}(\adv)=\left|\Pr\left[b\sample\bit,\;x\sample\mathcal{D}^{\mathsf{X}}_{\mathsf{P},b},\;b'\sample\adv(x):b'=b\right]-\frac12\right|,\qquad \mathsf{Adv}^{\mathsf{X}}(\adv_\A,\adv_\B)=\max_{\mathsf{P}\in\{\A,\B\}}\mathsf{Adv}^{\mathsf{X}\text{-}\mathsf{P}}(\adv_\mathsf{P})

and the RKEM is \varepsilon-ratchet-simulatable when all three advantages are at most \varepsilon.

RatchetSimulatable

def RatchetSimulatable (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
    (ε : ℝ) : Prop :=
    ∃ (sim : rkem.RatchetSimulator leak),
    ∀ (baseA baseB : KeyBaseSimAdversary Par EK DK)
      (updA updB : KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand leak.EncRand)
      (ctxtA ctxtB : CtxtSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand),
    rkem.keyBaseSimAdvantage sim baseA baseB ≤ ε ∧
    rkem.keyUpdSimAdvantage sim updA updB ≤ ε ∧
    rkem.ctxtSimAdvantage sim ctxtA ctxtB ≤ ε

Lean code for Definition8.1.2●14 definitions

structure(7 fields)defined in SecureMessaging/RKEM/Defs.lean

complete

structure RKEMScheme.RatchetSimulator {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) (leak : rkem.RandLeak) :
  Type 1

structure RKEMScheme.RatchetSimulator
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  (leak : rkem.RandLeak) : Type 1

Ratchet simulators `(RSimKey-P₁, RSimKey-P₂, RSimCtxt-P)_{P ∈ {A,B}}` of
[TripleRatchet, Def. 5.5], for `rkem` with randomness-leak package `leak`. `Aux` is the
simulator's own auxiliary-state space, passed from `RSimKey-P₁` to `RSimKey-P₂`.

Fields

Aux : Type

Auxiliary state produced by `RSimKey-P₁` and consumed by `RSimKey-P₂`.

rsimKeyA1 : Par → EK → DK → ProbComp (EK × DK × self.Aux)

`RSimKey-A₁(par, ekA, dkA) → (ekÂ, dkÂ, aux)`: simulates `A`'s updated key pair from `A`'s
fresh key pair.

rsimKeyA2 : Par → EK → DK → self.Aux → ProbComp (CT × K × K × leak.EncRand)

`RSimKey-A₂(par, ekB̂, dkB̂, aux) → (ctB, K, K', rand₂)`: completes `A`'s round from `B`'s
updated key pair, producing the ciphertext to `B`, `A`'s and `B`'s shared keys, and coins
explaining `REnc-A`.

rsimCtxtA : Par → EK → EK → DK → ProbComp (CT × EK × K × K)

`RSimCtxt-A(par, ekÂ, ekB̂, dkB̂) → (ctB, ekA, K, K')`: simulates `A`'s ciphertext and
fresh encapsulation key from `A`'s updated encapsulation key and `B`'s updated key pair.

rsimKeyB1 : Par → EK → DK → ProbComp (EK × DK × self.Aux)

`RSimKey-B₁`: as `rsimKeyA1`, with the roles of `A` and `B` swapped.

rsimKeyB2 : Par → EK → DK → self.Aux → ProbComp (CT × K × K × leak.EncRand)

`RSimKey-B₂`: as `rsimKeyA2`, with the roles of `A` and `B` swapped.

rsimCtxtB : Par → EK → EK → DK → ProbComp (CT × EK × K × K)

`RSimCtxt-B`: as `rsimCtxtA`, with the roles of `A` and `B` swapped.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyBaseSimDistA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) :
  ProbComp (EK × DK)

def RKEMScheme.keyBaseSimDistA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (par : Par) (b : Bool) :
  ProbComp (EK × DK)

**Figure 10** (`D^KeyBaseSim_{A,b}`).

```
D_{A,0}:  (ekÂ, dkÂ) ← D̂_RKeyGen-A
D_{A,1}:  (ekA, dkA) ← D_RKeyGen-A,  (ekÂ, dkÂ, _) ← RSimKey-A₁(ekA, dkA)
return (ekÂ, dkÂ)
```

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyBaseSimExpA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary : RKEMScheme.KeyBaseSimAdversary Par EK DK) : ProbComp Bool

def RKEMScheme.keyBaseSimExpA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyBaseSimAdversary Par EK
      DK) :
  ProbComp Bool

Base-key-simulatability experiment for party `A`: `b ← {0,1}, x ← D^KeyBaseSim_{A,b},
b' ← 𝒜(x)`, returning `b = b'`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyUpdSimDistA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) :
  ProbComp
    (RKEMScheme.KeyUpdSimView EK DK CT K sim.Aux leak.KeygenRand
      leak.EncRand)

def RKEMScheme.keyUpdSimDistA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (par : Par) (b : Bool) :
  ProbComp
    (RKEMScheme.KeyUpdSimView EK DK CT K
      sim.Aux leak.KeygenRand
      leak.EncRand)

**Figure 11** (`D^KeyUpdSim_{A,b}`).

```
(ekB, dkB) ← D_RKeyGen-B{rand₀},  (ekB̂, dkB̂, aux₀) ← RSimKey-B₁(ekB, dkB),
(ekA, dkA) ← D_RKeyGen-A{rand₁},
D_{A,0}:  (ctB, K, dkÂ) ← REnc-A(ekB̂, dkA; rand₂),  (K', ekÂ) ← RDec-B(dkB̂, ctB, ekA)
D_{A,1}:  (ekÂ, dkÂ, aux₁) ← RSimKey-A₁(ekA, dkA),
          (ctB, K, K', rand₂) ← RSimKey-A₂(ekB̂, dkB̂, aux₁)
return ((ekB̂, dkB̂), (ekÂ, dkÂ), ctB, K, K', aux₀, rand₀, rand₁, rand₂)
```

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyUpdSimExpA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ProbComp Bool

def RKEMScheme.keyUpdSimExpA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyUpdSimAdversary Par EK
      DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ProbComp Bool

Updated-key-simulatability experiment for party `A`: `b ← {0,1}, x ← D^KeyUpdSim_{A,b},
b' ← 𝒜(x)`, returning `b = b'`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.ctxtSimDistB {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak) (par : Par) (b : Bool) :
  ProbComp (RKEMScheme.CtxtSimView EK DK CT K sim.Aux leak.KeygenRand)

def RKEMScheme.ctxtSimDistB
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (par : Par) (b : Bool) :
  ProbComp
    (RKEMScheme.CtxtSimView EK DK CT K
      sim.Aux leak.KeygenRand)

**Figure 12** (`D^CtxtSim_{B,b}`).

```
(ekA, dkA) ← D_RKeyGen-A{rand},  (ekÂ, dkÂ, aux) ← RSimKey-A₁(ekA, dkA),
D_{B,0}:  (ekB, dkB) ← D_RKeyGen-B,
          (ctA, K, dkB̂) ← REnc-B(ekÂ, dkB),  (K', ekB̂) ← RDec-A(dkÂ, ctA, ekB)
D_{B,1}:  (ekB̂, dkB̂) ← D̂_RKeyGen-B,  (ctA, ekB, K, K') ← RSimCtxt-B(ekB̂, ekÂ, dkÂ)
return (aux, rand, (ekÂ, dkÂ), ctA, (ekB, ekB̂), (K, K'))
```

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.ctxtSimExpA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.CtxtSimAdversary Par EK DK CT K sim.Aux
      leak.KeygenRand) :
  ProbComp Bool

def RKEMScheme.ctxtSimExpA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.CtxtSimAdversary Par EK DK
      CT K sim.Aux leak.KeygenRand) :
  ProbComp Bool

Ciphertext-simulatability experiment for party `A`: `b ← {0,1}, x ← D^CtxtSim_{A,b},
b' ← 𝒜(x)`, returning `b = b'`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyBaseSimAdvantageA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary : RKEMScheme.KeyBaseSimAdversary Par EK DK) : ℝ

def RKEMScheme.keyBaseSimAdvantageA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyBaseSimAdversary Par EK
      DK) :
  ℝ

`Adv^{KeyBaseSim-A}`: `|Pr[keyBaseSimExpA = true] - 1/2|`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyBaseSimAdvantage {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB : RKEMScheme.KeyBaseSimAdversary Par EK DK) : ℝ

def RKEMScheme.keyBaseSimAdvantage
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB :
    RKEMScheme.KeyBaseSimAdversary Par EK
      DK) :
  ℝ

`Adv^{KeyBaseSim} := max_{P ∈ {A,B}} Adv^{KeyBaseSim-P}`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyUpdSimAdvantageA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ℝ

def RKEMScheme.keyUpdSimAdvantageA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.KeyUpdSimAdversary Par EK
      DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ℝ

`Adv^{KeyUpdSim-A}`: `|Pr[keyUpdSimExpA = true] - 1/2|`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.keyUpdSimAdvantage {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB :
    RKEMScheme.KeyUpdSimAdversary Par EK DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ℝ

def RKEMScheme.keyUpdSimAdvantage
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB :
    RKEMScheme.KeyUpdSimAdversary Par EK
      DK CT K sim.Aux leak.KeygenRand
      leak.EncRand) :
  ℝ

`Adv^{KeyUpdSim} := max_{P ∈ {A,B}} Adv^{KeyUpdSim-P}`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.ctxtSimAdvantageA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.CtxtSimAdversary Par EK DK CT K sim.Aux
      leak.KeygenRand) :
  ℝ

def RKEMScheme.ctxtSimAdvantageA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversary :
    RKEMScheme.CtxtSimAdversary Par EK DK
      CT K sim.Aux leak.KeygenRand) :
  ℝ

`Adv^{CtxtSim-A}`: `|Pr[ctxtSimExpA = true] - 1/2|`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.ctxtSimAdvantage {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB :
    RKEMScheme.CtxtSimAdversary Par EK DK CT K sim.Aux
      leak.KeygenRand) :
  ℝ

def RKEMScheme.ctxtSimAdvantage
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak}
  (sim : rkem.RatchetSimulator leak)
  (adversaryA adversaryB :
    RKEMScheme.CtxtSimAdversary Par EK DK
      CT K sim.Aux leak.KeygenRand) :
  ℝ

`Adv^{CtxtSim} := max_{P ∈ {A,B}} Adv^{CtxtSim-P}`.

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.RatchetSimulatable {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K) {leak : rkem.RandLeak}
  (ε : ℝ) : Prop

def RKEMScheme.RatchetSimulatable
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  {leak : rkem.RandLeak} (ε : ℝ) : Prop

**Definition 5.5** (Ratchet simulatability). An RKEM `rkem` is `ε`-ratchet-simulatable with
respect to `leak` if there exists a family of simulators `sim` such that, for every choice of
distinguishers:

- the base-key simulatability advantage is at most `ε`;
- the updated-key simulatability advantage is at most `ε`;
- the ciphertext simulatability advantage is at most `ε`.

Each advantage is the maximum over parties `A` and `B`.

Definition8.1.3

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1used by 1✓L∃∀N

\todo

def securityExpA (rkem : RKEMScheme ProbComp Par EK DK CT K)
    (adversary : FSINDCPAAdversary Par EK DK CT K) [SampleableType K] : ProbComp Bool := do
  let b ← $ᵗ Bool
  let k1 ← $ᵗ K
  let par ← rkem.rsetup
  let (ekA, dkA) ← rkem.rkeygenAFresh par
  let (ekBHat, dkBHat) ← rkem.rkeygenBUpdated par
  let (ctB, k0, dkAHat) ← rkem.rencA par ekBHat dkA
  let (_, ekAHat) ← rkem.rdecB par dkBHat ctB ekA
  let b' ← adversary par ekA ekAHat ekBHat ctB dkAHat (if b then k1 else k0)
  return b == b'

Lean code for Definition8.1.3●1 definition

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.securityExpA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K)
  (adversary : RKEMScheme.FSINDCPAAdversary Par EK DK CT K)
  [SampleableType K] : ProbComp Bool

def RKEMScheme.securityExpA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  (adversary :
    RKEMScheme.FSINDCPAAdversary Par EK DK
      CT K)
  [SampleableType K] : ProbComp Bool

**Definition 5.4** (FS-IND-CPA experiment, party `A`).

```
b ← {0,1}, K1 ← $K,
(ekA, dkA) ← D_RKeyGen-A, (ek̂B, dk̂B) ← D̂_RKeyGen-B,
(ctB, K0, dk̂A) ← REnc-A(par, ek̂B, dkA),
(·, ek̂A) ← RDec-B(par, dk̂B, ctB, ekA),
b' ← A(ekA, ek̂A, ek̂B, ctB, dk̂A, K_b)
```
returning `b = b'`.

Definition8.1.4

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1used by 1✓L∃∀N

\todo

noncomputable def fsIndCpaAdvantageA (rkem : RKEMScheme ProbComp Par EK DK CT K)
    (adversary : FSINDCPAAdversary Par EK DK CT K) [SampleableType K] : ℝ :=
  |(Pr[= true | rkem.securityExpA adversary]).toReal - 1 / 2|

Lean code for Definition8.1.4●1 definition

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.fsIndCpaAdvantageA {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K)
  (adversary : RKEMScheme.FSINDCPAAdversary Par EK DK CT K)
  [SampleableType K] : ℝ

def RKEMScheme.fsIndCpaAdvantageA
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  (adversary :
    RKEMScheme.FSINDCPAAdversary Par EK DK
      CT K)
  [SampleableType K] : ℝ

`Adv^{FS-IND-CPA-A}`: `|Pr[securityExpA = true] - 1/2|`.

Definition8.1.5

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1used by 1✓L∃∀N

\todo

noncomputable def fsIndCpaAdvantage (rkem : RKEMScheme ProbComp Par EK DK CT K)
    (adversaryA adversaryB : FSINDCPAAdversary Par EK DK CT K) [SampleableType K] : ℝ :=
  max (rkem.fsIndCpaAdvantageA adversaryA) (rkem.fsIndCpaAdvantageB adversaryB)

Lean code for Definition8.1.5●1 definition

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.fsIndCpaAdvantage {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K)
  (adversaryA adversaryB : RKEMScheme.FSINDCPAAdversary Par EK DK CT K)
  [SampleableType K] : ℝ

def RKEMScheme.fsIndCpaAdvantage
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  (adversaryA adversaryB :
    RKEMScheme.FSINDCPAAdversary Par EK DK
      CT K)
  [SampleableType K] : ℝ

`Adv^{FS-IND-CPA} := max_{P ∈ {A,B}} Adv^{FS-IND-CPA-P}`.

Definition8.1.6

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1

Used by 5

Reverse dependency previews

Preview

Theorem 8.3.3

Loading preview

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

✓L∃∀N

GitHub#178

\todo

def FSINDCPASecure (rkem : RKEMScheme ProbComp Par EK DK CT K)
    (adversaryA adversaryB : FSINDCPAAdversary Par EK DK CT K) (epsilon : ℝ) [SampleableType K] :
    Prop :=
  rkem.fsIndCpaAdvantage adversaryA adversaryB ≤ epsilon

Lean code for Definition8.1.6●1 definition

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.FSINDCPASecure {Par EK DK CT K : Type}
  (rkem : RKEMScheme ProbComp Par EK DK CT K)
  (adversaryA adversaryB : RKEMScheme.FSINDCPAAdversary Par EK DK CT K)
  (epsilon : ℝ) [SampleableType K] : Prop

def RKEMScheme.FSINDCPASecure
  {Par EK DK CT K : Type}
  (rkem :
    RKEMScheme ProbComp Par EK DK CT K)
  (adversaryA adversaryB :
    RKEMScheme.FSINDCPAAdversary Par EK DK
      CT K)
  (epsilon : ℝ) [SampleableType K] : Prop

**Definition 5.4** (FS-IND-CPA security). `rkem` is `epsilon`-FS-IND-CPA-secure against
`adversaryA`, `adversaryB` if both per-party advantages are at most `epsilon`. Asymptotic
FS-IND-CPA security, as stated in [TripleRatchet], additionally quantifies this over every PPT
adversary and requires `epsilon` to be negligible in the security parameter.

Definition8.1.7

Group: Ratcheting Key Encapsulation Mechanism (RKEM). (6)

Group member previews

Preview

Definition 8.1.1

Loading preview

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

uses 1

Used by 6

Reverse dependency previews

Preview

Theorem 8.2.2

Loading preview

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

✓L∃∀N

GitHub#177

\todo

def deltaCorrect (rkem : RKEMScheme m Par EK DK CT K) (runtime : ProbCompRuntime m)
    (deltaCorr : ℝ≥0∞) (deltaDist : ℝ≥0∞) [DecidableEq K] : Prop :=
  rkem.deltaCorrectUpdatedKeys runtime deltaCorr ∧ rkem.deltaCloseUpdateKeyDist runtime deltaDist

Lean code for Definition8.1.7●1 definition

defdefined in SecureMessaging/RKEM/Defs.lean

complete

def RKEMScheme.deltaCorrect.{u, u_1} {m : Type → Type u} [Monad m]
  {Par EK DK CT K : Type} (rkem : RKEMScheme m Par EK DK CT K)
  (runtime : ProbCompRuntime m) (deltaCorr deltaDist : ENNReal)
  [DecidableEq K] : Prop

def RKEMScheme.deltaCorrect.{u, u_1}
  {m : Type → Type u} [Monad m]
  {Par EK DK CT K : Type}
  (rkem : RKEMScheme m Par EK DK CT K)
  (runtime : ProbCompRuntime m)
  (deltaCorr deltaDist : ENNReal)
  [DecidableEq K] : Prop

**Definition 5.3** (Correctness). `rkem` is `(deltaCorr, deltaDist)`-correct if it
satisfies both correctness with updated keys (`deltaCorrectUpdatedKeys`) and correctness of
the update-key distribution (`deltaCloseUpdateKeyDist`).