KEM-DEM Hybrid Public Key Encryption

The Chained Symmetric Encryption worked example used a single primitive twice, with two reductions both aimed at the same assumption.

In this worked example we examine KEM-DEM hybrid public key encryption, which combines a key encapsulation mechanism (KEM) $K$ and a symmetric encryption scheme $E$ into a public key encryption scheme $\mathsf{KEMDEM}(K, E)$. To encrypt a message $m$ under a public key $\mathit{pk}$, the construction encapsulates a fresh shared secret $\mathit{ss}$ under $\mathit{pk}$ and then uses $\mathit{ss}$ as a one-time symmetric key to encrypt $m$. The ciphertext is:

$(c_{\mathsf{kem}}, c_{\mathsf{sym}}) \quad \text{ where } \quad (\mathit{ss}, c_{\mathsf{kem}}) \gets K.\mathsf{Encaps}(\mathit{pk}), \quad c_{\mathsf{sym}} \gets E.\mathsf{Enc}(\mathit{ss}, m)$

We prove that $\mathsf{KEMDEM}(K, E)$ satisfies CPA security, assuming that $K$ is CPA-secure, that $E$ satisfies one-time secrecy, and that $E$’s key generation algorithm produces keys uniformly distributed over its key space. The proof uses five reductions: two to KEM CPA security (one forward, one back), two to key uniformity of $E$ (one forward, one back), and one to one-time secrecy of $E$ in the middle.

This worked example introduces three patterns beyond chained encryption: multi-primitive composition (a KEM and a SymEnc combine into a PKE), reductions in opposite directions (the same assumption is invoked twice, once forward and once backward), and bridging between key distributions with a key-uniformity assumption.

The full proof is available at Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof.

---

• 1. What this proves
• 2. The primitives and the security games
  • Symmetric encryption primitive
  • One-time secrecy game (left/right)
  • Key uniformity game
  • KEM primitive
  • KEM CPA game
  • PKE primitive
  • PKE CPA game
• 3. The KEMDEM scheme
• 4. The proof structure
• 5. Reduction $R_1$: Game 0 → Game 1
• 6. Reduction $R_2$: Game 1 → Game 2
• 7. Reduction $R_3$: Game 2 → Game 3
• 8. Reduction $R_4$: Game 3 → Game 4
• 9. Reduction $R_5$: Game 4 → Game 5
• 10. The full games block
• 11. Verifying
• 12. Lessons learned
  • 13. Next steps

---

1. What this proves

KEM-DEM hybrid public key encryption is the standard construction that turns a key encapsulation mechanism (KEM) $K$ and a symmetric encryption scheme $E$ into a public key encryption (PKE) scheme $\mathsf{KEMDEM}(K, E)$. The KEM is used to establish a per-message shared secret under the recipient’s public key, and the symmetric scheme is then used to encrypt the actual message under that shared secret. The ciphertext is the pair $(c_{\mathsf{kem}}, c_{\mathsf{sym}})$. Decryption reverses this: decapsulate $c_{\mathsf{kem}}$ to recover the shared secret, then symmetrically decrypt $c_{\mathsf{sym}}$. The structural requirement is $K.\mathcal{S} \subseteq E.\mathcal{K}$ — the KEM’s shared secret space must be a subset of the symmetric encryption scheme’s key space — so that the shared secret can be used directly as a symmetric key.

The theorem proved here is: if $K$ is CPA-secure, $E$ has one-time secrecy (OTS), and $E$’s key generation algorithm produces uniformly distributed keys, then $\mathsf{KEMDEM}(K,E)$ is CPA-secure as a public key encryption scheme.

Why the key-uniformity assumption is needed. The KEMDEM scheme uses the KEM’s shared secret directly as the symmetric key — it never calls E.KeyGen(). But the one-time secrecy game for $E$ does call E.KeyGen() to sample its one-time key. So at the point where the proof wants to invoke one-time secrecy, the “symmetric key” in the current game is a uniform sample from the KEM’s shared secret space (which equals $E.\mathcal{K}$), while the OTS challenger samples its key via E.KeyGen(). These two distributions need to be lined up before the OTS assumption can be applied. The proof does this with a key-uniformity assumption: a small left/right game asserting that E.KeyGen() is indistinguishable from uniform sampling over E.Key. Two extra hops — one forward, one back — bridge the gap around the one-time secrecy hop.

Joy of Cryptography / Boneh-Shoup parallel. The KEM-DEM construction and its CPA-security proof appear in Mike Rosulek’s Joy of Cryptography and as Exercise 11.9 in Boneh and Shoup’s A Graduate Course in Applied Cryptography. The proof here follows the same game-hopping argument described in those references: replace the real KEM shared secret with a random key (using KEM CPA), switch the ciphertext from encrypting the left message to encrypting the right message (using SymEnc one-time secrecy), and then restore the real KEM shared secret (using KEM CPA again, in the reverse direction). ProofFrog mechanically verifies each hop of this argument.

---

2. The primitives and the security games

This proof involves three different cryptographic primitives — symmetric encryption $E$, key encapsulation $K$, and public key encryption $\mathsf{KEMDEM}(K,E)$ — each with its own security game, plus a small key-uniformity game on $E$. We recall all of them before looking at the construction.

Symmetric encryption primitive

A symmetric encryption scheme is, as in the chained encryption worked example, a triple of algorithms over a key space $\mathcal{K}$, message space $\mathcal{M}$, and ciphertext space $\mathcal{C}$:

$\begin{array}{l} \mathsf{KeyGen}: () \to \mathcal{K} \\ \mathsf{Enc}: \mathcal{K} \times \mathcal{M} \to \mathcal{C} \\ \mathsf{Dec}: \mathcal{K} \times \mathcal{C} \to \mathcal{M} \quad \text{(deterministic)} \end{array}$

Notice that Dec here is total ($\mathcal{M}$, not $\mathcal{M} \cup \{\bot\}$), reflecting the simplifying assumption that decryption never fails. This is a different primitive from the one used in the chained encryption example, so it has its own file. The FrogLang primitive file is Primitives/NonNullableSymEnc.primitive:

Primitive SymEnc(Set MessageSpace, Set CiphertextSpace, Set KeySpace) {
    Set Message = MessageSpace;
    Set Ciphertext = CiphertextSpace;
    Set Key = KeySpace;

    Key KeyGen();
    Ciphertext Enc(Key k, Message m);
    deterministic Message Dec(Key k, Ciphertext c);
}

Try it. From the examples/ directory, run proof_frog check Primitives/NonNullableSymEnc.primitive to type-check the primitive file, or open it in the web editor and click Type Check.

One-time secrecy game (left/right)

The one-time secrecy game used in this proof is phrased as a left/right indistinguishability game, in contrast to the real/random formulation used in the chained encryption worked example. The adversary submits two messages $m_L$ and $m_R$, and the challenger encrypts either $m_L$ (Left game) or $m_R$ (Right game) under a freshly sampled key. The adversary must guess which side it is interacting with. As in any “one-time” experiment, the key is sampled fresh on every oracle call via E.KeyGen():

$\begin{array}{l} \underline{\mathsf{Left}_E.\mathsf{Eavesdrop}(m_L, m_R)} \\ k \gets E.\mathsf{KeyGen}() \\ c \gets E.\mathsf{Enc}(k, m_L) \\ \text{return } c \end{array} \qquad \begin{array}{l} \underline{\mathsf{Right}_E.\mathsf{Eavesdrop}(m_L, m_R)} \\ k \gets E.\mathsf{KeyGen}() \\ c \gets E.\mathsf{Enc}(k, m_R) \\ \text{return } c \end{array}$

The FrogLang security game file is Games/SymEnc/INDOT.game:

import '../../Primitives/SymEnc.primitive';

Game Left(SymEnc E) {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        E.Key k = E.KeyGen();
        E.Ciphertext c = E.Enc(k, mL);
        return c;
    }
}

Game Right(SymEnc E) {
    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
        E.Key k = E.KeyGen();
        E.Ciphertext c = E.Enc(k, mR);
        return c;
    }
}

export as INDOT;

Try it. From the examples/ directory, run proof_frog check Games/SymEnc/INDOT.game, or open the file in the web editor and click Type Check.

Key uniformity game

The second assumption on $E$ is key uniformity: the distribution of keys produced by E.KeyGen() is indistinguishable from a uniform sample over E.Key. This is also phrased as a left/right game, with the two sides using the two sampling methods:

$\begin{array}{l} \underline{\mathsf{Real}_E.\mathsf{Challenge}()} \\ k \gets E.\mathsf{KeyGen}() \\ \text{return } k \end{array} \qquad \begin{array}{l} \underline{\mathsf{Random}_E.\mathsf{Challenge}()} \\ k \stackrel{\$}{\leftarrow} E.\mathcal{K} \\ \text{return } k \end{array}$

This assumption is the bridge that lets the proof cross from a “symmetric key sampled uniformly from $E.\mathcal{K}$” world to a “symmetric key generated by E.KeyGen()” world (which is what the OTS game uses). It will be invoked twice: once on each side of the OTS hop. The FrogLang security game file is Games/SymEnc/KeyUniformity.game:

import '../../Primitives/SymEnc.primitive';

Game Real(SymEnc E) {
    E.Key Challenge() {
        E.Key k = E.KeyGen();
        return k;
    }
}

Game Random(SymEnc E) {
    E.Key Challenge() {
        E.Key k <- E.Key;
        return k;
    }
}

export as KeyUniformity;

Try it. From the examples/ directory, run proof_frog check Games/SymEnc/KeyUniformity.game, or open the file in the web editor and click Type Check.

KEM primitive

A key encapsulation mechanism is a triple of algorithms over a public key space $\mathcal{PK}$, secret key space $\mathcal{SK}$, ciphertext space $\mathcal{C}$, and shared secret space $\mathcal{S}$:

$\begin{array}{l} \mathsf{KeyGen}: () \to \mathcal{PK} \times \mathcal{SK} \\ \mathsf{Encaps}: \mathcal{PK} \to \mathcal{S} \times \mathcal{C} \\ \mathsf{Decaps}: \mathcal{SK} \times \mathcal{C} \to \mathcal{S} \quad \text{(deterministic)} \end{array}$

Encaps produces a pair: a shared secret plus a ciphertext that travels to the recipient. Decaps recovers the shared secret given the ciphertext and the recipient’s secret key. This version assumes that decapsulation never fails. The FrogLang primitive file is Primitives/KEM.primitive:

Primitive KEM(Set SharedSecretSpace, Set CiphertextSpace, Set PKeySpace, Set SKeySpace) {
    Set SharedSecret = SharedSecretSpace;
    Set Ciphertext = CiphertextSpace;
    Set PublicKey = PKeySpace;
    Set SecretKey = SKeySpace;

    [PublicKey, SecretKey] KeyGen();
    [SharedSecret, Ciphertext] Encaps(PublicKey pk);
    deterministic SharedSecret Decaps(SecretKey sk, Ciphertext m);
}

Try it. From the examples/ directory, run proof_frog check Primitives/KEM.primitive, or open the file in the web editor and click Type Check.

KEM CPA game

CPA security for a KEM captures the indistinguishability of real and random shared secrets, given the corresponding KEM ciphertext. The adversary’s Initialize call returns the public key, and it may then call a Challenge oracle that returns a $(\mathit{ss}, c_{\mathsf{kem}})$ pair. In the Real game, $\mathit{ss}$ is the genuine shared secret produced by encapsulation. In the Random game, the ciphertext is still a genuine encapsulation but the shared secret is replaced by a fresh uniform sample, completely independent of $c_{\mathsf{kem}}$:

$\begin{array}{l} \underline{\mathsf{Initialize}()} \\ (\mathit{pk}, \mathit{sk}) \gets K.\mathsf{KeyGen}() \\ \text{return } \mathit{pk} \end{array} \qquad \begin{array}{l} \underline{\mathsf{Real}_K.\mathsf{Challenge}()} \\ (\mathit{ss}, c) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ \text{return } (\mathit{ss}, c) \end{array} \qquad \begin{array}{l} \underline{\mathsf{Random}_K.\mathsf{Challenge}()} \\ (\_, c) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ \mathit{ss} \stackrel{\$}{\leftarrow} K.\mathcal{S} \\ \text{return } (\mathit{ss}, c) \end{array}$

(Initialize is shared between both sides.) The FrogLang security game file is Games/KEM/INDCPA_MultiChal.game:

import '../../Primitives/KEM.primitive';

Game Real(KEM K) {
    K.PublicKey pk;
    K.SecretKey sk;

    K.PublicKey Initialize() {
        [K.PublicKey, K.SecretKey] k = K.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    [K.SharedSecret, K.Ciphertext] Challenge() {
        [K.SharedSecret, K.Ciphertext] rsp = K.Encaps(pk);
        K.SharedSecret ss = rsp[0];
        K.Ciphertext ctxt = rsp[1];
        return [ss, ctxt];
    }
}

Game Random(KEM K) {
    K.PublicKey pk;
    K.SecretKey sk;

    K.PublicKey Initialize() {
        [K.PublicKey, K.SecretKey] k = K.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    [K.SharedSecret, K.Ciphertext] Challenge() {
        [K.SharedSecret, K.Ciphertext] rsp = K.Encaps(pk);
        K.SharedSecret ss <- K.SharedSecret;
        K.Ciphertext ctxt = rsp[1];
        return [ss, ctxt];
    }
}

export as KEM_INDCPA_MultiChal;

Try it. From the examples/ directory, run proof_frog check Games/KEM/INDCPA_MultiChal.game, or open the file in the web editor and click Type Check.

PKE primitive

The public key encryption primitive is the goal of the construction: a triple of algorithms over a message space $\mathcal{M}$, ciphertext space $\mathcal{C}$, public key space $\mathcal{PK}$, and secret key space $\mathcal{SK}$:

$\begin{array}{l} \mathsf{KeyGen}: () \to \mathcal{PK} \times \mathcal{SK} \\ \mathsf{Enc}: \mathcal{PK} \times \mathcal{M} \to \mathcal{C} \\ \mathsf{Dec}: \mathcal{SK} \times \mathcal{C} \to \mathcal{M} \cup \{\bot\} \quad \text{(deterministic)} \end{array}$

The FrogLang primitive file is Primitives/PubKeyEnc.primitive:

Primitive PubKeyEnc(Set MessageSpace, Set CiphertextSpace, Set PKeySpace, Set SKeySpace) {
    Set Message = MessageSpace;
    Set Ciphertext = CiphertextSpace;
    Set PublicKey = PKeySpace;
    Set SecretKey = SKeySpace;

    [PublicKey, SecretKey] KeyGen();
    Ciphertext Enc(PublicKey pk, Message m);
    deterministic Message? Dec(SecretKey sk, Ciphertext m);
}

Try it. From the examples/ directory, run proof_frog check Primitives/PubKeyEnc.primitive, or open the file in the web editor and click Type Check.

PKE CPA game

The PKE CPA game is, like SymEnc one-time secrecy here, a left/right indistinguishability game. The adversary obtains the public key from Initialize and may call the Challenge(mL, mR) oracle multiple times — multi-message CPA — and each call returns either an encryption of $m_L$ or an encryption of $m_R$ under the long-term public key:

$\begin{array}{l} \underline{\mathsf{Initialize}()} \\ (\mathit{pk}, \mathit{sk}) \gets E.\mathsf{KeyGen}() \\ \text{return } \mathit{pk} \end{array} \qquad \begin{array}{l} \underline{\mathsf{Left}_E.\mathsf{Challenge}(m_L, m_R)} \\ \text{return } E.\mathsf{Enc}(\mathit{pk}, m_L) \end{array} \qquad \begin{array}{l} \underline{\mathsf{Right}_E.\mathsf{Challenge}(m_L, m_R)} \\ \text{return } E.\mathsf{Enc}(\mathit{pk}, m_R) \end{array}$

The FrogLang security game file is Games/PubKeyEnc/INDCPA_MultiChal.game:

import '../../Primitives/PubKeyEnc.primitive';

Game Left(PubKeyEnc E) {
    E.PublicKey pk;
    E.SecretKey sk;

    E.PublicKey Initialize() {
        [E.PublicKey, E.SecretKey] k = E.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    E.Ciphertext Challenge(E.Message mL, E.Message mR) {
        return E.Enc(pk, mL);
    }
}

Game Right(PubKeyEnc E) {
    E.PublicKey pk;
    E.SecretKey sk;

    E.PublicKey Initialize() {
        [E.PublicKey, E.SecretKey] k = E.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    E.Ciphertext Challenge(E.Message mL, E.Message mR) {
        return E.Enc(pk, mR);
    }
}

export as INDCPA_MultiChal;

Try it. From the examples/ directory, run proof_frog check Games/PubKeyEnc/INDCPA_MultiChal.game, or open the file in the web editor and click Type Check.

---

3. The KEMDEM scheme

$\mathsf{KEMDEM}(K, E)$ takes a KEM $K$ and a symmetric encryption scheme $E$ and produces a public key encryption scheme. Its key pair is $K$’s key pair, its messages come from $E$, and its ciphertexts are pairs of a KEM ciphertext and a symmetric ciphertext. It requires $K.\mathcal{S} \subseteq E.\mathcal{K}$ so that the KEM’s shared secret can serve directly as a symmetric key. In the proof we will further impose equality $K.\mathcal{S} = E.\mathcal{K}$ by binding both sets to the same Set variable in the proof’s let: block; see §4 below.

The sets needed for the scheme definition are:

$\begin{array}{l} \mathcal{PK} = K.\mathcal{PK}, \quad \mathcal{SK} = K.\mathcal{SK}, \quad \mathcal{M} = E.\mathcal{M}, \quad \mathcal{C} = K.\mathcal{C} \times E.\mathcal{C} \end{array}$

The algorithms comprising the scheme are:

$\begin{array}{l} \underline{\mathsf{KeyGen}()} \\ \text{return } K.\mathsf{KeyGen}() \end{array} \quad \begin{array}{l} \underline{\mathsf{Enc}(\mathit{pk}, m)} \\ (k_{\mathsf{sym}}, c_{\mathsf{kem}}) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ c_{\mathsf{sym}} \gets E.\mathsf{Enc}(k_{\mathsf{sym}}, m) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array} \quad \begin{array}{l} \underline{\mathsf{Dec}(\mathit{sk}, (c_{\mathsf{kem}}, c_{\mathsf{sym}}))} \\ k_{\mathsf{sym}} \gets K.\mathsf{Decaps}(\mathit{sk}, c_{\mathsf{kem}}) \\ \text{return } E.\mathsf{Dec}(k_{\mathsf{sym}}, c_{\mathsf{sym}}) \end{array}$

KeyGen simply delegates to the KEM. Enc encapsulates under the public key to produce the shared secret $k_{\mathsf{sym}}$ and KEM ciphertext $c_{\mathsf{kem}}$, then uses that shared secret directly as the DEM key to encrypt the message. Dec reverses the process. The FrogLang scheme file is Schemes/PubKeyEnc/HybridKEMDEM.scheme:

import '../../Primitives/KEM.primitive';
import '../../Primitives/NonNullableSymEnc.primitive';
import '../../Primitives/PubKeyEnc.primitive';

Scheme KEMDEM(KEM K, SymEnc E) extends PubKeyEnc {
    requires K.SharedSecret subsets E.Key;

    Set Message = E.Message;
    Set Ciphertext = [K.Ciphertext, E.Ciphertext];
    Set PublicKey = K.PublicKey;
    Set SecretKey = K.SecretKey;

    [PublicKey, SecretKey] KeyGen() {
        return K.KeyGen();
    }

    Ciphertext Enc(PublicKey pk, Message m) {
        [K.SharedSecret, K.Ciphertext] x = K.Encaps(pk);
        E.Key k_sym = x[0];
        K.Ciphertext c_kem = x[1];
        E.Ciphertext c_sym = E.Enc(k_sym, m);
        return [c_kem, c_sym];
    }

    deterministic Message? Dec(SecretKey sk, Ciphertext c) {
        K.Ciphertext c_kem = c[0];
        E.Ciphertext c_sym = c[1];
        K.SharedSecret k_sym = K.Decaps(sk, c_kem);
        return E.Dec(k_sym, c_sym);
    }
}

Try it. From the examples/ directory, run proof_frog check Schemes/PubKeyEnc/HybridKEMDEM.scheme, or open the file in the web editor and click Type Check.

Note that Dec returns Message? (nullable) because KEMDEM extends PubKeyEnc, whose primitive declares Dec as returning an optional type. The underlying NonNullableSymEnc primitive’s Dec returns plain Message (non-nullable), but the KEMDEM scheme’s Dec signature must match the PubKeyEnc primitive it extends.

The requires K.SharedSecret subsets E.Key; clause is an essential part of the entire construction. It states that the KEM’s shared secret space must be a subset of the SymEnc’s key space. Without it, the assignment E.Key k_sym = x[0]; in Enc would be a type error — x[0] has type K.SharedSecret, not E.Key. The requires clause makes the subtype relationship explicit, so the type checker can accept the code.

The ciphertext type [K.Ciphertext, E.Ciphertext] is a tuple. In FrogLang, [T1, T2] is the two-component product type, and components are accessed by constant index: c[0] is the KEM ciphertext, c[1] is the symmetric ciphertext.

---

4. The proof structure

The games: block lists twelve game steps, producing eleven hops. Five of those hops are assumption hops (one per reduction); the other six are interchangeability hops verified by the engine. Conceptually the proof moves through six games, which we’ll call $\mathsf{Game}_0$ through $\mathsf{Game}_5$:

• $\mathsf{Game}_0$ — the $\mathsf{KEMDEM}$ scheme encrypting the left message $m_L$ under the real KEM shared secret. This is INDCPA_MultiChal(KD).Left with the scheme inlined.
• $\mathsf{Game}_1$ — encrypting $m_L$ under a DEM key sampled uniformly from $K.\mathcal{S} = E.\mathcal{K}$, while the KEM ciphertext is still produced by a real Encaps call.
• $\mathsf{Game}_2$ — encrypting $m_L$ under a DEM key produced by E.KeyGen().
• $\mathsf{Game}_3$ — encrypting the right message $m_R$ under a DEM key produced by E.KeyGen().
• $\mathsf{Game}_4$ — encrypting $m_R$ under a DEM key sampled uniformly from $K.\mathcal{S}$.
• $\mathsf{Game}_5$ — encrypting $m_R$ under the real KEM shared secret. This is INDCPA_MultiChal(KD).Right with the scheme inlined.

Five reductions bridge these six games:

• $R_1$ (KEM CPA, $\mathsf{Game}_0 \to \mathsf{Game}_1$): reduces to KEM CPA security in the Real → Random direction. The shared secret starts as the genuine output of Encaps and becomes a fresh uniform sample.
• $R_2$ (KeyUniformity, $\mathsf{Game}_1 \to \mathsf{Game}_2$): reduces to key uniformity of $E$ in the Random → Real direction. The symmetric key distribution moves from uniform over $E.\mathcal{K}$ to the output of E.KeyGen().
• $R_3$ (OneTimeSecrecy, $\mathsf{Game}_2 \to \mathsf{Game}_3$): reduces to one-time secrecy of $E$. The encrypted message switches from $m_L$ to $m_R$ under a KeyGen-sampled key.
• $R_4$ (KeyUniformity, $\mathsf{Game}_3 \to \mathsf{Game}_4$): structurally identical to $R_2$ but encrypts $m_R$, and invokes key uniformity in the Real → Random direction.
• $R_5$ (KEM CPA, $\mathsf{Game}_4 \to \mathsf{Game}_5$): structurally identical to $R_1$ but encrypts $m_R$, and invokes KEM CPA in the Random → Real direction.

Reductions $R_1$ and $R_5$ both reduce to KEM CPA security, but they invoke it in opposite directions: $R_1$ goes Real → Random, $R_5$ goes Random → Real. Similarly $R_2$ and $R_4$ invoke key uniformity in opposite directions. Both directions of each assumption are valid because indistinguishability is symmetric: if no adversary can distinguish the two sides in one direction, no adversary can distinguish them in the other.

This proof file does not write out explicit intermediate game definitions. Each conceptual $\mathsf{Game}_i$ appears in the games: list only as a composed form — either AssumptionGame compose Reduction or as an inlined side of INDCPA_MultiChal(KD). The engine verifies the interchangeability hops by canonicalizing the adjacent composed forms directly. You can add these intermediate game definitions if you find it helpful; ProofFrog will check they match their neighbouring games.

The proof’s let: block binds $K.\mathcal{S}$ and $E.\mathcal{K}$ to the same Set variable (KEMSharedSecretSpace), imposing the equality $K.\mathcal{S} = E.\mathcal{K}$ that the proof relies on whenever a uniform sample from one side must match a uniform sample from the other.

---

5. Reduction $R_1$: Game 0 → Game 1

The first reduction adapts a $\mathsf{CPA}(\mathsf{KEMDEM}(K,E))$ adversary so that it can play against a $\mathsf{CPAKEM}(K)$ challenger. It has no key pair of its own — all key material comes from the challenger. Its Challenge oracle delegates to challenger.Challenge() to obtain a $(k_{\mathsf{sym}}, c_{\mathsf{kem}})$ pair, then uses $k_{\mathsf{sym}}$ as the symmetric key to encrypt the left message:

$\begin{array}{l} \underline{R_1.\mathsf{Challenge}(m_L, m_R)} \\ (k_{\mathsf{sym}}, c_{\mathsf{kem}}) \gets \mathsf{challenger}.\mathsf{Challenge}() \\ c_{\mathsf{sym}} \gets E.\mathsf{Enc}(k_{\mathsf{sym}}, m_L) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array}$

Note that $R_1$ has no Initialize method of its own: the compose machinery automatically forwards Initialize from the outer game to the inner KEM_INDCPA_MultiChal(K) challenger, so the challenger’s Initialize — which generates the KEM key pair and returns pk — becomes the Initialize of the composed game.

When the external challenger is $\mathsf{Real}_K$, $k_{\mathsf{sym}}$ is the genuine shared secret produced by Encaps, and $R_1 \circ \mathsf{Real}_K$ produces the same distribution as $\mathsf{Game}_0$: the $\mathsf{KEMDEM}$ scheme encrypting $m_L$ under a real shared secret. When the challenger switches to $\mathsf{Random}_K$, $k_{\mathsf{sym}}$ becomes a uniformly random sample from $K.\mathcal{S}$, independent of $c_{\mathsf{kem}}$, and $R_1 \circ \mathsf{Random}_K$ produces the same distribution as $\mathsf{Game}_1$.

In FrogLang:

// Reduction for hop from Game 0 to Game 1
// - Reduction to CPA security of the KEM. The reduction uses the shared secret
//   from the KEM CPA challenger, which is either real (= Game 0) or random (= Game 1).
Reduction R1(SymEnc E, KEM K, KEMDEM KD) compose KEM_INDCPA_MultiChal(K) against INDCPA_MultiChal(KD).Adversary {
    KD.Ciphertext Challenge(KD.Message mL, KD.Message mR) {
        [K.SharedSecret, K.Ciphertext] y = challenger.Challenge();
        K.SharedSecret k_sym = y[0];
        K.Ciphertext c_kem = y[1];
        E.Ciphertext c_sym = E.Enc(k_sym, mL);
        return [c_kem, c_sym];
    }
}

Try it. $R_1$ lives inside HybridKEMDEM_INDCPA_MultiChal.proof along with the rest of the proof. From the examples/ directory, run proof_frog prove Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof to verify the whole proof, or open the file in the web editor and click Run Proof. See §11 Verifying for the expected output.

Notice that $R_1$ has no state fields: all key material lives inside the $\mathsf{CPAKEM}(K)$ challenger that $R_1$ composes against. This contrasts with $R_2$ through $R_4$ below, which have to manage their own KEM key pair because they compose against a different challenger.

---

6. Reduction $R_2$: Game 1 → Game 2

After the assumption hop on KEM CPA, the proof is in a state where the symmetric key is a uniform sample from $K.\mathcal{S} = E.\mathcal{K}$. But the next hop — one-time secrecy of $E$ — will want the symmetric key to be the output of E.KeyGen() instead (because that’s what the OTS game’s challenger does internally). So we first bridge the two distributions with a key-uniformity hop.

$R_2$ composes against a $\mathsf{KeyUniformity}(E)$ challenger. It has no KEM challenger available — the $\mathsf{CPAKEM}(K)$ assumption was consumed in the previous hop — and so $R_2$ must generate the KEM key pair itself and answer Initialize queries from its own state. Its Challenge oracle encapsulates under its own public key to produce $c_{\mathsf{kem}}$ (discarding the shared secret), asks the KeyUniformity(E) challenger for a symmetric key, and uses that key to encrypt $m_L$:

$\begin{array}{l} \underline{R_2.\mathsf{Initialize}()} \\ (\mathit{pk}, \mathit{sk}) \gets K.\mathsf{KeyGen}() \\ \text{return } \mathit{pk} \end{array} \qquad \begin{array}{l} \underline{R_2.\mathsf{Challenge}(m_L, m_R)} \\ (\_, c_{\mathsf{kem}}) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ k_{\mathsf{sym}} \gets \mathsf{challenger}.\mathsf{Challenge}() \\ c_{\mathsf{sym}} \gets E.\mathsf{Enc}(k_{\mathsf{sym}}, m_L) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array}$

When the KeyUniformity(E) challenger is in $\mathsf{Random}$ mode, $k_{\mathsf{sym}}$ is a uniform sample from $E.\mathcal{K}$, which equals $K.\mathcal{S}$ (imposed by the proof’s let: block). So $R_2 \circ \mathsf{Random}$ matches $\mathsf{Game}_1$, which in turn matches $R_1 \circ \mathsf{Random}_K$ (the closing step of the previous pattern) under canonicalization. When the challenger switches to $\mathsf{Real}$ mode, $k_{\mathsf{sym}}$ is the output of E.KeyGen(), and $R_2 \circ \mathsf{Real}$ matches $\mathsf{Game}_2$.

In FrogLang:

// Reduction for hop from Game 1 to Game 2
// - Reduction to key uniformity of the symmetric encryption scheme. The reduction uses
//   the symmetric key from the key uniformity challenger, which is either real (= Game 2)
//   or random (= Game 1).
Reduction R2(SymEnc E, KEM K, KEMDEM KD) compose KeyUniformity(E) against INDCPA_MultiChal(KD).Adversary {
    K.PublicKey pk;
    K.SecretKey sk;

    K.PublicKey Initialize() {
        [K.PublicKey, K.SecretKey] k = K.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    KD.Ciphertext Challenge(KD.Message mL, KD.Message mR) {
        [K.SharedSecret, K.Ciphertext] x = K.Encaps(pk);
        K.SharedSecret k_sym = challenger.Challenge();
        K.Ciphertext c_kem = x[1];
        E.Ciphertext c_sym = E.Enc(k_sym, mL);
        return [c_kem, c_sym];
    }
}

This is a recurring pattern in multi-primitive proofs: a reduction that targets one assumption must internally simulate every other primitive that the surrounding game depends on. $R_2$ plays against a KeyUniformity(E) challenger but still needs a real KEM key pair — because the scheme under attack uses K.KeyGen() and K.Encaps() as part of its Enc algorithm — so $R_2$ generates that KEM key pair in its own Initialize.

---

7. Reduction $R_3$: Game 2 → Game 3

With the DEM key now distributed as E.KeyGen(), the proof is ready to invoke one-time secrecy of $E$. $R_3$ composes against an $\mathsf{OneTimeSecrecy}(E)$ challenger. Like $R_2$, it generates the KEM key pair in its own Initialize. Its Challenge oracle encapsulates to produce $c_{\mathsf{kem}}$ (discarding the shared secret), and asks the OTS(E) challenger to produce the DEM ciphertext on either $m_L$ or $m_R$ under a fresh key:

$\begin{array}{l} \underline{R_3.\mathsf{Initialize}()} \\ (\mathit{pk}, \mathit{sk}) \gets K.\mathsf{KeyGen}() \\ \text{return } \mathit{pk} \end{array} \qquad \begin{array}{l} \underline{R_3.\mathsf{Challenge}(m_L, m_R)} \\ (\_, c_{\mathsf{kem}}) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ c_{\mathsf{sym}} \gets \mathsf{challenger}.\mathsf{Eavesdrop}(m_L, m_R) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array}$

Crucially, $R_3$ discards the shared secret produced by Encaps and lets the OTS challenger sample its own fresh DEM key via E.KeyGen(). When the OTS challenger is in $\mathsf{Left}$ mode, the DEM ciphertext is an encryption of $m_L$ under a KeyGen-sampled key, matching $\mathsf{Game}_2$. When the OTS challenger is in $\mathsf{Right}$ mode, the DEM ciphertext is an encryption of $m_R$, matching $\mathsf{Game}_3$. This is the central hop of the whole proof — the point where the “which message is encrypted” bit actually flips.

In FrogLang:

// Reduction for hop from Game 2 to Game 3
// - Reduction to one-time secrecy of the symmetric encryption scheme. The reduction uses the
//   challenger to encrypt either mL (= Game 2) or mR (= Game 3).
Reduction R3(SymEnc E, KEM K, KEMDEM KD) compose INDOT(E) against INDCPA_MultiChal(KD).Adversary {
    K.PublicKey pk;
    K.SecretKey sk;

    K.PublicKey Initialize() {
        [K.PublicKey, K.SecretKey] k = K.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    KD.Ciphertext Challenge(KD.Message mL, KD.Message mR) {
        [K.SharedSecret, K.Ciphertext] x = K.Encaps(pk);
        K.Ciphertext c_kem = x[1];
        E.Ciphertext c_sym = challenger.Eavesdrop(mL, mR);
        return [c_kem, c_sym];
    }
}

---

8. Reduction $R_4$: Game 3 → Game 4

The rest of the proof “undoes” the earlier distributional bridges, but on the right-message side. $R_4$ is structurally identical to $R_2$ but encrypts $m_R$ instead of $m_L$, and the direction of the assumption flips: now the proof uses key uniformity to move back from “key from E.KeyGen()” to “key sampled uniformly from $E.\mathcal{K}$”.

$\begin{array}{l} \underline{R_4.\mathsf{Initialize}()} \\ (\mathit{pk}, \mathit{sk}) \gets K.\mathsf{KeyGen}() \\ \text{return } \mathit{pk} \end{array} \qquad \begin{array}{l} \underline{R_4.\mathsf{Challenge}(m_L, m_R)} \\ (\_, c_{\mathsf{kem}}) \gets K.\mathsf{Encaps}(\mathit{pk}) \\ k_{\mathsf{sym}} \gets \mathsf{challenger}.\mathsf{Challenge}() \\ c_{\mathsf{sym}} \gets E.\mathsf{Enc}(k_{\mathsf{sym}}, m_R) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array}$

When the KeyUniformity(E) challenger is in $\mathsf{Real}$ mode, $R_4 \circ \mathsf{Real}$ matches $\mathsf{Game}_3$ (closing the OTS pattern). When the challenger switches to $\mathsf{Random}$ mode, $R_4 \circ \mathsf{Random}$ matches $\mathsf{Game}_4$ (opening the closing KEM CPA pattern).

In FrogLang:

// Reduction for hop from Game 3 to Game 4
// - Reduction to key uniformity of the symmetric encryption scheme. The reduction uses
//   the symmetric key from the key uniformity challenger, which is either real (= Game 3)
//   or random (= Game 4).
Reduction R4(SymEnc E, KEM K, KEMDEM KD) compose KeyUniformity(E) against INDCPA_MultiChal(KD).Adversary {
    K.PublicKey pk;
    K.SecretKey sk;

    K.PublicKey Initialize() {
        [K.PublicKey, K.SecretKey] k = K.KeyGen();
        pk = k[0];
        sk = k[1];
        return pk;
    }

    KD.Ciphertext Challenge(KD.Message mL, KD.Message mR) {
        [K.SharedSecret, K.Ciphertext] x = K.Encaps(pk);
        K.SharedSecret k_sym = challenger.Challenge();
        K.Ciphertext c_kem = x[1];
        E.Ciphertext c_sym = E.Enc(k_sym, mR);
        return [c_kem, c_sym];
    }
}

---

9. Reduction $R_5$: Game 4 → Game 5

The fifth and final reduction is structurally identical to $R_1$ — it lets its composed $\mathsf{CPAKEM}(K)$ challenger supply the key pair and the $(k_{\mathsf{sym}}, c_{\mathsf{kem}})$ pair — but it encrypts $m_R$ instead of $m_L$:

$\begin{array}{l} \underline{R_5.\mathsf{Challenge}(m_L, m_R)} \\ (k_{\mathsf{sym}}, c_{\mathsf{kem}}) \gets \mathsf{challenger}.\mathsf{Challenge}() \\ c_{\mathsf{sym}} \gets E.\mathsf{Enc}(k_{\mathsf{sym}}, m_R) \\ \text{return } (c_{\mathsf{kem}}, c_{\mathsf{sym}}) \end{array}$

When the KEM challenger is in $\mathsf{Random}$ mode, $k_{\mathsf{sym}}$ is a random shared secret and $R_5 \circ \mathsf{Random}_K$ matches $\mathsf{Game}_4$. When the challenger switches to $\mathsf{Real}_K$, $k_{\mathsf{sym}}$ is the genuine shared secret and $R_5 \circ \mathsf{Real}_K$ matches $\mathsf{Game}_5$, which is in turn interchangeable with INDCPA_MultiChal(KD).Right.

This is the Random → Real direction of the KEM CPA assumption: the proof has finished using the random-key intermediate world and is restoring the real KEM shared secret, but on the right-message side. Both directions of the assumption are valid because indistinguishability is symmetric.

In FrogLang:

// Reduction for hop from Game 4 to Game 5
// - Reduction to CPA security of the KEM. The reduction uses the shared secret
//   from the KEM CPA challenger, which is either real (= Game 5) or random (= Game 4).
Reduction R5(SymEnc E, KEM K, KEMDEM KD) compose KEM_INDCPA_MultiChal(K) against INDCPA_MultiChal(KD).Adversary {
    KD.Ciphertext Challenge(KD.Message mL, KD.Message mR) {
        [K.SharedSecret, K.Ciphertext] y = challenger.Challenge();
        K.SharedSecret k_sym = y[0];
        K.Ciphertext c_kem = y[1];
        E.Ciphertext c_sym = E.Enc(k_sym, mR);
        return [c_kem, c_sym];
    }
}

---

10. The full games block

Putting all twelve game steps together, the games: section of HybridKEMDEM_INDCPA_MultiChal.proof reads:

games:
    // Game 0
    INDCPA_MultiChal(KD).Left against INDCPA_MultiChal(KD).Adversary;
    KEM_INDCPA_MultiChal(K).Real compose R1(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    // Game 1
    KEM_INDCPA_MultiChal(K).Random compose R1(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    KeyUniformity(E).Random compose R2(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    // Game 2
    KeyUniformity(E).Real compose R2(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    INDOT(E).Left compose R3(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    // Game 3
    INDOT(E).Right compose R3(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    KeyUniformity(E).Real compose R4(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    // Game 4
    KeyUniformity(E).Random compose R4(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    KEM_INDCPA_MultiChal(K).Random compose R5(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    // Game 5
    KEM_INDCPA_MultiChal(K).Real compose R5(E, K, KD) against INDCPA_MultiChal(KD).Adversary;
    INDCPA_MultiChal(KD).Right against INDCPA_MultiChal(KD).Adversary;

The twelve entries produce eleven hops. Five are assumption hops — one per reduction — at positions 2 → 3 ($R_1$, CPAKEM Real → Random), 4 → 5 ($R_2$, KeyUniformity Random → Real), 6 → 7 ($R_3$, OneTimeSecrecy Left → Right), 8 → 9 ($R_4$, KeyUniformity Real → Random), and 10 → 11 ($R_5$, CPAKEM Random → Real). The other six transitions (1 → 2, 3 → 4, 5 → 6, 7 → 8, 9 → 10, 11 → 12) are interchangeability hops verified by the engine.

Notice how each reduction occupies two consecutive entries in the games list — one for each side of the composed assumption game — and interchangeability hops connect adjacent reductions at their conceptual boundary $\mathsf{Game}_i$. The interchangeability hop at positions 3 → 4, for example, is the engine verifying that KEM_INDCPA_MultiChal(K).Random compose R1 and KeyUniformity(E).Random compose R2 both canonicalize to $\mathsf{Game}_1$, even though they get there via very different-looking source programs.

The full let:, assume:, and theorem: blocks, together with the five reductions above, complete the proof file, which you can find at Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof.

---

11. Verifying

Activate your Python virtual environment first if it is not already active in this terminal: source .venv/bin/activate on macOS/Linux (bash/zsh), source .venv/bin/activate.fish on fish, or .venv\Scripts\Activate.ps1 on Windows PowerShell. See Installation.

From the examples/ directory:

proof_frog prove Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof

Expected output:

Proof Succeeded!

The full step-by-step output shows 11 hops over 12 game steps: 6 interchangeability hops (verified by code canonicalization) and 5 assumption hops (one for each of $R_1$ through $R_5$).

In the web editor, open Proofs/PubKeyEnc/HybridKEMDEM_INDCPA_MultiChal.proof and click Run Proof. The output panel turns green with the same step-by-step report.

---

12. Lessons learned

• Multi-primitive composition. The proof reasons about three distinct primitives simultaneously — a KEM, a SymEnc, and a PKE — each with its own security game and its own type namespace. Reductions must carefully distinguish which primitive’s methods and sets they are invoking. The requires clause on the scheme is what makes the types align across primitive boundaries.

• Reductions in opposite directions. $R_1$ and $R_5$ both reduce to the same underlying assumption ($\mathsf{CPAKEM}(K)$), but $R_1$ invokes it in the Real → Random direction and $R_5$ invokes it in the Random → Real direction. Similarly, $R_2$ and $R_4$ invoke key uniformity in opposite directions. Both directions are valid because indistinguishability is symmetric. This “go-and-come-back” pattern often comes up in security proofs: here we use the KEM assumption to move into a world with a random key, do the message-switching argument, then use the same KEM assumption to move back out. Neither direction is privileged; the same security game serves both roles.

• Bridging distributions with a key-uniformity assumption. The KEMDEM scheme never calls E.KeyGen() — it uses the KEM’s shared secret directly as the symmetric key — while the one-time secrecy game for $E$ does call E.KeyGen(). These two key distributions aren’t always identical, so the proof needs a key-uniformity assumption (that “E.KeyGen() is indistinguishable from uniform sampling over E.Key”) to bridge them. The bridge is invoked symmetrically — once on each side of the OTS hop — which is why there are five reductions instead of three.

• Generic construction parameter handling. The $\mathsf{KEMDEM}$ scheme is parameterized by $(K, E)$, and the proof is parameterized by the same values in its let: block. Every reduction carries (E, K, KD) as parameters. This is how ProofFrog proves theorems about generic constructions rather than concrete instantiations: the proof holds for any choice of $K$ and $E$ satisfying the stated assumptions and the $K.\mathcal{S} = E.\mathcal{K}$ constraint.

• Proofs without explicit intermediate games. Unlike proofs that write out each $\mathsf{Game}_i$ as a standalone Game definition, this proof keeps its intermediate games implicit — every entry in the games: list is either a side of INDCPA_MultiChal(KD) or a compose expression. The engine verifies the interchangeability hops by canonicalizing adjacent composed forms directly. This keeps the proof file shorter, at the cost of making each conceptual game only visible in the reader’s head (or in the line comments that label them). You can add them if you want, or you can use the web editor’s game hop detail view to see what the intermediate games are.

---

13. Next steps

This concludes the tutorial and worked examples section of the ProofFrog manual. From here you have a few options:

• Build your own proof! You now have the tools to start modelling your own ideas in ProofFrog.
• Explore the examples catalogue to see other examples of cryptographic schemes and proofs modelled in ProofFrog.
• Read the language reference to dive deeper into FrogLang.
• Since ProofFrog is a new tool and is targeted at introduction proofs, it’s important to understand the limitations. There’s also information about troubleshooting when you get stuck. You can ask questions on the ProofFrog discussion boards on GitHub.
• See how proofs in ProofFrog compare to proofs in more advanced formal verification tools like EasyCrypt via the Proof Ladders project, which includes an example showing CPA security of KEM-DEM in both ProofFrog and EasyCrypt. That version of the ProofFrog proof uses a slightly different formulation of the one-time secrecy game — one phrased with uniform sampling E.Key k <- E.Key; instead of E.KeyGen() — which lets the proof sidestep the key-uniformity assumption entirely and collapses the five reductions on this page down to three.
• Learn more about the technical background of ProofFrog in the for researchers section.
• Get in touch! We’d love to hear about your use of ProofFrog. Contributions of examples or improvements to the ProofFrog software are also welcome. The best way to reach us is on the ProofFrog GitHub repositories.