The Even–Mansour cipher in the ideal-permutation model

The Even–Mansour construction ([BS23], Section 4.7; [EM97]) builds a block cipher from a single public permutation π : Equiv.Perm G on a finite group G by XORing (or adding in G) independent pre-whitening and post-whitening keys (k₀, k₁) ∈ G × G: $$E((k_0, k_1), x) = \pi(x + k_0) + k_1, \qquad D((k_0, k_1), y) = \pi^{-1}(y - k_1) - k_0.$$ In the single-key variant ([DKS12]), k₀ = k₁ = k.

We formalize four aspects of the Even–Mansour construction:

1. Algebraic structure and one-query secrecy: evenMansourEquiv π k₀ k₁ : Equiv.Perm G bundles encryption and decryption as a permutation of G, satisfies the inverse-cipher conjugation law (evenMansourEquiv π k₀ k₁).symm = evenMansourEquiv π.symm (-k₁) (-k₀) (which swaps k₀ and k₁ over any group of exponent two such as BitString n), acts as a bijection on Equiv.Perm G for every fixed key pair (evenMansourPermEquiv), and achieves perfect one-query secrecy for any fixed π (map_prod_evenMansourEncrypt_uniformOfFintype).
2. Necessity of both whitening keys ([BS23], Section 4.7): omitting post-whitening (preWhitenEquiv π k₀ x = π (x + k₀)) or pre-whitening (postWhitenEquiv π k₁ x = π x + k₁) allows an explicit 2-query adversary (making 1 cipher query and 1 primitive permutation query, IsCallBounded _ 1 1) to recover the secret key with probability 1 and achieve key-recovery game advantage 1 - |G|⁻¹ against an independent uniform permutation and uniform target key (advantage_preWhitenKeyRecoveryGame_eq, advantage_postWhitenKeyRecoveryGame_eq).
3. One-sided query security: because evenMansourPermEquiv k₀ k₁ is a bijection on Equiv.Perm G, any adversary that queries only the cipher oracle (liftLeft) or only the primitive permutation oracle (liftRight) has zero distinguishing advantage between the real Even–Mansour game and two independent uniform permutations (advantage_evenMansourRealGame_liftLeft_eq_zero, advantage_evenMansourRealGame_liftRight_eq_zero).
4. Bad-key transcript intersection bound ([BS23], Theorem 4.10): given a cipher transcript T_e : List (G × G) and a primitive permutation transcript T_π : List (G × G), a key (k₀, k₁) is bad (isBadEvenMansourKey T_e T_π k) when some (x, y) ∈ T_e and (u, v) ∈ T_π collide on the internal permutation input (x + k₀ = u) or output (y - k₁ = v). Outside this bad set, the internal permutation queries made through the cipher are disjoint in both domain and range from the direct queries to π (disjoint_of_isBadEvenMansourKey_eq_false), and when T_e and T_π are consistent with evenMansourEquiv π k₀ k₁ and π, output collisions reduce to input collisions (isBadKeyPair_eq_decide_of_evenMansourEquiv). Under a uniform two-key (k₀, k₁) or single key k, the bad-key probability is at most 2 * |T_e| * |T_π| / |G| (toOuterMeasure_isBadEvenMansourKey_toReal_le, toOuterMeasure_isBadSingleKeyEvenMansour_toReal_le). For any adaptive distinguisher satisfying IsCallBounded program Q_e Q_π, OracleComp.IsCostBounded.transcript_cost_le bounds every supported transcript by |T_e| ≤ Q_e and |T_π| ≤ Q_π, yielding the 2 * Q_e * Q_π / |G| bad-key bound on every supported execution path (IsCallBounded.badEvenMansourKey_toReal_le, IsCallBounded.badSingleKeyEvenMansour_toReal_le). The lazy-sampled bidirectional random-permutation coupling step connecting this bad-key intersection bound to full two-sided Game.advantage (evenMansourRealGame program) (evenMansourIdealGame program) remains open.

Main definitions

• Cslib.Crypto.EvenMansour.evenMansourEncrypt, evenMansourDecrypt, evenMansourEquiv, singleKeyEvenMansourEquiv: Even–Mansour encryption, decryption, and bundled permutations.
• Cslib.Crypto.EvenMansour.preWhitenEquiv, postWhitenEquiv, preWhitenKeyRecoveryAttack, postWhitenKeyRecoveryAttack: single-whitening variants and 2-query key-recovery attacks.
• Cslib.Crypto.EvenMansour.PermQuery, PermOracleSpec, EvenMansourSpec, IsCallBounded: bidirectional cipher and primitive permutation oracle interface and separate query budgets.
• Cslib.Crypto.EvenMansour.evenMansourRealGame, singleKeyEvenMansourRealGame, evenMansourIdealGame: real and ideal bidirectional permutation games.
• Cslib.Crypto.EvenMansour.isBadKeyPair, isBadEvenMansourKey, isBadSingleKeyEvenMansour, transcriptCipher, transcriptPerm: bad-key collision predicates and transcript projections.

Main results

• Cslib.Crypto.EvenMansour.map_prod_evenMansourEncrypt_uniformOfFintype: one-query perfect secrecy and independence from the pre-whitening key k₀.
• Cslib.Crypto.EvenMansour.advantage_preWhitenKeyRecoveryGame_eq, Cslib.Crypto.EvenMansour.advantage_postWhitenKeyRecoveryGame_eq: 2-query attacks achieve key-recovery game advantage 1 - |G|⁻¹ when either whitening key is omitted.
• Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftLeft_eq_zero, Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftRight_eq_zero: zero advantage when queries are restricted to one oracle.
• Cslib.Crypto.EvenMansour.toOuterMeasure_isBadEvenMansourKey_toReal_le, Cslib.Crypto.EvenMansour.toOuterMeasure_isBadSingleKeyEvenMansour_toReal_le, Cslib.Crypto.EvenMansour.IsCallBounded.badEvenMansourKey_toReal_le, Cslib.Crypto.EvenMansour.IsCallBounded.badSingleKeyEvenMansour_toReal_le: Boneh–Shoup Theorem 4.10 bad-key probability bound 2 * Q_e * Q_π / |G|.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 4.7 (Theorem 4.10).
• S. Even, Y. Mansour, A Construction of a Cipher from a Single Pseudorandom Permutation.
• O. Dunkelman, N. Keller, A. Shamir, Minimalism in Cryptography: The Even–Mansour Scheme Revisited.

Algebraic Even–Mansour cipher over an additive group

def Cslib.Crypto.EvenMansour.evenMansourEncrypt {G : Type u_1} [AddGroup G] (π : G → G) (k₀ k₁ x : G) : G

Even–Mansour encryption ([BS23], Section 4.7; [EM97]): pre-whiten by adding k₀, apply the public permutation π, and post-whiten by adding k₁.

def Cslib.Crypto.EvenMansour.evenMansourDecrypt {G : Type u_1} [AddGroup G] (π_inv : G → G) (k₀ k₁ y : G) : G

Even–Mansour decryption: remove post-whitening key k₁, apply the inverse permutation π_inv, and remove pre-whitening key k₀.

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourDecrypt_evenMansourEncrypt {G : Type u_1} [AddGroup G] {π π_inv : G → G} (h : Function.LeftInverse π_inv π) (k₀ k₁ x : G) : evenMansourDecrypt π_inv k₀ k₁ (evenMansourEncrypt π k₀ k₁ x) = x

Decryption inverts encryption whenever π_inv is a left inverse of π.

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourEncrypt_evenMansourDecrypt {G : Type u_1} [AddGroup G] {π π_inv : G → G} (h : Function.RightInverse π_inv π) (k₀ k₁ y : G) : evenMansourEncrypt π k₀ k₁ (evenMansourDecrypt π_inv k₀ k₁ y) = y

Encryption inverts decryption whenever π_inv is a right inverse of π.

def Cslib.Crypto.EvenMansour.evenMansourEquiv {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ : G) : Equiv.Perm G

The Even–Mansour cipher bundled as a permutation Equiv.Perm G.

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_apply {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ x : G) : (evenMansourEquiv π k₀ k₁) x = π (x + k₀) + k₁

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_symm_apply {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ y : G) : (Equiv.symm (evenMansourEquiv π k₀ k₁)) y = (Equiv.symm π) (y - k₁) - k₀

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_zero {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) : evenMansourEquiv π 0 0 = π

With zero whitening keys, the Even–Mansour cipher is the underlying permutation π.

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_evenMansourEquiv {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ k₀' k₁' : G) : evenMansourEquiv (evenMansourEquiv π k₀ k₁) k₀' k₁' = evenMansourEquiv π (k₀' + k₀) (k₁ + k₁')

Composing two Even–Mansour wrappers with the same permutation adds the whitening keys.

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_symm {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ : G) : Equiv.symm (evenMansourEquiv π k₀ k₁) = evenMansourEquiv (Equiv.symm π) (-k₁) (-k₀)

The inverse of an Even–Mansour cipher with keys (k₀, k₁) and permutation π is an Even–Mansour cipher with keys (-k₁, -k₀) and inverse permutation π.symm.

@[reducible, inline]

abbrev Cslib.Crypto.EvenMansour.singleKeyEvenMansourEquiv {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k : G) : Equiv.Perm G

Single-key Even–Mansour cipher (k₀ = k₁ = k, [DKS12]).

theorem Cslib.Crypto.EvenMansour.evenMansourDecrypt_eq_of_neg_eq_self {G : Type u_1} [AddGroup G] (hneg : ∀ (x : G), -x = x) (π_inv : G → G) (k₀ k₁ y : G) : evenMansourDecrypt π_inv k₀ k₁ y = evenMansourEncrypt π_inv k₁ k₀ y

Over a group of exponent two (∀ x : G, -x = x), Even–Mansour decryption is encryption under the inverse permutation with the two keys swapped.

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_symm_eq_of_neg_eq_self {G : Type u_1} [AddGroup G] (hneg : ∀ (x : G), -x = x) (π : Equiv.Perm G) (k₀ k₁ : G) : Equiv.symm (evenMansourEquiv π k₀ k₁) = evenMansourEquiv (Equiv.symm π) k₁ k₀

Over a group of exponent two (∀ x : G, -x = x), inverting the Even–Mansour permutation swaps the pre-whitening and post-whitening keys.

theorem Cslib.Crypto.EvenMansour.evenMansourEquiv_symm_bitString {n : ℕ} (π : Equiv.Perm (BitString n)) (k₀ k₁ : BitString n) : Equiv.symm (evenMansourEquiv π k₀ k₁) = evenMansourEquiv (Equiv.symm π) k₁ k₀

Over BitString n, inverting the Even–Mansour permutation swaps k₀ and k₁.

def Cslib.Crypto.EvenMansour.evenMansourPermEquiv {G : Type u_1} [AddGroup G] (k₀ k₁ : G) : Equiv.Perm (Equiv.Perm G)

For any fixed keys (k₀, k₁), wrapping a permutation π in Even–Mansour is a bijection on Equiv.Perm G.

@[simp]

theorem Cslib.Crypto.EvenMansour.evenMansourPermEquiv_apply {G : Type u_1} [AddGroup G] (k₀ k₁ : G) (π : Equiv.Perm G) : (evenMansourPermEquiv k₀ k₁) π = evenMansourEquiv π k₀ k₁

One-query perfect secrecy

def Cslib.Crypto.EvenMansour.oneQueryKeyEquiv {G : Type u_1} [AddGroup G] (π : G → G) (x : G) : Equiv.Perm (G × G)

For any fixed function π : G → G and input x : G, the map (k₀, k₁) ↦ (k₀, π(x + k₀) + k₁) is a bijection on G × G.

theorem Cslib.Crypto.EvenMansour.map_prod_evenMansourEncrypt_uniformOfFintype {G : Type u_1} [AddGroup G] [Fintype G] [Nonempty G] (π : G → G) (x : G) : PMF.map (fun (k : G × G) => (k.1, evenMansourEncrypt π k.1 k.2 x)) (Probability.PMF.uniformOfFintype (G × G)) = Probability.PMF.uniformOfFintype (G × G)

One-query perfect secrecy: for any fixed π : G → G and plaintext x : G, under uniform independent keys (k₀, k₁), the pre-whitening key k₀ and the ciphertext evenMansourEncrypt π k₀ k₁ x are independent and uniformly distributed on G × G.

theorem Cslib.Crypto.EvenMansour.map_evenMansourEncrypt_uniformOfFintype {G : Type u_1} [AddGroup G] [Fintype G] [Nonempty G] (π : G → G) (x : G) : PMF.map (fun (k : G × G) => evenMansourEncrypt π k.1 k.2 x) (Probability.PMF.uniformOfFintype (G × G)) = Probability.PMF.uniformOfFintype G

Under uniform independent keys (k₀, k₁), a single Even–Mansour encryption of x is uniformly distributed on G for every fixed π : G → G.

Necessity of both whitening keys (algebraic recovery)

@[reducible, inline]

abbrev Cslib.Crypto.EvenMansour.preWhitenEquiv {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ : G) : Equiv.Perm G

Even–Mansour with pre-whitening only (k₁ = 0): E(k₀, x) = π(x + k₀) ([BS23], Section 4.7).

@[reducible, inline]

abbrev Cslib.Crypto.EvenMansour.postWhitenEquiv {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₁ : G) : Equiv.Perm G

Even–Mansour with post-whitening only (k₀ = 0): E(k₁, x) = π(x) + k₁ ([BS23], Section 4.7).

def Cslib.Crypto.EvenMansour.preWhitenKeyRecovery {G : Type u_1} [AddGroup G] (pi_inv_enc_x x : G) : G

Key recovery for preWhitenEquiv: given y = E(k₀, x) and u = π⁻¹(y), recover k₀ = -x + u.

theorem Cslib.Crypto.EvenMansour.preWhitenKeyRecovery_spec {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₀ x : G) : preWhitenKeyRecovery ((Equiv.symm π) ((preWhitenEquiv π k₀) x)) x = k₀

A single encryption query y = preWhitenEquiv π k₀ x and inverse permutation query π.symm y recover k₀ deterministically.

def Cslib.Crypto.EvenMansour.postWhitenKeyRecovery {G : Type u_1} [AddGroup G] (enc_x pi_x : G) : G

Key recovery for postWhitenEquiv: given y = E(k₁, x) and v = π(x), recover k₁ = -v + y.

theorem Cslib.Crypto.EvenMansour.postWhitenKeyRecovery_spec {G : Type u_1} [AddGroup G] (π : Equiv.Perm G) (k₁ x : G) : postWhitenKeyRecovery ((postWhitenEquiv π k₁) x) (π x) = k₁

A single encryption query y = postWhitenEquiv π k₁ x and forward permutation query π x recover k₁ deterministically.

Bidirectional ideal-permutation oracle interface and games

inductive Cslib.Crypto.EvenMansour.PermQuery (G : Type) : Type

A bidirectional query to a permutation on G: either evaluate in the forward direction or evaluate the inverse permutation.

• forward {G : Type} (x : G) : PermQuery G

  Forward query x ↦ P(x).

• inverse {G : Type} (y : G) : PermQuery G

  Inverse query y ↦ P⁻¹(y).

def Cslib.Crypto.EvenMansour.instDecidableEqPermQuery.decEq {G✝ : Type} [DecidableEq G✝] (x✝ x✝¹ : PermQuery G✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Crypto.EvenMansour.instDecidableEqPermQuery {G✝ : Type} [DecidableEq G✝] : DecidableEq (PermQuery G✝)

@[reducible, inline]

abbrev Cslib.Crypto.EvenMansour.PermOracleSpec (G : Type) : OracleSpec (PermQuery G)

The oracle specification of a bidirectional permutation on G.

def Cslib.Crypto.EvenMansour.evalPerm {G : Type} (P : Equiv.Perm G) : PermQuery G → G

Answer a bidirectional permutation query using P : Equiv.Perm G.

@[simp]

theorem Cslib.Crypto.EvenMansour.evalPerm_forward {G : Type} (P : Equiv.Perm G) (x : G) : evalPerm P (PermQuery.forward x) = P x

@[simp]

theorem Cslib.Crypto.EvenMansour.evalPerm_inverse {G : Type} (P : Equiv.Perm G) (y : G) : evalPerm P (PermQuery.inverse y) = (Equiv.symm P) y

@[reducible, inline]

abbrev Cslib.Crypto.EvenMansour.EvenMansourSpec (G : Type) : OracleSpec (PermQuery G ⊕ PermQuery G)

The combined oracle interface in the Even–Mansour security experiment ([BS23], Section 4.7): left queries (.inl) call the cipher permutation E and right queries (.inr) call the public primitive permutation π.

def Cslib.Crypto.EvenMansour.cipherCost {G : Type} : PermQuery G ⊕ PermQuery G → ℕ

Cost function counting cipher oracle calls (1 for .inl, 0 for .inr).

def Cslib.Crypto.EvenMansour.permCost {G : Type} : PermQuery G ⊕ PermQuery G → ℕ

Cost function counting primitive permutation oracle calls (0 for .inl, 1 for .inr).

def Cslib.Crypto.EvenMansour.IsCallBounded {G α : Type} (program : OracleComp (EvenMansourSpec G) α) (Q_e Q_π : ℕ) : Prop

An adversary program makes at most Q_e cipher queries and at most Q_π primitive permutation queries on every execution path.

theorem Cslib.Crypto.EvenMansour.IsCallBounded.isQueryBounded {G α : Type} {program : OracleComp (EvenMansourSpec G) α} {Q_e Q_π : ℕ} (h : IsCallBounded program Q_e Q_π) : program.IsQueryBounded (Q_e + Q_π)

A program making at most Q_e cipher queries and Q_π primitive queries makes at most Q_e + Q_π total queries.

def Cslib.Crypto.EvenMansour.queryCipherForward {G : Type} (x : G) : OracleComp (EvenMansourSpec G) G

Query the cipher permutation in the forward direction (x ↦ E(x)).

def Cslib.Crypto.EvenMansour.queryCipherInverse {G : Type} (y : G) : OracleComp (EvenMansourSpec G) G

Query the cipher permutation in the inverse direction (y ↦ E⁻¹(y)).

def Cslib.Crypto.EvenMansour.queryPermForward {G : Type} (u : G) : OracleComp (EvenMansourSpec G) G

Query the public primitive permutation in the forward direction (u ↦ π(u)).

def Cslib.Crypto.EvenMansour.queryPermInverse {G : Type} (v : G) : OracleComp (EvenMansourSpec G) G

Query the public primitive permutation in the inverse direction (v ↦ π⁻¹(v)).

theorem Cslib.Crypto.EvenMansour.isCallBounded_queryCipherForward {G : Type} (x : G) : IsCallBounded (queryCipherForward x) 1 0

theorem Cslib.Crypto.EvenMansour.isCallBounded_queryCipherInverse {G : Type} (y : G) : IsCallBounded (queryCipherInverse y) 1 0

theorem Cslib.Crypto.EvenMansour.isCallBounded_queryPermForward {G : Type} (u : G) : IsCallBounded (queryPermForward u) 0 1

theorem Cslib.Crypto.EvenMansour.isCallBounded_queryPermInverse {G : Type} (v : G) : IsCallBounded (queryPermInverse v) 0 1

def Cslib.Crypto.EvenMansour.evalTwoPerms {G α : Type} (E π : Equiv.Perm G) (program : OracleComp (EvenMansourSpec G) α) : α

Deterministically evaluate a program against cipher permutation E and primitive permutation π.

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_pure {G α : Type} (E π : Equiv.Perm G) (a : α) : evalTwoPerms E π (pure a) = a

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_map {G α β : Type} (E π : Equiv.Perm G) (f : α → β) (program : OracleComp (EvenMansourSpec G) α) : evalTwoPerms E π (f <$> program) = f (evalTwoPerms E π program)

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_bind {G α β : Type} (E π : Equiv.Perm G) (program : OracleComp (EvenMansourSpec G) α) (next : α → OracleComp (EvenMansourSpec G) β) : evalTwoPerms E π (program >>= next) = evalTwoPerms E π (next (evalTwoPerms E π program))

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_queryCipherForward {G : Type} (E π : Equiv.Perm G) (x : G) : evalTwoPerms E π (queryCipherForward x) = E x

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_queryCipherInverse {G : Type} (E π : Equiv.Perm G) (y : G) : evalTwoPerms E π (queryCipherInverse y) = (Equiv.symm E) y

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_queryPermForward {G : Type} (E π : Equiv.Perm G) (u : G) : evalTwoPerms E π (queryPermForward u) = π u

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_queryPermInverse {G : Type} (E π : Equiv.Perm G) (v : G) : evalTwoPerms E π (queryPermInverse v) = (Equiv.symm π) v

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_liftLeft {G α : Type} (E π π' : Equiv.Perm G) (program : OracleComp (PermOracleSpec G) α) : evalTwoPerms E π program.liftLeft = evalTwoPerms E π' program.liftLeft

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_liftRight {G α : Type} (E E' π : Equiv.Perm G) (program : OracleComp (PermOracleSpec G) α) : evalTwoPerms E π program.liftRight = evalTwoPerms E' π program.liftRight

def Cslib.Crypto.EvenMansour.evalEvenMansour {G α : Type} [AddGroup G] (π : Equiv.Perm G) (k₀ k₁ : G) (program : OracleComp (EvenMansourSpec G) α) : α

Deterministically evaluate a program in the real Even–Mansour world with public permutation π and keys (k₀, k₁).

def Cslib.Crypto.EvenMansour.preWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (x : G) : OracleComp (EvenMansourSpec G) G

Oracle attack recovering k₀ from preWhitenEquiv π k₀ in 1 cipher query and 1 primitive query: query y ← E(x) and u ← π⁻¹(y), then return -x + u.

theorem Cslib.Crypto.EvenMansour.isCallBounded_preWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (x : G) : IsCallBounded (preWhitenKeyRecoveryAttack x) 1 1

preWhitenKeyRecoveryAttack x makes at most 1 cipher query and 1 primitive query.

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_preWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (π : Equiv.Perm G) (k₀ x : G) : evalTwoPerms (preWhitenEquiv π k₀) π (preWhitenKeyRecoveryAttack x) = k₀

Against preWhitenEquiv π k₀ and π, preWhitenKeyRecoveryAttack x deterministically returns k₀.

def Cslib.Crypto.EvenMansour.postWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (x : G) : OracleComp (EvenMansourSpec G) G

Oracle attack recovering k₁ from postWhitenEquiv π k₁ in 1 cipher query and 1 primitive query: query y ← E(x) and v ← π(x), then return -v + y.

theorem Cslib.Crypto.EvenMansour.isCallBounded_postWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (x : G) : IsCallBounded (postWhitenKeyRecoveryAttack x) 1 1

postWhitenKeyRecoveryAttack x makes at most 1 cipher query and 1 primitive query.

@[simp]

theorem Cslib.Crypto.EvenMansour.evalTwoPerms_postWhitenKeyRecoveryAttack {G : Type} [AddGroup G] (π : Equiv.Perm G) (k₁ x : G) : evalTwoPerms (postWhitenEquiv π k₁) π (postWhitenKeyRecoveryAttack x) = k₁

Against postWhitenEquiv π k₁ and π, postWhitenKeyRecoveryAttack x deterministically returns k₁.

noncomputable def Cslib.Crypto.EvenMansour.evenMansourRealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (EvenMansourSpec G) Bool) : Game

The real Even–Mansour security experiment ([BS23], Section 4.7): sample a uniform permutation π ← Equiv.Perm G and uniform independent keys (k₀, k₁) ← G × G, and run program against evenMansourEquiv π k₀ k₁ and π.

noncomputable def Cslib.Crypto.EvenMansour.singleKeyEvenMansourRealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (EvenMansourSpec G) Bool) : Game

The single-key Even–Mansour security experiment ([DKS12]): sample a uniform permutation π ← Equiv.Perm G and a single uniform key k ← G, and run program against singleKeyEvenMansourEquiv π k and π.

noncomputable def Cslib.Crypto.EvenMansour.evenMansourIdealGame {G : Type} [Fintype G] [DecidableEq G] (program : OracleComp (EvenMansourSpec G) Bool) : Game

The ideal Even–Mansour security experiment: sample two independent uniform permutations E, π ← Equiv.Perm G and run program against E and π.

theorem Cslib.Crypto.EvenMansour.evenMansourRealGame_liftLeft_eq_ideal {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (PermOracleSpec G) Bool) : evenMansourRealGame program.liftLeft = evenMansourIdealGame program.liftLeft

For any adversary program that queries only the cipher oracle (liftLeft program), the real Even–Mansour game is identically distributed to the ideal game.

@[simp]

theorem Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftLeft_eq_zero {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (PermOracleSpec G) Bool) : (evenMansourRealGame program.liftLeft).advantage (evenMansourIdealGame program.liftLeft) = 0

Any adversary that queries only the cipher oracle (liftLeft) has zero advantage between the real Even–Mansour game and the ideal game.

theorem Cslib.Crypto.EvenMansour.evenMansourRealGame_liftRight_eq_ideal {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (PermOracleSpec G) Bool) : evenMansourRealGame program.liftRight = evenMansourIdealGame program.liftRight

For any adversary program that queries only the primitive permutation oracle (liftRight program), the real Even–Mansour game is identically distributed to the ideal game.

@[simp]

theorem Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftRight_eq_zero {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (program : OracleComp (PermOracleSpec G) Bool) : (evenMansourRealGame program.liftRight).advantage (evenMansourIdealGame program.liftRight) = 0

Any adversary that queries only the primitive permutation oracle (liftRight) has zero advantage between the real Even–Mansour game and the ideal game.

2-query oracle attacks when either whitening key is omitted

noncomputable def Cslib.Crypto.EvenMansour.preWhitenKeyRecoveryRealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : Game

Key-recovery game for pre-whitening-only Even–Mansour: draw π ← Equiv.Perm G and k₀ ← G, run preWhitenKeyRecoveryAttack x against preWhitenEquiv π k₀ and π, and test whether it outputs k₀.

noncomputable def Cslib.Crypto.EvenMansour.preWhitenKeyRecoveryIdealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : Game

Ideal comparison game for preWhitenKeyRecoveryAttack: draw independent uniform permutations E, π ← Equiv.Perm G and a uniform target key k₀ ← G, and test whether preWhitenKeyRecoveryAttack x outputs k₀.

@[simp]

theorem Cslib.Crypto.EvenMansour.preWhitenKeyRecoveryRealGame_eq_pure_true {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : preWhitenKeyRecoveryRealGame x = PMF.pure true

In the real pre-whitened game, preWhitenKeyRecoveryAttack x succeeds with probability 1.

theorem Cslib.Crypto.EvenMansour.preWhitenKeyRecoveryIdealGame_true_toReal {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : ((preWhitenKeyRecoveryIdealGame x) true).toReal = (↑(Fintype.card G))⁻¹

In the ideal game, preWhitenKeyRecoveryAttack x outputs the uniform target k₀ with probability |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.advantage_preWhitenKeyRecoveryGame_eq {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : ↑((preWhitenKeyRecoveryRealGame x).advantage (preWhitenKeyRecoveryIdealGame x)) = 1 - (↑(Fintype.card G))⁻¹

2-query break of pre-whitening-only Even–Mansour ([BS23], Section 4.7): omitting post-whitening (k₁ = 0) allows a 2-query attack (1 cipher query + 1 primitive query) to achieve key-recovery game advantage 1 - |G|⁻¹.

noncomputable def Cslib.Crypto.EvenMansour.postWhitenKeyRecoveryRealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : Game

Key-recovery game for post-whitening-only Even–Mansour: draw π ← Equiv.Perm G and k₁ ← G, run postWhitenKeyRecoveryAttack x against postWhitenEquiv π k₁ and π, and test whether it outputs k₁.

noncomputable def Cslib.Crypto.EvenMansour.postWhitenKeyRecoveryIdealGame {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : Game

Ideal comparison game for postWhitenKeyRecoveryAttack: draw independent uniform permutations E, π ← Equiv.Perm G and a uniform target key k₁ ← G, and test whether postWhitenKeyRecoveryAttack x outputs k₁.

@[simp]

theorem Cslib.Crypto.EvenMansour.postWhitenKeyRecoveryRealGame_eq_pure_true {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : postWhitenKeyRecoveryRealGame x = PMF.pure true

In the real post-whitened game, postWhitenKeyRecoveryAttack x succeeds with probability 1.

theorem Cslib.Crypto.EvenMansour.postWhitenKeyRecoveryIdealGame_true_toReal {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : ((postWhitenKeyRecoveryIdealGame x) true).toReal = (↑(Fintype.card G))⁻¹

In the ideal game, postWhitenKeyRecoveryAttack x outputs the uniform target k₁ with probability |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.advantage_postWhitenKeyRecoveryGame_eq {G : Type} [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] (x : G) : ↑((postWhitenKeyRecoveryRealGame x).advantage (postWhitenKeyRecoveryIdealGame x)) = 1 - (↑(Fintype.card G))⁻¹

2-query break of post-whitening-only Even–Mansour ([BS23], Section 4.7): omitting pre-whitening (k₀ = 0) allows a 2-query attack (1 cipher query + 1 primitive query) to achieve key-recovery game advantage 1 - |G|⁻¹.

Bad-key transcript intersection analysis (Boneh–Shoup Theorem 4.10)

def Cslib.Crypto.EvenMansour.isBadKeyPair {G : Type} [AddGroup G] [DecidableEq G] (e p k : G × G) : Bool

A key pair k = (k₀, k₁) is bad for a cipher input-output pair e = (x, y) and a primitive permutation input-output pair p = (u, v) if the internal permutation input x + k₀ collides with u or the internal permutation output y - k₁ collides with v ([BS23], Section 4.7, Theorem 4.10).

def Cslib.Crypto.EvenMansour.isBadEvenMansourKey {G : Type} [AddGroup G] [DecidableEq G] (T_e T_π : List (G × G)) (k : G × G) : Bool

A key pair k = (k₀, k₁) is bad for a cipher transcript T_e : List (G × G) and a primitive permutation transcript T_π : List (G × G) if some e ∈ T_e and p ∈ T_π collide on the internal permutation input or output ([BS23], Section 4.7, Theorem 4.10).

def Cslib.Crypto.EvenMansour.isBadSingleKeyEvenMansour {G : Type} [AddGroup G] [DecidableEq G] (T_e T_π : List (G × G)) (k : G) : Bool

Single-key specialization (k₀ = k₁ = k, [DKS12]) of the Even–Mansour bad-key predicate.

def Cslib.Crypto.EvenMansour.isBadInputKey {G : Type} [AddGroup G] [DecidableEq G] (T_e T_π : List (G × G)) (k₀ : G) : Bool

Input-only bad-key predicate (x + k₀ = u for some (x, y) ∈ T_e and (u, v) ∈ T_π), which captures all collisions in the real Even–Mansour world where y = π(x + k₀) + k₁ and v = π(u).

@[simp]

theorem Cslib.Crypto.EvenMansour.isBadKeyPair_eq_true_iff {G : Type} [AddGroup G] [DecidableEq G] (e p k : G × G) : isBadKeyPair e p k = true ↔ e.1 + k.1 = p.1 ∨ e.2 - k.2 = p.2

@[simp]

theorem Cslib.Crypto.EvenMansour.isBadEvenMansourKey_eq_true_iff {G : Type} [AddGroup G] [DecidableEq G] (T_e T_π : List (G × G)) (k : G × G) : isBadEvenMansourKey T_e T_π k = true ↔ ∃ e ∈ T_e, ∃ p ∈ T_π, e.1 + k.1 = p.1 ∨ e.2 - k.2 = p.2

theorem Cslib.Crypto.EvenMansour.disjoint_of_isBadEvenMansourKey_eq_false {G : Type} [AddGroup G] [DecidableEq G] {T_e T_π : List (G × G)} {k : G × G} (hgood : isBadEvenMansourKey T_e T_π k = false) {e p : G × G} (he : e ∈ T_e) (hp : p ∈ T_π) : e.1 + k.1 ≠ p.1 ∧ e.2 - k.2 ≠ p.2

Domain and range disjointness outside bad keys: when isBadEvenMansourKey T_e T_π k = false, every cipher pair (x, y) ∈ T_e has internal permutation input x + k₀ distinct from every primitive query input u in T_π, and internal permutation output y - k₁ distinct from every primitive query output v in T_π.

theorem Cslib.Crypto.EvenMansour.input_collision_iff_output_collision {G : Type} [AddGroup G] (π : Equiv.Perm G) (k : G × G) {e p : G × G} (he : (evenMansourEquiv π k.1 k.2) e.1 = e.2) (hp : π p.1 = p.2) : e.1 + k.1 = p.1 ↔ e.2 - k.2 = p.2

When e = (x, y) is consistent with evenMansourEquiv π k₀ k₁ (π (x + k₀) + k₁ = y) and p = (u, v) is consistent with π (π u = v), an output collision y - k₁ = v is equivalent to an input collision x + k₀ = u.

theorem Cslib.Crypto.EvenMansour.isBadKeyPair_eq_decide_of_evenMansourEquiv {G : Type} [AddGroup G] [DecidableEq G] (π : Equiv.Perm G) (k : G × G) {e p : G × G} (he : (evenMansourEquiv π k.1 k.2) e.1 = e.2) (hp : π p.1 = p.2) : isBadKeyPair e p k = decide (e.1 + k.1 = p.1)

On a pair (e, p) consistent with evenMansourEquiv π k.1 k.2 and π, isBadKeyPair e p k reduces to the input collision decide (e.1 + k.1 = p.1).

theorem Cslib.Crypto.EvenMansour.isBadEvenMansourKey_eq_isBadInputKey_of_evenMansourEquiv {G : Type} [AddGroup G] [DecidableEq G] (π : Equiv.Perm G) (k : G × G) {T_e T_π : List (G × G)} (hT_e : ∀ e ∈ T_e, (evenMansourEquiv π k.1 k.2) e.1 = e.2) (hT_π : ∀ p ∈ T_π, π p.1 = p.2) : isBadEvenMansourKey T_e T_π k = isBadInputKey T_e T_π k.1

On transcripts T_e and T_π consistent with evenMansourEquiv π k.1 k.2 and π, isBadEvenMansourKey T_e T_π k equals isBadInputKey T_e T_π k.1.

Exact single-pair collision probabilities and multi-query union bounds

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadKeyPair_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (e p : G × G) : (Probability.PMF.uniformOfFintype (G × G)).toOuterMeasure {k : G × G | isBadKeyPair e p k = true} ≤ 2 * (↑(Fintype.card G))⁻¹

For a single pair (e, p), a uniform key pair k ← G × G satisfies isBadKeyPair e p k with probability at most 2 * |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadKeyPair_singleKey_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (e p : G × G) : (Probability.PMF.uniformOfFintype G).toOuterMeasure {k : G | isBadKeyPair e p (k, k) = true} ≤ 2 * (↑(Fintype.card G))⁻¹

For a single pair (e, p), a single uniform key k ← G satisfies isBadKeyPair e p (k, k) with probability at most 2 * |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadEvenMansourKey_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (T_e T_π : List (G × G)) : (Probability.PMF.uniformOfFintype (G × G)).toOuterMeasure {k : G × G | isBadEvenMansourKey T_e T_π k = true} ≤ 2 * ↑T_e.length * ↑T_π.length * (↑(Fintype.card G))⁻¹

Boneh–Shoup Theorem 4.10 bad-key union bound (ℝ≥0∞): for any cipher transcript T_e and primitive permutation transcript T_π, a uniform key pair (k₀, k₁) ← G × G is bad with probability at most 2 * |T_e| * |T_π| * |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadEvenMansourKey_toReal_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (T_e T_π : List (G × G)) : ((Probability.PMF.uniformOfFintype (G × G)).toOuterMeasure {k : G × G | isBadEvenMansourKey T_e T_π k = true}).toReal ≤ 2 * ↑T_e.length * ↑T_π.length / ↑(Fintype.card G)

Boneh–Shoup Theorem 4.10 bad-key union bound (ℝ): for any cipher transcript T_e and primitive permutation transcript T_π, a uniform key pair (k₀, k₁) ← G × G is bad with real probability at most 2 * |T_e| * |T_π| / |G|.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadSingleKeyEvenMansour_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (T_e T_π : List (G × G)) : (Probability.PMF.uniformOfFintype G).toOuterMeasure {k : G | isBadSingleKeyEvenMansour T_e T_π k = true} ≤ 2 * ↑T_e.length * ↑T_π.length * (↑(Fintype.card G))⁻¹

Single-key Even–Mansour bad-key union bound (ℝ≥0∞, [DKS12]): for any cipher transcript T_e and primitive permutation transcript T_π, a single uniform key k ← G is bad with probability at most 2 * |T_e| * |T_π| * |G|⁻¹.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadSingleKeyEvenMansour_toReal_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (T_e T_π : List (G × G)) : ((Probability.PMF.uniformOfFintype G).toOuterMeasure {k : G | isBadSingleKeyEvenMansour T_e T_π k = true}).toReal ≤ 2 * ↑T_e.length * ↑T_π.length / ↑(Fintype.card G)

Single-key Even–Mansour bad-key union bound (ℝ, [DKS12]): for any cipher transcript T_e and primitive permutation transcript T_π, a single uniform key k ← G is bad with real probability at most 2 * |T_e| * |T_π| / |G|.

theorem Cslib.Crypto.EvenMansour.toOuterMeasure_isBadInputKey_toReal_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] (T_e T_π : List (G × G)) : ((Probability.PMF.uniformOfFintype G).toOuterMeasure {k₀ : G | isBadInputKey T_e T_π k₀ = true}).toReal ≤ ↑T_e.length * ↑T_π.length / ↑(Fintype.card G)

Input-collision union bound (ℝ): for any cipher transcript T_e and primitive transcript T_π, a uniform pre-whitening key k₀ ← G triggers an input collision isBadInputKey T_e T_π k₀ with real probability at most |T_e| * |T_π| / |G|.

Adaptive distinguisher transcript bounds via IsCallBounded

def Cslib.Crypto.EvenMansour.transcriptCipherEntry {G : Type} (entry : (q : PermQuery G ⊕ PermQuery G) × EvenMansourSpec G q) : Option (G × G)

Project a logged EvenMansourSpec G query-response entry onto its cipher input-output pair (x, y) (turning .inverse y with answer x into (x, y)), or none for primitive queries.

def Cslib.Crypto.EvenMansour.transcriptPermEntry {G : Type} (entry : (q : PermQuery G ⊕ PermQuery G) × EvenMansourSpec G q) : Option (G × G)

Project a logged EvenMansourSpec G query-response entry onto its primitive permutation input-output pair (u, v) (turning .inverse v with answer u into (u, v)), or none for cipher queries.

def Cslib.Crypto.EvenMansour.transcriptCipher {G : Type} (T : OracleComp.Transcript (EvenMansourSpec G)) : List (G × G)

The list of cipher input-output pairs recorded in a bidirectional interaction transcript.

def Cslib.Crypto.EvenMansour.transcriptPerm {G : Type} (T : OracleComp.Transcript (EvenMansourSpec G)) : List (G × G)

The list of primitive permutation input-output pairs recorded in a bidirectional interaction transcript.

@[simp]

theorem Cslib.Crypto.EvenMansour.length_transcriptCipher_eq_sum_cipherCost {G : Type} (T : OracleComp.Transcript (EvenMansourSpec G)) : (transcriptCipher T).length = (List.map (fun (entry : (q : PermQuery G ⊕ PermQuery G) × EvenMansourSpec G q) => cipherCost entry.fst) T).sum

The length of transcriptCipher T equals the total cipherCost of T.

@[simp]

theorem Cslib.Crypto.EvenMansour.length_transcriptPerm_eq_sum_permCost {G : Type} (T : OracleComp.Transcript (EvenMansourSpec G)) : (transcriptPerm T).length = (List.map (fun (entry : (q : PermQuery G ⊕ PermQuery G) × EvenMansourSpec G q) => permCost entry.fst) T).sum

The length of transcriptPerm T equals the total permCost of T.

theorem Cslib.Crypto.EvenMansour.IsCallBounded.length_transcriptCipher_le {G State γ : Type} {program : OracleComp (EvenMansourSpec G) γ} {Q_e Q_π : ℕ} (h : IsCallBounded program Q_e Q_π) (oracle : (q : PermQuery G ⊕ PermQuery G) → StateT State PMF (EvenMansourSpec G q)) {s s' : State} {result : γ} {T : OracleComp.Transcript (EvenMansourSpec G)} (hmem : (result, s', T) ∈ ((OracleComp.interpret (OracleComp.withTranscript oracle) program).run (s, [])).support) : (transcriptCipher T).length ≤ Q_e

Against any stateful bidirectional oracle, a supported run of program with IsCallBounded program Q_e Q_π records at most Q_e cipher pairs.

theorem Cslib.Crypto.EvenMansour.IsCallBounded.length_transcriptPerm_le {G State γ : Type} {program : OracleComp (EvenMansourSpec G) γ} {Q_e Q_π : ℕ} (h : IsCallBounded program Q_e Q_π) (oracle : (q : PermQuery G ⊕ PermQuery G) → StateT State PMF (EvenMansourSpec G q)) {s s' : State} {result : γ} {T : OracleComp.Transcript (EvenMansourSpec G)} (hmem : (result, s', T) ∈ ((OracleComp.interpret (OracleComp.withTranscript oracle) program).run (s, [])).support) : (transcriptPerm T).length ≤ Q_π

Against any stateful bidirectional oracle, a supported run of program with IsCallBounded program Q_e Q_π records at most Q_π primitive permutation pairs.

theorem Cslib.Crypto.EvenMansour.IsCallBounded.badEvenMansourKey_toReal_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] {State γ : Type} {program : OracleComp (EvenMansourSpec G) γ} {Q_e Q_π : ℕ} (h : IsCallBounded program Q_e Q_π) (oracle : (q : PermQuery G ⊕ PermQuery G) → StateT State PMF (EvenMansourSpec G q)) {s s' : State} {result : γ} {T : OracleComp.Transcript (EvenMansourSpec G)} (hmem : (result, s', T) ∈ ((OracleComp.interpret (OracleComp.withTranscript oracle) program).run (s, [])).support) : ((Probability.PMF.uniformOfFintype (G × G)).toOuterMeasure {k : G × G | isBadEvenMansourKey (transcriptCipher T) (transcriptPerm T) k = true}).toReal ≤ 2 * ↑Q_e * ↑Q_π / ↑(Fintype.card G)

Boneh–Shoup Theorem 4.10 for adaptive call-bounded distinguishers (two-key): on any supported transcript T of a distinguisher satisfying IsCallBounded program Q_e Q_π, a uniform key pair (k₀, k₁) ← G × G is bad with real probability at most 2 * Q_e * Q_π / |G|.

theorem Cslib.Crypto.EvenMansour.IsCallBounded.badSingleKeyEvenMansour_toReal_le {G : Type} [AddGroup G] [DecidableEq G] [Fintype G] [Nonempty G] {State γ : Type} {program : OracleComp (EvenMansourSpec G) γ} {Q_e Q_π : ℕ} (h : IsCallBounded program Q_e Q_π) (oracle : (q : PermQuery G ⊕ PermQuery G) → StateT State PMF (EvenMansourSpec G q)) {s s' : State} {result : γ} {T : OracleComp.Transcript (EvenMansourSpec G)} (hmem : (result, s', T) ∈ ((OracleComp.interpret (OracleComp.withTranscript oracle) program).run (s, [])).support) : ((Probability.PMF.uniformOfFintype G).toOuterMeasure {k : G | isBadSingleKeyEvenMansour (transcriptCipher T) (transcriptPerm T) k = true}).toReal ≤ 2 * ↑Q_e * ↑Q_π / ↑(Fintype.card G)

Boneh–Shoup Theorem 4.10 for adaptive call-bounded distinguishers (single-key): on any supported transcript T of a distinguisher satisfying IsCallBounded program Q_e Q_π, a single uniform key k ← G is bad with real probability at most 2 * Q_e * Q_π / |G|.