Generate a key pair and store a fallback secret for ciphertexts that fail validation.

Here \mathsf{PKE.KeyGen}(a,\mathsf{seed}_{SE}) denotes key generation with supplied seeds, implemented by PKE.keygenFromSeeds.

\begin{array}{l} s \sample \{0,1\}^{\ell};\quad \mathsf{seed}_{SE} \sample \{0,1\}^{r};\quad z \sample \{0,1\}^{128} \\[0.35em] a \gets H(z,128) \\[0.35em] ((a,B),S^{\mathsf T}) \gets \mathsf{PKE.KeyGen}(a,\mathsf{seed}_{SE}) \\[0.35em] b \gets P(B);\quad \mathsf{pk} \gets (a,b) \\[0.35em] \mathsf{pkh} \gets H(a\|b,\ell) \\[0.35em] \mathsf{sk} \gets (s,\mathsf{pk},S^{\mathsf T},\mathsf{pkh}) \\[0.35em] \Return (\mathsf{pk},\mathsf{sk}) \end{array}

Lean specification

def keygen {ps : ParameterSet} (ops : Operations ps) : ProbComp (PublicKey ps × SecretKey ps) := do let fallback ← $ᵗ (SharedSecretBits ps) let seedSE ← $ᵗ (SeedSEBits ps) let z ← $ᵗ (Bits lenZ) let p := ps.params let seedA := ops.shake z.toList lenSeedA let a := ops.gen seedA let stream := ops.shake (keygenPrefix.toList ++ seedSE.toList) (nbar * p.n * lenChi + p.n * nbar * lenChi) let samples := splitBits (a := nbar * p.n * lenChi) (b := p.n * nbar * lenChi) stream let st := (SampleMatrix ps.errorTable nbar p.n samples.1).map (fun x : ℤ => (x : ZMod p.q)) let e := (SampleMatrix ps.errorTable p.n nbar samples.2).map (fun x : ℤ => (x : ZMod p.q)) let b := a * st.transpose + e let pk : PublicKey ps := { seedA := seedA b := packBits ps p.n nbar (publicKeyBits_mod_eight ps) b } return (pk, { fallback := fallback publicKey := pk secretTranspose := st publicKeyHash := hashPublicKey ops pk })

Encrypt a fresh random message, then derive the shared secret from the ciphertext and intermediate key. In eFrodoKEM, t=0 and the salt is empty. The hash output is split into an r-bit seed and an \ell-bit key.

\begin{array}{l} \mu \sample \{0,1\}^{\ell};\quad \mathsf{salt} \sample \{0,1\}^{t} \\[0.35em] \mathsf{pkh} \gets H(a\|b,\ell) \\[0.35em] (\mathsf{seed}_{SE},k) \gets H(\mathsf{pkh}\|\mu\|\mathsf{salt},r+\ell) \\[0.35em] (B',C) \gets \mathsf{PKE.Enc}((a,U(b)),\mu;\mathsf{seed}_{SE}) \\[0.35em] c_1 \gets P(B');\quad c_2 \gets P(C);\quad c \gets (c_1,c_2,\mathsf{salt}) \\[0.35em] \mathsf{ss} \gets H(c_1\|c_2\|\mathsf{salt}\|k,\ell) \\[0.35em] \Return (c,\mathsf{ss}) \end{array}

Lean specification

def encaps {ps : ParameterSet} (ops : Operations ps) (pk : PublicKey ps) : ProbComp (Ciphertext ps × SharedSecretBits ps) := do let message ← $ᵗ (MessageBits ps) let salt ← $ᵗ (SaltBits ps) let p := ps.params let derived := deriveSeedAndKey ops (hashPublicKey ops pk) message salt let stream := ops.shake (encryptionPrefix.toList ++ derived.1.toList) (mbar * p.n * lenChi + (mbar * p.n * lenChi + mbar * nbar * lenChi)) let first := splitBits (a := mbar * p.n * lenChi) (b := mbar * p.n * lenChi + mbar * nbar * lenChi) stream let rest := splitBits (a := mbar * p.n * lenChi) (b := mbar * nbar * lenChi) first.2 let sp := (SampleMatrix ps.errorTable mbar p.n first.1).map (fun x : ℤ => (x : ZMod p.q)) let ep := (SampleMatrix ps.errorTable mbar p.n rest.1).map (fun x : ℤ => (x : ZMod p.q)) let a := ops.gen pk.seedA let bp := sp * a + ep let c1 := packBits ps mbar p.n (ciphertext1Bits_mod_eight ps) bp let epp := (SampleMatrix ps.errorTable mbar nbar rest.2).map (fun x : ℤ => (x : ZMod p.q)) let b := unpackBits ps p.n nbar (publicKeyBits_mod_eight ps) pk.b let v := sp * b + epp let c2 := packBits ps mbar nbar (ciphertext2Bits_mod_eight ps) (v + Encode p (message.cast (messageBits_length ps))) let c : Ciphertext ps := { c1 := c1, c2 := c2, salt := salt } return (c, ops.shake (c.c1.toList ++ c.c2.toList ++ c.salt.toList ++ derived.2.toList) p.ell)

Recover a candidate message, then derive an error seed and an intermediate key as in encapsulation. Reencrypt the message and compare both reconstructed matrices with those received. If either differs, replace the intermediate key with the fallback secret. Finally, hash the received ciphertext with the selected key.

\begin{array}{l} (s,(a,b),S^{\mathsf T},\mathsf{pkh}) \gets \mathsf{sk};\quad (c_1,c_2,\mathsf{salt}) \gets c \\[0.35em] (B',C) \gets (U(c_1),U(c_2)) \\[0.35em] \mu' \gets \mathsf{PKE.Dec}(S^{\mathsf T},(B',C)) \\[0.35em] (\mathsf{seed}'_{SE},k') \gets H(\mathsf{pkh}\|\mu'\|\mathsf{salt},r+\ell) \\[0.35em] (B'',C') \gets \mathsf{PKE.Enc}((a,U(b)),\mu';\mathsf{seed}'_{SE}) \\[0.35em] \widehat{k} \gets \begin{cases} k' & \text{if } B'=B'' \text{ and } C=C', \\[0.35em] s & \text{otherwise} \end{cases} \\[0.35em] \Return H(c_1\|c_2\|\mathsf{salt}\|\widehat{k},\ell) \end{array}

Lean specification

def decaps {ps : ParameterSet} (ops : Operations ps) (sk : SecretKey ps) (c : Ciphertext ps) : SharedSecretBits ps := let p := ps.params let bp := unpackBits ps mbar p.n (ciphertext1Bits_mod_eight ps) c.c1 let cm := unpackBits ps mbar nbar (ciphertext2Bits_mod_eight ps) c.c2 let m := cm - bp * sk.secretTranspose.transpose let message := (Decode p m).cast (messageBits_length ps).symm let derived := deriveSeedAndKey ops sk.publicKeyHash message c.salt let stream := ops.shake (encryptionPrefix.toList ++ derived.1.toList) (mbar * p.n * lenChi + (mbar * p.n * lenChi + mbar * nbar * lenChi)) let first := splitBits (a := mbar * p.n * lenChi) (b := mbar * p.n * lenChi + mbar * nbar * lenChi) stream let rest := splitBits (a := mbar * p.n * lenChi) (b := mbar * nbar * lenChi) first.2 let sp := (SampleMatrix ps.errorTable mbar p.n first.1).map (fun x : ℤ => (x : ZMod p.q)) let ep := (SampleMatrix ps.errorTable mbar p.n rest.1).map (fun x : ℤ => (x : ZMod p.q)) let a := ops.gen sk.publicKey.seedA let bpp := sp * a + ep let epp := (SampleMatrix ps.errorTable mbar nbar rest.2).map (fun x : ℤ => (x : ZMod p.q)) let b := unpackBits ps p.n nbar (publicKeyBits_mod_eight ps) sk.publicKey.b let v := sp * b + epp let cp := v + Encode p (message.cast (messageBits_length ps)) let selected := if bp = bpp ∧ cm = cp then derived.2 else sk.fallback ops.shake (c.c1.toList ++ c.c2.toList ++ c.salt.toList ++ selected.toList) p.ell