Secure Messaging

8.2. RKEM from DDH (non-FS)🔗

Definition8.2.1
Group: RKEM from DDH (non-FS). (2)
Group member previews
Preview
Theorem 8.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
GitHub#66

Adapted from Dodis et al. (2025), Appendix A.3 and Figure 28, without the figure's forward-secure modifications.

\textsf{Notation and public parameters}

\begin{array}{ll} G=\langle g\rangle & \text{cyclic group of prime order } q \\ \mathsf{par}=() & \text{vacuous public parameters} \\ (\ek_\mathsf{P},\dk_\mathsf{P})=(g^x,x)\in G\times\mathbb{Z}_q & \text{key pair; fresh and updated key generation coincide} \\ \ct=() & \text{empty ciphertext} \\ K=g^{xy}\in G & \text{shared key, for key pairs }(g^x,x)\text{ and }(g^y,y) \end{array}

Ciphertexts are empty: the sender's public value g^x doubles as the KEM ciphertext and as its encapsulation key, which the generic CKA construction transmits alongside the ciphertext and \RDec\text{-}\mathsf{P} receives as \ek_{\mathsf{\bar P}}. Used in the generic CKA construction, this RKEM yields the Double Ratchet CKA of Alwen et al. (2019) (see CKA from DDH).

The scheme is the non-forward-secure special case of an RKEM: \REnc\text{-}\mathsf{P} returns its input \dk_\mathsf{P} unchanged as the updated decapsulation key, and \RDec\text{-}\mathsf{P} returns its input \ek_{\mathsf{\bar P}} unchanged as the peer's updated encapsulation key. In particular, it is not FS-IND-CPA secure, since the forward-security game hands the adversary \dkh{A}=x together with \ekh{B}=Y, from which it recomputes K=Y^x; the paper only claims plain IND-CPA security under DDH (Theorem A.4).

Both parties run the same algorithms, shown below for one round in each direction, with \A's key pair (g^x,x) on the left and \B's key pair (g^y,y) on the right. In Lean, the group is modelled additively as a module over the scalar field F (playing \mathbb{Z}_q) with a fixed generator \mathsf{gen}, given as a parameter of the construction: g^x is x • gen and Y^x is x • Y.

Key generation.

\mathsf{RKeyGen}\text{-}\A(\mathsf{par},\mathsf{mode})

\begin{array}{l} x\sample\mathbb{Z}_q \\ (\ekA,\dkA)\gets(g^x,x) \\ \Return(\ekA,\dkA) \end{array}

\mathsf{RKeyGen}\text{-}\B(\mathsf{par},\mathsf{mode})

\begin{array}{l} y\sample\mathbb{Z}_q \\ (\ek_\B,\dk_\B)\gets(g^y,y) \\ \Return(\ek_\B,\dk_\B) \end{array}

Round \A\to\B.

\REnc\text{-}\A(\ekh{B}:=Y,\dkA:=x)

\begin{array}{l} \ct_\B:=()\pcomment{\text{empty ciphertext}} \\ K:=Y^x\pcomment{=g^{xy}} \\ \dkh{A}:=x \\ \Return(\ct_\B,K,\dkh{A}) \end{array}

\RDec\text{-}\B(\dkh{B}:=y,\ct_\B,\ekA:=X)

\begin{array}{l} K:=X^y\pcomment{=g^{xy}} \\ \ekh{A}:=X \\ \Return(K,\ekh{A}) \end{array}

Round \B\to\A.

\RDec\text{-}\A(\dkh{A}:=x,\ct_\A,\ek_\B:=Y)

\begin{array}{l} K:=Y^x\pcomment{=g^{xy}} \\ \ekh{B}:=Y \\ \Return(K,\ekh{B}) \end{array}

\REnc\text{-}\B(\ekh{A}:=X,\dk_\B:=y)

\begin{array}{l} \ct_\A:=()\pcomment{\text{empty ciphertext}} \\ K:=X^y\pcomment{=g^{xy}} \\ \dkh{B}:=y \\ \Return(\ct_\A,K,\dkh{B}) \end{array}

In Lean, both parties run the same rkeygen, renc and rdec.

RKeyGen-P

def rkeygen (gen : G) (_par : Unit) : ProbComp (G × F) := do let x ← $ᵗ F return (x • gen, x)

REnc-P

def renc (_par : Unit) (ekPeerHat : G) (dkSelf : F) : ProbComp (Unit × G × F) := do let ctPeer := () let key := dkSelf • ekPeerHat let dkSelfHat := dkSelf return (ctPeer, key, dkSelfHat)

RDec-P

def rdec (_par : Unit) (dkSelfHat : F) (_ctSelf : Unit) (ekPeer : G) : ProbComp (G × G) := do let key := dkSelfHat • ekPeer let ekPeerHat := ekPeer return (key, ekPeerHat)

DH RKEM scheme

def scheme (gen : G) : RKEMScheme ProbComp Unit G F Unit G where rsetup := pure () rkeygenAFresh := rkeygen gen rkeygenAUpdated := rkeygen gen rkeygenBFresh := rkeygen gen rkeygenBUpdated := rkeygen gen rencA := renc rdecA := rdec rencB := renc rdecB := rdec

Security notions that expose algorithm coins are stated relative to a randomness-leak package of the RKEM. For this construction, fresh key generation leaks the sampled scalar x, from which the key pair (g^x,x) is computed, and \REnc\text{-}\mathsf{P}, which is deterministic, leaks empty coins.

Leaking key generation

def rkeygenRleak (gen : G) (_par : Unit) : ProbComp ((G × F) × F) := do let x ← $ᵗ F return ((x • gen, x), x)

Leaking encapsulation

def rencRleak (par : Unit) (ekPeerHat : G) (dkSelf : F) : ProbComp ((Unit × G × F) × Unit) := do let out ← renc par ekPeerHat dkSelf return (out, ())

Randomness-leak package

def randLeak (gen : G) : (scheme (F := F) gen).RandLeak where KeygenRand := F EncRand := Unit rkeygenAFreshRleak := rkeygenRleak gen rkeygenBFreshRleak := rkeygenRleak gen rencARleak := rencRleak rencBRleak := rencRleak rkeygenAFresh_fst := rkeygenRleak_fst gen rkeygenBFresh_fst := rkeygenRleak_fst gen rencA_fst := rencRleak_fst rencB_fst := rencRleak_fst
Lean code for Definition8.2.1●7 definitions
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.rkeygen {F : Type} [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G) (_par : Unit) :
  ProbComp (G × F)
    def ddhRKEM.rkeygen {F : Type} [Field F]
  [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G)
  (_par : Unit) : ProbComp (G × F)
    Fresh/updated ratcheting key generation for the DH construction: both distributions
coincide, sampling `x ←$ F` and returning `(x • gen, x)`.

RKeyGen-P(par, mode):
  x ←$ ℤ_q
  (ekP, dkP) ← (g^x, x)
  return (ekP, dkP)
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.renc {F : Type} [Field F] {G : Type} [AddCommGroup G]
  [Module F G] (_par : Unit) (ekPeerHat : G) (dkSelf : F) :
  ProbComp (Unit × G × F)
    def ddhRKEM.renc {F : Type} [Field F]
  {G : Type} [AddCommGroup G] [Module F G]
  (_par : Unit) (ekPeerHat : G)
  (dkSelf : F) : ProbComp (Unit × G × F)
    DH-RKEM encapsulation. The ciphertext is empty, the shared key is `dkSelf • ekPeerHat`, and
the "updated" decapsulation key is `dkSelf` itself.

REnc-P(êkP̄ := Y, dkP := x):
  ctP̄ := ()
  K   := Y^x
  d̂kP := x
  return (ctP̄, K, d̂kP)

P̄ above corresponds to Peer below, while P corresponds to Self.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.rdec {F : Type} [Field F] {G : Type} [AddCommGroup G]
  [Module F G] (_par : Unit) (dkSelfHat : F) (_ctSelf : Unit)
  (ekPeer : G) : ProbComp (G × G)
    def ddhRKEM.rdec {F : Type} [Field F]
  {G : Type} [AddCommGroup G] [Module F G]
  (_par : Unit) (dkSelfHat : F)
  (_ctSelf : Unit) (ekPeer : G) :
  ProbComp (G × G)
    DH-RKEM decapsulation. The ciphertext is ignored, the shared key is `dkSelfHat • ekPeer`,
and the "updated" peer encapsulation key is `ekPeer` itself.

RDec-P(d̂kP := x, ctP, ekP̄ := Y):
  K   := Y^x
  êkP̄ := Y
  return (K, êkP̄)

P̄ above corresponds to Peer below, while P corresponds to Self.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.scheme {F : Type} [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G) :
  RKEMScheme ProbComp Unit G F Unit G
    def ddhRKEM.scheme {F : Type} [Field F]
  [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G]
  (gen : G) :
  RKEMScheme ProbComp Unit G F Unit G
    Non-forward-secure Diffie-Hellman RKEM ([TripleRatchet, Appendix A.3, Fig. 28]) over a module
`Module F G` with generator `gen : G`. Public parameters are vacuous; encapsulation keys are group
elements, decapsulation keys are scalars, ciphertexts are empty and shared keys are group
elements. Fresh and updated key generation coincide, since Fig. 28's `RKeyGen-P` ignores its mode,
and `REnc-P`/`RDec-P` leave the keys unchanged ([TripleRatchet, Remark 5.2]).

The encapsulation and decapsulation algorithms are the same for `A` and `B`.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.rkeygenRleak {F : Type} [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G) (_par : Unit) :
  ProbComp ((G × F) × F)
    def ddhRKEM.rkeygenRleak {F : Type} [Field F]
  [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G)
  (_par : Unit) : ProbComp ((G × F) × F)
    DH-RKEM fresh key generation `RKeyGen-P(par, ⊥)` (`rkeygen`), also returning its coins: the
sampled scalar `x` itself, from which the key pair `(x • gen, x)` is computed.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.rencRleak {F : Type} [Field F] {G : Type} [AddCommGroup G]
  [Module F G] (par : Unit) (ekPeerHat : G) (dkSelf : F) :
  ProbComp ((Unit × G × F) × Unit)
    def ddhRKEM.rencRleak {F : Type} [Field F]
  {G : Type} [AddCommGroup G] [Module F G]
  (par : Unit) (ekPeerHat : G)
  (dkSelf : F) :
  ProbComp ((Unit × G × F) × Unit)
    DH-RKEM encapsulation `REnc-P` (`renc`), also returning its coins. `REnc-P` is deterministic,
so its coins are empty.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/Construction.lean
    complete
    def ddhRKEM.randLeak {F : Type} [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] (gen : G) :
  (ddhRKEM.scheme gen).RandLeak
    def ddhRKEM.randLeak {F : Type} [Field F]
  [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G]
  (gen : G) :
  (ddhRKEM.scheme gen).RandLeak
    Randomness-leak package of the DH RKEM. Fresh key generation `RKeyGen-P(par, ⊥)` leaks its
sampled scalar (`rkeygenRleak`), and the deterministic `REnc-P` leaks empty coins (`rencRleak`). As
for the construction itself, both parties coincide.
Theorem8.2.2
Group: RKEM from DDH (non-FS). (2)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 8.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
GitHub#67

Adapted from Dodis et al. (2025), Theorem A.3.

The non-forward-secure RKEM from DDH is perfectly correct, that is, (0,0)-correct in the sense of the RKEM correctness definition. Explicitly, for each party \mathsf{P}\in\{\A,\B\} with peer \mathsf{\bar P}, consider one round of the protocol from \mathsf{P} towards \mathsf{\bar P}:

\begin{array}{l} (\ek_\mathsf{P},\dk_\mathsf{P})\sample\DRKG{P},\quad (\ekh{\bar P},\dkh{\bar P})\sample\DRKGup{\bar P}, \\ (\ct_{\mathsf{\bar P}},K,\dkh{P})\gets\REnc\text{-}\mathsf{P}(\ekh{\bar P},\dk_\mathsf{P}),\quad (K',\ekh{P})\gets\RDec\text{-}\mathsf{\bar P}(\dkh{\bar P},\ct_{\mathsf{\bar P}},\ek_\mathsf{P}). \end{array}

Then:

  1. Correctness with updated keys: \Pr[K=K']=1.

  2. Correctness of the update-key distribution: the pair (\ekh{P},\dkh{P}) is distributed exactly as \DRKGup{P}.

Perfect correctness

theorem deltaCorrect [DecidableEq G] (gen : G) : RKEMScheme.deltaCorrect (scheme (F := F) gen) ProbCompRuntime.probComp 0 0
Lean code for Theorem8.2.2●3 theorems
  • theoremdefined in SecureMessaging/RKEM/FromDDHNonFS/Correctness.lean
    complete
    theorem ddhRKEM.probOutput_correctExpA_eq_one {F : Type} [Field F]
  [SampleableType F] {G : Type} [AddCommGroup G] [Module F G]
  [DecidableEq G] (gen : G) :
  Pr[= true | (ddhRKEM.scheme gen).correctExpA] = 1
    theorem ddhRKEM.probOutput_correctExpA_eq_one
  {F : Type} [Field F] [SampleableType F]
  {G : Type} [AddCommGroup G] [Module F G]
  [DecidableEq G] (gen : G) :
  Pr[= true |
      (ddhRKEM.scheme gen).correctExpA] =
    1
    In one round of the DH RKEM from `A` towards `B`, the two parties always agree on the shared
key: `x • (y • gen) = y • (x • gen)`, the paper's `g^{xy} = g^{yx}`.
  • theoremdefined in SecureMessaging/RKEM/FromDDHNonFS/Correctness.lean
    complete
    theorem ddhRKEM.evalDist_ratchetRoundOutputA_eq_evalDist_rkeygen {F : Type}
  [Field F] [SampleableType F] {G : Type} [AddCommGroup G] [Module F G]
  (gen : G) :
  ProbCompRuntime.probComp.evalDist
      (ddhRKEM.scheme gen).ratchetRoundOutputA =
    ProbCompRuntime.probComp.evalDist (ddhRKEM.rkeygen gen ())
    theorem ddhRKEM.evalDist_ratchetRoundOutputA_eq_evalDist_rkeygen
  {F : Type} [Field F] [SampleableType F]
  {G : Type} [AddCommGroup G] [Module F G]
  (gen : G) :
  ProbCompRuntime.probComp.evalDist
      (ddhRKEM.scheme
          gen).ratchetRoundOutputA =
    ProbCompRuntime.probComp.evalDist
      (ddhRKEM.rkeygen gen ())
    `ratchetRoundOutputA` at the DH RKEM has exactly the distribution of fresh key generation: the
updated pair it returns is `A`'s fresh pair itself, and `B`'s key pair is discarded.
  • theoremdefined in SecureMessaging/RKEM/FromDDHNonFS/Correctness.lean
    complete
    theorem ddhRKEM.deltaCorrect {F : Type} [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G] [DecidableEq G] (gen : G) :
  (ddhRKEM.scheme gen).deltaCorrect ProbCompRuntime.probComp 0 0
    theorem ddhRKEM.deltaCorrect {F : Type} [Field F]
  [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G]
  [DecidableEq G] (gen : G) :
  (ddhRKEM.scheme gen).deltaCorrect
    ProbCompRuntime.probComp 0 0
    **Perfect correctness** (Def. 5.3, [TripleRatchet, Thm. A.3]) of the non-forward-secure DH
RKEM: both the shared-key error and the update-key-distribution error are exactly zero.
Theorem8.2.3
Group: RKEM from DDH (non-FS). (2)
Group member previews
Preview
Definition 8.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 8.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
GitHub#68

Adapted from Dodis et al. (2025), Theorem A.5 and Figure 30.

Let (\RSimKey\text{-}\mathsf{P}_1,\RSimKey\text{-}\mathsf{P}_2,\RSimCtxt\text{-}\mathsf{P})_{\mathsf{P}\in\{\A,\B\}} be the simulators of Figure 30, given below. The non-forward-secure RKEM from DDH is perfectly ratchet simulatable with respect to these simulators, that is, 0-ratchet simulatable in the sense of the RKEM ratchet simulatability definition. Explicitly, for each property \mathsf{X}\in\{\mathsf{KeyBaseSim},\mathsf{KeyUpdSim},\mathsf{CtxtSim}\} and each party \mathsf{P}\in\{\A,\B\}, the real and simulated distributions are identical,

\mathcal{D}^{\mathsf{X}}_{\mathsf{P},0}=\mathcal{D}^{\mathsf{X}}_{\mathsf{P},1},

and consequently every distinguisher \adv has advantage \mathsf{Adv}^{\mathsf{X}\text{-}\mathsf{P}}(\adv)=0.

Perfect ratchet simulatability

theorem RatchetSimulatable (gen : G) : (scheme (F := F) gen).RatchetSimulatable (leak := randLeak gen) 0

Ratchet simulatability is stated relative to the construction's randomness-leak package (see the RKEM from DDH non-FS construction).

The simulators are the same for both parties \mathsf{P}\in\{\A,\B\}, with peer \mathsf{\bar P}. They follow Figure 30 of the paper, and the simulation is perfect as printed.

\RSimKey\text{-}\mathsf{P}_1(\ek_\mathsf{P}:=X,\dk_\mathsf{P}:=x)\quad\mathsf{P}\in\{\A,\B\}

\begin{array}{l} \aux_1:=x \\ \Return(X,x,\aux_1)\pcomment{\text{keys left unchanged, as by }\REnc\text{-}\mathsf{P}} \\ \pcommentline{\text{Fig. 30: }(x,X,\aux_1)} \end{array}

RSimKey-P₁

def rsimKey1 (_par : Unit) (ekSelf : G) (dkSelf : F) : ProbComp (G × F × F) := do let aux := dkSelf return (ekSelf, dkSelf, aux)
\RSimKey\text{-}\mathsf{P}_2(\ekh{\bar P}:=Y,\dkh{\bar P}:=y,\aux_1:=x)\quad\mathsf{P}\in\{\A,\B\}

\begin{array}{l} K:=Y^x\pcomment{=X^y=g^{xy}\text{, the peer's }K'} \\ \ct_{\mathsf{\bar P}}:=();\;\rand_2:=()\pcomment{\REnc\text{-}\mathsf{P}\text{ is deterministic}} \\ \Return(\ct_{\mathsf{\bar P}},K,K,\rand_2) \end{array}

RSimKey-P₂

def rsimKey2 (_par : Unit) (ekPeerHat : G) (_dkPeerHat : F) (aux : F) : ProbComp (Unit × G × G × Unit) := do let dkSelf := aux let key := dkSelf • ekPeerHat let ctPeer := () let rand₂ := () return (ctPeer, key, key, rand₂)
\RSimCtxt\text{-}\mathsf{P}(\ekh{P}:=X,\ekh{\bar P}:=Y,\dkh{\bar P}:=y)\quad\mathsf{P}\in\{\A,\B\}

\begin{array}{l} K:=X^y\pcomment{=g^{xy}} \\ \ct_{\mathsf{\bar P}}:=() \\ \Return(\ct_{\mathsf{\bar P}},X,K,K)\pcomment{\ek_\mathsf{P}:=\ekh{P}\text{, as }\RDec\text{-}\mathsf{\bar P}\text{ returns it}} \end{array}

RSimCtxt-P

def rsimCtxt (_par : Unit) (ekSelfHat _ekPeerHat : G) (dkPeerHat : F) : ProbComp (Unit × G × G × G) := do let key := dkPeerHat • ekSelfHat let ctPeer := () return (ctPeer, ekSelfHat, key, key)

Ratchet simulators

def ratchetSimulator (gen : G) : (scheme (F := F) gen).RatchetSimulator (randLeak gen) where Aux := F rsimKeyA1 := rsimKey1 rsimKeyA2 := rsimKey2 rsimCtxtA := rsimCtxt rsimKeyB1 := rsimKey1 rsimKeyB2 := rsimKey2 rsimCtxtB := rsimCtxt
Lean code for Theorem8.2.3●5 declarations
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/RatchetSimulatability.lean
    complete
    def ddhRKEM.rsimKey1 {F G : Type} (_par : Unit) (ekSelf : G) (dkSelf : F) :
  ProbComp (G × F × F)
    def ddhRKEM.rsimKey1 {F G : Type}
  (_par : Unit) (ekSelf : G)
  (dkSelf : F) : ProbComp (G × F × F)
    `RSimKey-P₁` of [TripleRatchet, Fig. 30]:

RSimKey-P₁(ekP := X, dkP := x):
  aux₁ := x
  return (X, x, aux₁)

The simulated updated key pair is `P`'s fresh key pair itself, as in the non-forward-secure
scheme. The figure returns `(x, X, aux₁)`; see the module docstring.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/RatchetSimulatability.lean
    complete
    def ddhRKEM.rsimKey2 {F : Type} [Field F] {G : Type} [AddCommGroup G]
  [Module F G] (_par : Unit) (ekPeerHat : G) (_dkPeerHat aux : F) :
  ProbComp (Unit × G × G × Unit)
    def ddhRKEM.rsimKey2 {F : Type} [Field F]
  {G : Type} [AddCommGroup G] [Module F G]
  (_par : Unit) (ekPeerHat : G)
  (_dkPeerHat aux : F) :
  ProbComp (Unit × G × G × Unit)
    `RSimKey-P₂` of [TripleRatchet, Fig. 30]:

RSimKey-P₂(êkP̄ := Y, d̂kP̄ := y, aux₁ := x):   -- d̂kP̄ is unused
K     := Y^x
ctP̄  := ()
rand₂ := ()
return (ctP̄, K, K, rand₂)

P̄ above corresponds to Peer below, while P corresponds to Self.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/RatchetSimulatability.lean
    complete
    def ddhRKEM.rsimCtxt {F : Type} [Field F] {G : Type} [AddCommGroup G]
  [Module F G] (_par : Unit) (ekSelfHat _ekPeerHat : G)
  (dkPeerHat : F) : ProbComp (Unit × G × G × G)
    def ddhRKEM.rsimCtxt {F : Type} [Field F]
  {G : Type} [AddCommGroup G] [Module F G]
  (_par : Unit) (ekSelfHat _ekPeerHat : G)
  (dkPeerHat : F) :
  ProbComp (Unit × G × G × G)
    `RSimCtxt-P` of [TripleRatchet, Fig. 30]:

RSimCtxt-P(êkP := X, êkP̄ := Y, d̂kP̄ := y):   -- êkP̄ is unused
K    := X^y
ctP̄ := ()
return (ctP̄, X, K, K)

P̄ above corresponds to Peer below, while P corresponds to Self.
  • defdefined in SecureMessaging/RKEM/FromDDHNonFS/RatchetSimulatability.lean
    complete
    def ddhRKEM.ratchetSimulator {F : Type} [Field F] [SampleableType F]
  {G : Type} [AddCommGroup G] [Module F G] (gen : G) :
  (ddhRKEM.scheme gen).RatchetSimulator (ddhRKEM.randLeak gen)
    def ddhRKEM.ratchetSimulator {F : Type}
  [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G]
  (gen : G) :
  (ddhRKEM.scheme gen).RatchetSimulator
    (ddhRKEM.randLeak gen)
    The ratchet simulators of [TripleRatchet, Fig. 30] for the non-forward-secure DH RKEM, with
respect to `randLeak`. The auxiliary state `aux₁ = x` is `P`'s decapsulation key. As for the
construction itself, the simulators are the same for `A` and `B`.
  • theoremdefined in SecureMessaging/RKEM/FromDDHNonFS/RatchetSimulatability.lean
    complete
    theorem ddhRKEM.RatchetSimulatable {F : Type} [Field F] [SampleableType F]
  {G : Type} [AddCommGroup G] [Module F G] (gen : G) :
  (ddhRKEM.scheme gen).RatchetSimulatable 0
    theorem ddhRKEM.RatchetSimulatable {F : Type}
  [Field F] [SampleableType F] {G : Type}
  [AddCommGroup G] [Module F G]
  (gen : G) :
  (ddhRKEM.scheme gen).RatchetSimulatable
    0
    **Theorem A.5** ([TripleRatchet]), non-forward-secure part: the non-forward-secure DH RKEM is
perfectly (`ε = 0`) ratchet simulatable (Def. 5.5) with respect to `randLeak`, witnessed by the
simulators `ratchetSimulator` of [TripleRatchet, Fig. 30]. Holds unconditionally.