8.4. RKEM from KEM
Definition8.4.1
uses 1
✓L∃∀N
Associated Lean declarations
-
kemRKEM.scheme[complete] -
kemRKEM.rencRleak[complete] -
kemRKEM.randLeak[complete]
\todo
fresh/updated ratcheting key generation
def rkeygen {m : Type → Type u} [Monad m] {K PK SK C : Type}
(kem : KEMScheme m K PK SK C) : Unit → m (PK × SK) :=
fun _ => kem.keygenencapsulation
def renc {m : Type → Type u} [Monad m] {K PK SK C : Type}
(kem : KEMScheme m K PK SK C) (_par : Unit) (ekPeer : PK) (_dkSelf : SK) :
m ((PK × C) × K × SK) := do
let (ct, key) ← kem.encaps ekPeer
let (ekSelfHat, dkSelfHat) ← kem.keygen
return ((ekSelfHat, ct), key, dkSelfHat)decapsulation
def rdec {m : Type → Type u} [Monad m] {K PK SK C : Type}
(kem : KEMScheme m K PK SK C) (total : TotalDecaps kem)
(_par : Unit) (dkSelfHat : SK) (ctSelf : PK × C) (_ekPeer : PK) :
m (K × PK) := do
let (ekPeerHat, ct) := ctSelf
-- We have that kem.decaps dkSelfHat ct = some <$> decapsTotal dkSelfHat ct
let key ← total.decapsTotal dkSelfHat ct
return (key, ekPeerHat)generic RKEM scheme
def scheme {m : Type → Type u} [Monad m] {K PK SK C : Type}
(kem : KEMScheme m K PK SK C) (total : TotalDecaps kem) :
RKEMScheme m Unit PK SK (PK × C) K where
rsetup := pure ()
rkeygenAFresh := rkeygen kem
rkeygenAUpdated := rkeygen kem
rkeygenBFresh := rkeygen kem
rkeygenBUpdated := rkeygen kem
rencA := renc kem
rdecA := rdec kem total
rencB := renc kem
rdecB := rdec kem total
Security notions that expose algorithm coins are stated relative to a randomness-leak package of the RKEM. For this construction it is built from one of the underlying KEM: fresh key generation leaks the coins of \KeyGen, and \REnc\text{-}\mathsf{P}, which runs \Enc and then \KeyGen, leaks the pair of their coins.
Leaking encapsulation
def rencRleak {kem : KEMScheme m K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit)
(ekPeer : PK) (_dkSelf : SK) : m (((PK × C) × K × SK) × kemLeak.Rand) := do
let ((ct, key), encRand) ← kemLeak.encapsRleak ekPeer
let ((ekSelfHat, dkSelfHat), keygenRand) ← kemLeak.keygenRleak
return (((ekSelfHat, ct), key, dkSelfHat), (encRand, keygenRand))Randomness-leak package
def randLeak (kem : KEMScheme m K PK SK C) (total : TotalDecaps kem) (kemLeak : kem.RandLeak) :
(scheme kem total).RandLeak where
KeygenRand := kemLeak.KeygenRand
EncRand := kemLeak.Rand
rkeygenAFreshRleak := fun _ => kemLeak.keygenRleak
rkeygenBFreshRleak := fun _ => kemLeak.keygenRleak
rencARleak := rencRleak kemLeak
rencBRleak := rencRleak kemLeak
rkeygenAFresh_fst := fun _ => kemLeak.keygen_fst
rkeygenBFresh_fst := fun _ => kemLeak.keygen_fst
rencA_fst := rencRleak_fst kemLeak
rencB_fst := rencRleak_fst kemLeakLean code for Definition8.4.1●3 definitions
Associated Lean declarations
-
kemRKEM.scheme[complete]
-
kemRKEM.rencRleak[complete]
-
kemRKEM.randLeak[complete]
Associated Lean declarations
-
kemRKEM.scheme[complete] -
kemRKEM.rencRleak[complete] -
kemRKEM.randLeak[complete]
-
defdefined in SecureMessaging/RKEM/FromKEM/Construction.leancomplete
def kemRKEM.scheme.{u} {m : Type → Type u} [Monad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) (total : kem.TotalDecaps) : RKEMScheme m Unit PK SK (PK × C) K
def kemRKEM.scheme.{u} {m : Type → Type u} [Monad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) (total : kem.TotalDecaps) : RKEMScheme m Unit PK SK (PK × C) K
Generic RKEM scheme induced by a KEM ([TripleRatchet, Appendix A.1, Fig. 26]). Public parameters are vacuous; the ratcheting key spaces are the KEM's own key spaces, with fresh and updated distributions coinciding; ciphertexts bundle a freshly generated public key with the underlying KEM ciphertext. Requires a witness `total` that `kem`'s decapsulation is total, matching `RKEMScheme`'s decapsulation algorithms, which never fail. The encapsulation and decapsulation algorithms are the same for `A` and `B`.
-
defdefined in SecureMessaging/RKEM/FromKEM/Construction.leancomplete
def kemRKEM.rencRleak.{u} {m : Type → Type u} [Monad m] {K PK SK C : Type} {kem : KEMScheme m K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit) (ekPeer : PK) (_dkSelf : SK) : m (((PK × C) × K × SK) × kemLeak.Rand)
def kemRKEM.rencRleak.{u} {m : Type → Type u} [Monad m] {K PK SK C : Type} {kem : KEMScheme m K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit) (ekPeer : PK) (_dkSelf : SK) : m (((PK × C) × K × SK) × kemLeak.Rand)
KEM-RKEM encapsulation `REnc-P` (`renc`), also returning its coins: the coins of the KEM encapsulation `Enc(êkP̄)` followed by those of the fresh key generation `KeyGen()`. P̄ above corresponds to Peer below, while P corresponds to Self.
-
defdefined in SecureMessaging/RKEM/FromKEM/Construction.leancomplete
def kemRKEM.randLeak.{u} {m : Type → Type u} [Monad m] [LawfulMonad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RandLeak
def kemRKEM.randLeak.{u} {m : Type → Type u} [Monad m] [LawfulMonad m] {K PK SK C : Type} (kem : KEMScheme m K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RandLeak
Randomness-leak package of the RKEM-from-KEM construction, built from a randomness-leak package `kemLeak` of the underlying KEM. Fresh key generation `RKeyGen-P(par, ⊥)` is KEM key generation and leaks its coins; `REnc-P` leaks the coins of its KEM encapsulation and of its fresh key generation (`rencRleak`). As for the construction itself, both parties coincide.
Theorem8.4.2
\todo
theorem deltaCorrect [DecidableEq K] (kem : KEMScheme ProbComp K PK SK C)
(total : TotalDecaps kem) (δ : ℝ≥0∞) (hkem : kem.deltaCorrect ProbCompRuntime.probComp δ) :
RKEMScheme.deltaCorrect (scheme kem total) ProbCompRuntime.probComp δ 0Lean code for Theorem8.4.2●1 theorem
Associated Lean declarations
-
kemRKEM.deltaCorrect[complete]
Associated Lean declarations
-
kemRKEM.deltaCorrect[complete]
-
theoremdefined in SecureMessaging/RKEM/FromKEM/Correctness.leancomplete
theorem kemRKEM.deltaCorrect {K PK SK C : Type} [DecidableEq K] (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (δ : ENNReal) (hkem : kem.deltaCorrect ProbCompRuntime.probComp δ) : (kemRKEM.scheme kem total).deltaCorrect ProbCompRuntime.probComp δ 0
theorem kemRKEM.deltaCorrect {K PK SK C : Type} [DecidableEq K] (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (δ : ENNReal) (hkem : kem.deltaCorrect ProbCompRuntime.probComp δ) : (kemRKEM.scheme kem total).deltaCorrect ProbCompRuntime.probComp δ 0
**Quantitative correctness** (Def. 5.3) of the RKEM-from-KEM construction: if the underlying KEM is `δ`-correct, the construction is `(δ, 0)`-correct — the update-key-distribution error is exactly zero regardless of `δ`, by `evalDist_ratchetRoundOutputA_eq_evalDist_keygen`; only the `K = K'` error inherits `δ` from the underlying KEM.
Theorem8.4.3
\todo
IND-CPA reduction adversary
def indCpaReduction (kem : KEMScheme ProbComp K PK SK C)
(adversary : RKEMScheme.FSINDCPAAdversary Unit PK SK (PK × C) K) :
kem.IND_CPA_Adversary where
State := PK
preChallenge := fun ekBHat => pure ekBHat
postChallenge := fun ekBHat ct kb => do
let (ekA, _dkA) ← kem.keygen
let (ekAHat, dkAHat) ← kem.keygen
let b' ← adversary () ekA ekAHat ekBHat (ekAHat, ct) dkAHat kb
return !b'FS-IND-CPA security
theorem FSINDCPASecure (kem : KEMScheme ProbComp K PK SK C) (total : TotalDecaps kem)
(ε : ℝ)
(hcpa : ∀ adv : kem.IND_CPA_Adversary,
kem.IND_CPA_Advantage ProbCompRuntime.probComp adv ≤ ε)
(adversaryA adversaryB : RKEMScheme.FSINDCPAAdversary Unit PK SK (PK × C) K) :
RKEMScheme.FSINDCPASecure (scheme kem total) adversaryA adversaryB (ε / 2)Lean code for Theorem8.4.3●1 theorem
Associated Lean declarations
-
kemRKEM.FSINDCPASecure[complete]
Associated Lean declarations
-
kemRKEM.FSINDCPASecure[complete]
-
theoremdefined in SecureMessaging/RKEM/FromKEM/Security.leancomplete
theorem kemRKEM.FSINDCPASecure {K PK SK C : Type} [SampleableType K] (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (ε : ℝ) (hcpa : ∀ (adv : kem.IND_CPA_Adversary), KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp adv ≤ ε) (adversaryA adversaryB : RKEMScheme.FSINDCPAAdversary Unit PK SK (PK × C) K) : (kemRKEM.scheme kem total).FSINDCPASecure adversaryA adversaryB (ε / 2)
theorem kemRKEM.FSINDCPASecure {K PK SK C : Type} [SampleableType K] (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (ε : ℝ) (hcpa : ∀ (adv : kem.IND_CPA_Adversary), KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp adv ≤ ε) (adversaryA adversaryB : RKEMScheme.FSINDCPAAdversary Unit PK SK (PK × C) K) : (kemRKEM.scheme kem total).FSINDCPASecure adversaryA adversaryB (ε / 2)
**FS-IND-CPA security** (Def. 5.4) of the RKEM-from-KEM construction: if the underlying KEM is `ε`-IND-CPA-secure, uniformly over every adversary, the construction is FS-IND-CPA-secure at `ε / 2`. The `/ 2` is a convention conversion, not a loss; see the module docstring.
Theorem8.4.4
used by 0✓L∃∀N
Associated Lean declarations
-
kemRKEM.rsimKey1[complete] -
kemRKEM.rsimKey2[complete] -
kemRKEM.rsimCtxt[complete] -
kemRKEM.ratchetSimulator[complete] -
kemRKEM.RatchetSimulatable[complete]
Adapted from Dodis et al. (2025), Theorem A.2 and Figure 27.
The RKEM from KEM is perfectly ratchet simulatable: with the simulators below, the real and simulated distributions of base-key, updated-key and ciphertext simulatability coincide, so every distinguisher has advantage 0. This holds for any KEM whose decapsulation is total, which the construction itself already requires, with no correctness or security assumption.
Perfect ratchet simulatability
theorem RatchetSimulatable (kem : KEMScheme ProbComp K PK SK C) (total : TotalDecaps kem)
(kemLeak : kem.RandLeak) :
(scheme kem total).RatchetSimulatable (leak := randLeak kem total kemLeak) 0Ratchet simulatability is stated relative to the construction's randomness-leak package, built from one of the underlying KEM (see the RKEM from KEM construction).
The simulators are the same for both parties \mathsf{P}\in\{\A,\B\}, with peer \mathsf{\bar P}. They follow Figure 27 of the paper, with the changes marked in comments, which make the simulation perfect: as printed, \RSimCtxt\text{-}\mathsf{P} reuses \ekh{P} as the fresh key \ek_\mathsf{P}, which the real distribution samples independently, and \RSimKey\text{-}\mathsf{P}_2 returns K twice, which would require a perfectly correct KEM. The figure also returns the outputs of \RSimKey\text{-}\mathsf{P}_1 in a different order.
\RSimKey\text{-}\mathsf{P}_1(\ek_\mathsf{P},\dk_\mathsf{P})
\begin{array}{l}
(\ekh{P},\dkh{P})\sample\KeyGen(1^\lambda;\rand) \\
\aux_1:=(\ekh{P},\rand) \\
\Return(\ekh{P},\dkh{P},\aux_1)
\end{array}
RSimKey-P₁
def rsimKey1 {kem : KEMScheme ProbComp K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit)
(_ekSelf : PK) (_dkSelf : SK) : ProbComp (PK × SK × (PK × kemLeak.KeygenRand)) := do
let ((ekSelfHat, dkSelfHat), rand) ← kemLeak.keygenRleak
return (ekSelfHat, dkSelfHat, (ekSelfHat, rand))\RSimKey\text{-}\mathsf{P}_2(\ekh{\bar P},\dkh{\bar P},\aux_1)
\begin{array}{l}
\textbf{parse}\;(\ekh{P},\rand)\gets\aux_1 \\
(\ct,K)\sample\Enc(\ekh{\bar P};\rand') \\
K'\gets\Dec(\dkh{\bar P},\ct) \\
\ct_{\mathsf{\bar P}}:=(\ekh{P},\ct) \\
\rand_2:=(\rand',\rand)\pcomment{\text{Fig. 27: }(\aux_1,\rand')} \\
\Return(\ct_{\mathsf{\bar P}},K,K',\rand_2)\pcomment{\text{Fig. 27: }K\text{ for }K'}
\end{array}
RSimKey-P₂
def rsimKey2 {kem : KEMScheme ProbComp K PK SK C} (total : TotalDecaps kem)
(kemLeak : kem.RandLeak) (_par : Unit) (ekPeerHat : PK) (dkPeerHat : SK)
(aux : PK × kemLeak.KeygenRand) : ProbComp ((PK × C) × K × K × kemLeak.Rand) := do
let (ekSelfHat, rand) := aux
let ((ct, key), rand') ← kemLeak.encapsRleak ekPeerHat
let key' ← total.decapsTotal dkPeerHat ct
return ((ekSelfHat, ct), key, key', (rand', rand))\RSimCtxt\text{-}\mathsf{P}(\ekh{P},\ekh{\bar P},\dkh{\bar P})
\begin{array}{l}
(\ct,K)\sample\Enc(\ekh{\bar P}) \\
K'\gets\Dec(\dkh{\bar P},\ct) \\
\ct_{\mathsf{\bar P}}:=(\ekh{P},\ct) \\
(\ek_\mathsf{P},\_)\sample\KeyGen(1^\lambda)\pcomment{\text{Fig. 27: }\ek_\mathsf{P}:=\ekh{P}} \\
\Return(\ct_{\mathsf{\bar P}},\ek_\mathsf{P},K,K')
\end{array}
RSimCtxt-P
def rsimCtxt (kem : KEMScheme ProbComp K PK SK C) (total : TotalDecaps kem) (_par : Unit)
(ekSelfHat ekPeerHat : PK) (dkPeerHat : SK) : ProbComp ((PK × C) × PK × K × K) := do
let (ct, key) ← kem.encaps ekPeerHat
let key' ← total.decapsTotal dkPeerHat ct
let (ekSelf, _) ← kem.keygen
return ((ekSelfHat, ct), ekSelf, key, key')Ratchet simulators
def ratchetSimulator (kem : KEMScheme ProbComp K PK SK C) (total : TotalDecaps kem)
(kemLeak : kem.RandLeak) :
(scheme kem total).RatchetSimulator (randLeak kem total kemLeak) where
Aux := PK × kemLeak.KeygenRand
rsimKeyA1 := rsimKey1 kemLeak
rsimKeyA2 := rsimKey2 total kemLeak
rsimCtxtA := rsimCtxt kem total
rsimKeyB1 := rsimKey1 kemLeak
rsimKeyB2 := rsimKey2 total kemLeak
rsimCtxtB := rsimCtxt kem totalLean code for Theorem8.4.4●5 declarations
Associated Lean declarations
-
kemRKEM.rsimKey1[complete]
-
kemRKEM.rsimKey2[complete]
-
kemRKEM.rsimCtxt[complete]
-
kemRKEM.ratchetSimulator[complete]
-
kemRKEM.RatchetSimulatable[complete]
Associated Lean declarations
-
kemRKEM.rsimKey1[complete] -
kemRKEM.rsimKey2[complete] -
kemRKEM.rsimCtxt[complete] -
kemRKEM.ratchetSimulator[complete] -
kemRKEM.RatchetSimulatable[complete]
-
defdefined in SecureMessaging/RKEM/FromKEM/RatchetSimulatability.leancomplete
def kemRKEM.rsimKey1 {K PK SK C : Type} {kem : KEMScheme ProbComp K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit) (_ekSelf : PK) (_dkSelf : SK) : ProbComp (PK × SK × PK × kemLeak.KeygenRand)
def kemRKEM.rsimKey1 {K PK SK C : Type} {kem : KEMScheme ProbComp K PK SK C} (kemLeak : kem.RandLeak) (_par : Unit) (_ekSelf : PK) (_dkSelf : SK) : ProbComp (PK × SK × PK × kemLeak.KeygenRand)
`RSimKey-P₁` of [TripleRatchet, Fig. 27]: RSimKey-P₁(ekP, dkP): -- ekP, dkP are unused (êkP, d̂kP) ← KeyGen(1^λ; rand) aux₁ := (êkP, rand) return (êkP, d̂kP, aux₁) The simulated updated key pair is a fresh KEM key pair, as `REnc-P` itself would produce.
-
defdefined in SecureMessaging/RKEM/FromKEM/RatchetSimulatability.leancomplete
def kemRKEM.rsimKey2 {K PK SK C : Type} {kem : KEMScheme ProbComp K PK SK C} (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) (_par : Unit) (ekPeerHat : PK) (dkPeerHat : SK) (aux : PK × kemLeak.KeygenRand) : ProbComp ((PK × C) × K × K × kemLeak.Rand)
def kemRKEM.rsimKey2 {K PK SK C : Type} {kem : KEMScheme ProbComp K PK SK C} (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) (_par : Unit) (ekPeerHat : PK) (dkPeerHat : SK) (aux : PK × kemLeak.KeygenRand) : ProbComp ((PK × C) × K × K × kemLeak.Rand)
`RSimKey-P₂` of [TripleRatchet, Fig. 27]: RSimKey-P₂(êkP̄, d̂kP̄, aux₁): parse (êkP, rand) ← aux₁ (ct, K) ← Enc(êkP̄; rand') K' ← Dec(d̂kP̄, ct) ctP̄ := (êkP, ct) rand₂ := (rand', rand) return (ctP̄, K, K', rand₂) P̄ above corresponds to Peer below, while P corresponds to Self. The figure returns `K` in place of `K'` and sets `rand₂ := (aux₁, rand')`; see the module docstring.
-
defdefined in SecureMessaging/RKEM/FromKEM/RatchetSimulatability.leancomplete
def kemRKEM.rsimCtxt {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (_par : Unit) (ekSelfHat ekPeerHat : PK) (dkPeerHat : SK) : ProbComp ((PK × C) × PK × K × K)
def kemRKEM.rsimCtxt {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (_par : Unit) (ekSelfHat ekPeerHat : PK) (dkPeerHat : SK) : ProbComp ((PK × C) × PK × K × K)
`RSimCtxt-P` of [TripleRatchet, Fig. 27]: RSimCtxt-P(êkP, êkP̄, d̂kP̄): (ct, K) ←$ Enc(êkP̄) K' ← Dec(d̂kP̄, ct) ctP̄ := (êkP, ct) (ekP, ·) ← KeyGen(1^λ) return (ctP̄, ekP, K, K') P̄ above corresponds to Peer below, while P corresponds to Self. The figure sets `ekP := êkP` instead of sampling a fresh `ekP`; see the module docstring.
-
defdefined in SecureMessaging/RKEM/FromKEM/RatchetSimulatability.leancomplete
def kemRKEM.ratchetSimulator {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RatchetSimulator (kemRKEM.randLeak kem total kemLeak)
def kemRKEM.ratchetSimulator {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RatchetSimulator (kemRKEM.randLeak kem total kemLeak)
The ratchet simulators of [TripleRatchet, Fig. 27] for the RKEM-from-KEM construction, with respect to `randLeak`. The auxiliary state `aux₁ = (êkP, rand)` is the simulated updated encapsulation key and its key-generation coins. As for the construction itself, the simulators are the same for `A` and `B`.
-
theoremdefined in SecureMessaging/RKEM/FromKEM/RatchetSimulatability.leancomplete
theorem kemRKEM.RatchetSimulatable {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RatchetSimulatable 0
theorem kemRKEM.RatchetSimulatable {K PK SK C : Type} (kem : KEMScheme ProbComp K PK SK C) (total : kem.TotalDecaps) (kemLeak : kem.RandLeak) : (kemRKEM.scheme kem total).RatchetSimulatable 0
**Theorem A.2** ([TripleRatchet]) of the RKEM-from-KEM construction: it is perfectly (`ε = 0`) ratchet simulatable (Def. 5.5) with respect to `randLeak`, witnessed by the simulators `ratchetSimulator` of [TripleRatchet, Fig. 27]. Holds for any KEM with total decapsulation (`total`, already required by the construction), with no correctness or security assumption.