Skip to content

Pseudorandom functions

25 fully proved

The PRF experiment

DefinitionReal world of the PRF experiment#✓fully proved

Let \(K\), \(X\), \(Y\) and \(S\) be finite sets with \(K\), \(Y\) and \(S\) nonempty, let \(F : K \to X \to Y\) be a keyed function and let \(D\) be a distinguisher: an oracle algorithm with coins in \(S\) that queries a function \(X \to Y\) and outputs a bit. The real world is the distribution of the output of \(D\) with coins \(s\) and oracle \(F(k, \cdot)\), where the pair \((k, s)\) is uniform on \(K \times S\).

noncomputable def prfReal (F : K → X → Y) (D : S → OracleComp X Y Bool) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (K × S)).map fun ω => (D ω.2).run (F ω.1)
Uses 2 · Used by 5
Statement usesAdaptive oracle algorithms · Running an oracle algorithm
Used byCPA encryption from a PRF, concrete security · The CPA reduction is exact with the real oracle · The MAC reduction in the real PRF world · The MAC from a PRF, concrete security · PRF advantage

DefinitionRandom world of the PRF experiment#✓fully proved

Let \(X\), \(Y\) and \(S\) be finite sets with \(Y\) and \(S\) nonempty, and let \(D\) be a distinguisher: an oracle algorithm with coins in \(S\) that queries a function \(X \to Y\) and outputs a bit. The random world is the distribution of the output of \(D\) with coins \(s\) and oracle \(f\), where the pair \((f, s)\) is uniform on \((X \to Y) \times S\).

noncomputable def prfRand (D : S → OracleComp X Y Bool) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype ((X → Y) × S)).map fun ω => (D ω.2).run ω.1
Uses 2 · Used by 5
Statement usesAdaptive oracle algorithms · Running an oracle algorithm
Used byCPA encryption from a PRF, concrete security · The MAC from a PRF, concrete security · PRF advantage · The CPA reduction against a random function · Forging against a random function

DefinitionPRF advantage#✓fully proved

Let \(K\), \(X\), \(Y\) and \(S\) be finite sets with \(K\), \(Y\) and \(S\) nonempty, let \(F : K \to X \to Y\) be a keyed function and let \(D\) be a distinguisher: an oracle algorithm with coins in \(S\) that queries a function \(X \to Y\) and outputs a bit. The PRF advantage of \(D\) against \(F\) is the real number \(|p_{\mathrm{real}} - p_{\mathrm{rand}}|\), where \(p_{\mathrm{real}}\) is the probability that \(D\) outputs \(1\) in the real world (uniform coins \(s \in S\), oracle \(F(k, \cdot)\) for a uniform key \(k \in K\)) and \(p_{\mathrm{rand}}\) is the probability that \(D\) outputs \(1\) in the random world (uniform coins, oracle a uniformly random function \(X \to Y\)).

noncomputable def prfAdvantage (F : K → X → Y) (D : S → OracleComp X Y Bool) : ℝ :=
  |(prfReal F D true).toReal - (prfRand D true).toReal|
Uses 3 · Used by 2
Statement usesAdaptive oracle algorithms · Random world of the PRF experiment · Real world of the PRF experiment
Used byCPA encryption from a PRF, concrete security · The MAC from a PRF, concrete security

The MAC from a PRF

DefinitionWinning the forgery game#✓fully proved

A forger \(c\), an adaptive oracle algorithm with queries in \(M\), answers in \(T\) and output in \(M \times T\), wins against the tagging oracle \(O \colon M \to T\) when, run with oracle \(O\), it outputs a pair \((m, t)\) with \(O(m) = t\) and \(m\) is not among the queries it asks in that run.

def MacWins (O : M → T) (c : OracleComp M T (M × T)) : Prop :=
  O (c.run O).1 = (c.run O).2 ∧ (c.run O).1 ∉ c.queries O
Uses 3 · Used by 4
Statement usesAdaptive oracle algorithms · Queries of an oracle algorithm · Running an oracle algorithm
Used byCounting forgeries against a random function · The MAC forgery experiment · The MAC reduction in the real PRF world · Forging against a random function

DefinitionThe MAC forgery experiment#✓fully proved

Let \(K\) and \(R\) be finite nonempty types, let \(F \colon K \to M \to T\) be a keyed function, and let \(A\) be a forger: for coins \(r \in R\), \(A(r)\) is an adaptive oracle algorithm with queries in \(M\), answers in \(T\) and output in \(M \times T\). The existential-forgery experiment under an adaptive chosen-message attack for the MAC \(\mathrm{Mac}_k(m) = F(k, m)\) draws \((k, r)\) uniformly from \(K \times R\), runs \(A(r)\) with the tagging oracle \(F(k, \cdot)\), and outputs true exactly when \(A(r)\) wins against that oracle, that is, outputs a pair \((m, t)\) with \(F(k, m) = t\) where \(m\) is not among its queries.

noncomputable def macGame (F : K → M → T) (A : R → OracleComp M T (M × T)) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (K × R)).map fun ω => decide (MacWins (F ω.1) (A ω.2))
Uses 4 · Used by 2
Statement usesAdaptive oracle algorithms · Queries of an oracle algorithm · Running an oracle algorithm · Winning the forgery game
Used byThe MAC reduction in the real PRF world · The MAC from a PRF, concrete security

DefinitionThe distinguisher built from a forger#✓fully proved

For a list \(L\) of messages in \(M\) and a forger \(c\), an adaptive oracle algorithm with queries in \(M\), answers in \(T\) and output in \(M \times T\), the MAC reduction is the oracle algorithm with the same queries and answers and a Boolean output, defined by recursion on \(c\). If \(c\) stops with output \((m, t)\), it queries \(m\) and, on answer \(t'\), stops with output true exactly when \(t' = t\) and \(m \notin L\). If \(c\) queries \(x\) and continues with \(c_y\) on answer \(y\), it queries \(x\) and, on answer \(y\), continues as the MAC reduction of \(c_y\) with \(x\) added to \(L\).

Started with the empty list, it runs the forger, logging its queries, then queries the forged message and accepts when the answer is the forged tag and the message is fresh.

def macReduction (log : List M) : OracleComp M T (M × T) → OracleComp M T Bool
  | .pure p => query p.1 fun t => done (decide (t = p.2 ∧ p.1 ∉ log))
  | .liftBind x k => query x fun y => macReduction (x :: log) (k y)
Uses 4 · Used by 3
Statement usesAdaptive oracle algorithms · The oracle algorithm that stops at once · Query step · The signature of one oracle
Used byThe MAC reduction in the real PRF world · The MAC from a PRF, concrete security · Forging against a random function

TheoremThe MAC reduction in the real PRF world#✓fully proved

Let \(K\) and \(R\) be finite nonempty types, let \(F \colon K \to M \to T\) be a keyed function, and let \(A\) be a forger: for coins \(r \in R\), \(A(r)\) is an adaptive oracle algorithm with queries in \(M\), answers in \(T\) and output in \(M \times T\). Then the output distribution of the existential-forgery experiment for \(F\) and \(A\) equals the output distribution of the real world of the PRF experiment for \(F\) with the distinguisher that, on coins \(r\), runs the MAC reduction on \(A(r)\) starting from the empty query log.

theorem macGame_eq_prfReal (F : K → M → T) (A : R → OracleComp M T (M × T)) :
    macGame F A = prfReal F (fun r => macReduction [] (A r))
Uses 10 · Used by 1
Statement usesAdaptive oracle algorithms · The MAC forgery experiment · The distinguisher built from a forger · Real world of the PRF experiment
Proof usesThe oracle algorithm that stops at once · Queries of an oracle algorithm · Query step · Running an oracle algorithm · The signature of one oracle · Winning the forgery game
Used byThe MAC from a PRF, concrete security

TheoremCounting forgeries against a random function#✓fully proved

Let \(M\) and \(T\) be finite sets and let \(c\) be an adaptive oracle algorithm that queries messages in \(M\), receives tags in \(T\) and outputs a pair in \(M \times T\). Call a function \(f \colon M \to T\) a win for \(c\) when the run of \(c\) with oracle \(f\) outputs a pair \((m, t)\) with \(f(m) = t\) and \(m\) not among the messages queried in that run. If \(W\) is the set of functions \(M \to T\) that are wins for \(c\), then \(|W| \cdot |T| \le |T|^{|M|}\).

Changing the tag of the fresh forged message, which the run never queries, gives \(|T|\) functions with the same run, of which exactly one is a win.

theorem card_macWins_mul_le (c : OracleComp M T (M × T)) :
    (univ.filter fun f : M → T => MacWins f c).card * Fintype.card T ≤ Fintype.card (M → T)
Uses 5 · Used by 1
Statement usesAdaptive oracle algorithms · Queries of an oracle algorithm · Running an oracle algorithm · Winning the forgery game
Proof usesLocality of oracle runs
Used byForging against a random function

TheoremForging against a random function#✓fully proved

Let \(M\) and \(T\) be finite sets with \(T\) nonempty, and let \(A\) be a forger: an oracle algorithm with coins in a finite nonempty set that queries tags in \(T\) of messages in \(M\) and outputs a message together with a tag. When the tagging oracle is a uniformly random function \(M \to T\) and the coins are uniform, the MAC reduction built from \(A\) accepts (that is, \(A\) outputs the correct tag of a message it never queried) with probability at most \(1/|T|\).

theorem prfRand_macReduction_le (A : R → OracleComp M T (M × T)) :
    (prfRand (fun r => macReduction [] (A r)) true).toReal ≤ 1 / Fintype.card T
Uses 10 · Used by 1
Statement usesAdaptive oracle algorithms · The distinguisher built from a forger · Random world of the PRF experiment
Proof usesThe oracle algorithm that stops at once · Queries of an oracle algorithm · Query step · Running an oracle algorithm · The signature of one oracle · Winning the forgery game · Counting forgeries against a random function
Used byThe MAC from a PRF, concrete security

TheoremThe MAC from a PRF, concrete security#✓fully proved

Let \(K\), \(M\), \(T\) and \(R\) be finite types with \(K\), \(T\) and \(R\) nonempty, let \(F \colon K \to M \to T\) be a keyed function, and let \(A\) be an adaptive chosen-message forger: for coins \(r \in R\), \(A(r)\) is an adaptive oracle algorithm with queries in \(M\), answers in \(T\) and output in \(M \times T\). Then the probability that \(A\) wins the existential-forgery experiment for the MAC \(\mathrm{Mac}_k(m) = F(k, m)\) is at most the PRF advantage against \(F\) of the distinguisher that, on coins \(r\), runs the MAC reduction on \(A(r)\) starting from the empty query log, plus \(1 / |T|\).

This is the reduction of Katz and Lindell, Theorem 4.6, stated as a concrete inequality.

theorem macGame_le (F : K → M → T) (A : R → OracleComp M T (M × T)) :
    (macGame F A true).toReal ≤
      prfAdvantage F (fun r => macReduction [] (A r)) + 1 / Fintype.card T
Uses 8
Statement usesAdaptive oracle algorithms · The MAC forgery experiment · The distinguisher built from a forger · PRF advantage
Proof usesThe MAC reduction in the real PRF world · Random world of the PRF experiment · Forging against a random function · Real world of the PRF experiment

CPA encryption from a PRF

DefinitionEncryption from a keyed function#✓fully proved

Let \(Y\) be an additive commutative group of messages and let \(f \colon X \to Y\) be a function (in the scheme, \(f = F_k\) for a key \(k\)). The encryption of a message \(m \in Y\) with randomness \(r \in X\) is the pair \((r, f(r) + m) \in X \times Y\).

This is Construction 3.30 of Katz and Lindell, with XOR replaced by the addition of the message group.

def encrypt (Fk : X → Y) (m : Y) (r : X) : X × Y := (r, Fk r + m)
Used by 6
Used byThe CPA reduction is exact with the real oracle · The adversary's guess in the CPA experiment · Correctness of encryption with a keyed function · The CPA reduction against a random function · Running an algorithm against the bounded encryption oracle · The encryption oracle depends only on the encryption randomness

DefinitionDecryption with a keyed function#✓fully proved

For a function \(F_k \colon X \to Y\) into an additive commutative group \(Y\), the decryption of a ciphertext \((r, c) \in X \times Y\) is \(\mathrm{Dec}(r, c) = c - F_k(r)\).

def decrypt (Fk : X → Y) (c : X × Y) : Y := c.2 - Fk c.1
Used by 1
Used byCorrectness of encryption with a keyed function

TheoremCorrectness of encryption with a keyed function#✓fully proved

Let \(Y\) be an additive commutative group and \(F_k \colon X \to Y\) a function. For every message \(m \in Y\) and every randomness \(r \in X\), decrypting the ciphertext \(\mathrm{Enc}(m) = (r, F_k(r) + m)\) gives back \(m\), that is, \(\mathrm{Dec}(\mathrm{Enc}(m)) = m\) where \(\mathrm{Dec}(r, c) = c - F_k(r)\).

theorem decrypt_encrypt (Fk : X → Y) (m : Y) (r : X) : decrypt Fk (encrypt Fk m r) = m
Uses 2
Statement usesDecryption with a keyed function · Encryption from a keyed function

DefinitionSelecting the challenge message by a bit#✓fully proved

Given a pair of messages \((m_0, m_1) \in Y \times Y\) and a challenge bit \(b\), the selected message is \(m_1\) when \(b\) is true and \(m_0\) when \(b\) is false.

def pick (m : Y × Y) (b : Bool) : Y := if b then m.2 else m.1
Used by 4
Used byThe CPA reduction is exact with the real oracle · The adversary's guess in the CPA experiment · The PRF distinguisher built from a CPA adversary · The CPA reduction against a random function

DefinitionRunning an algorithm against the bounded encryption oracle#✓fully proved

Let \(X\) be a set, \(Y\) an abelian group written additively, \(f : X \to Y\) a function, \(q \in \mathbb{N}\) and \(\rho : \{0, \dots, q - 1\} \to X\) the encryption randomness of the queries. Run from query index \(i \in \mathbb{N}\), an oracle algorithm with messages in \(Y\) as queries, answers in \(X \times Y\) and outputs in \(\beta\) either fails or yields its output together with the next query index: if it stops with output \(a\), the result is \((a, i)\); if it queries a message \(m\) and \(i < q\), the oracle answers \((\rho(i), f(\rho(i)) + m)\) and the run continues from index \(i + 1\); if it queries a message and \(i \ge q\), the run fails.

def runEnc {β : Type*} (f : X → Y) (ρ : Fin q → X) : OracleComp Y (X × Y) β → ℕ → Option (β × ℕ)
  | .pure a, i => some (a, i)
  | .liftBind m k, i =>
    if h : i < q then runEnc f ρ (k (encrypt f m (ρ ⟨i, h⟩))) (i + 1) else none
Uses 3 · Used by 4
Statement usesAdaptive oracle algorithms · The signature of one oracle · Encryption from a keyed function
Used byThe CPA reduction is exact with the real oracle · The adversary's guess in the CPA experiment · The CPA reduction against a random function · The encryption oracle depends only on the encryption randomness

AbbreviationCPA adversary#✓fully proved

A CPA adversary with coins in \(R\), against an encryption oracle that takes messages in \(Y\) and returns ciphertexts in \(X \times Y\), assigns to each \(r \in R\) an adaptive oracle algorithm with access to the encryption oracle that outputs two challenge messages \((m_0, m_1) \in Y \times Y\) together with a second adaptive oracle algorithm, again with access to the encryption oracle, which takes the challenge ciphertext in \(X \times Y\) and outputs a guess for the challenge bit.

abbrev CPAAdversary (X Y R : Type*) :=
  R → OracleComp Y (X × Y) ((Y × Y) × (X × Y → OracleComp Y (X × Y) Bool))
Uses 1 · Used by 6
Statement usesAdaptive oracle algorithms
Used byCPA advantage · CPA encryption from a PRF, concrete security · The CPA experiment · The CPA reduction is exact with the real oracle · The PRF distinguisher built from a CPA adversary · The CPA reduction against a random function

DefinitionThe adversary's guess in the CPA experiment#✓fully proved

Let \(Y\) be an additive commutative group, \(f \colon X \to Y\) a function, \(q\) a natural number, \(\rho \colon \{0, \dots, q - 1\} \to X\) the encryption randomness, \(r_s \in X\) the challenge randomness and \(b\) a bit. Let \(c\) be an oracle algorithm for the encryption oracle that outputs two messages \((m_0, m_1) \in Y \times Y\) and a second-phase algorithm. The encryption query with index \(i\), counting from \(0\) across both phases, is answered for a message \(m\) by \((\rho_i, f(\rho_i) + m)\). Run \(c\); when it outputs \((m_0, m_1)\), run its second phase on the challenge ciphertext \((r_s, f(r_s) + m_b)\), where \(m_b\) is \(m_1\) if \(b\) is true and \(m_0\) otherwise. The guess is the output of the second phase. If the two phases together ask more than \(q\) encryption queries, the adversary is stopped and the guess is false.

def cpaGuess (f : X → Y) (ρ : Fin q → X) (rs : X) (b : Bool)
    (c : OracleComp Y (X × Y) ((Y × Y) × (X × Y → OracleComp Y (X × Y) Bool))) : Bool :=
  ((runEnc f ρ c 0).bind fun p =>
    (runEnc f ρ (p.1.2 (encrypt f (pick p.1.1 b) rs)) p.2).map Prod.fst).getD false
Uses 4 · Used by 3
Statement usesAdaptive oracle algorithms · Encryption from a keyed function · Selecting the challenge message by a bit · Running an algorithm against the bounded encryption oracle
Used byThe CPA experiment · The CPA reduction is exact with the real oracle · The CPA reduction against a random function

DefinitionThe CPA experiment#✓fully proved

Let \(K\), \(X\) and \(R\) be nonempty finite sets, \(Y\) an additive commutative group, \(q\) a natural number, \(F \colon K \to X \to Y\) a keyed function and \(A\) a CPA adversary with coins in \(R\). The CPA indistinguishability experiment \(\mathrm{PrivK}^{\mathrm{cpa}}\) for the scheme \(\mathrm{Enc}_k(m) = (r, F_k(r) + m)\) draws, uniformly and independently, a key \(k \in K\), encryption randomness \(\rho \colon \{0, \dots, q - 1\} \to X\) for the encryption queries, challenge randomness \(r_s \in X\), a challenge bit \(b\) and coins \(r \in R\). It outputs true exactly when the adversary's guess, with keyed function \(F_k\), encryption randomness \(\rho\), challenge randomness \(r_s\), challenge bit \(b\) and the algorithm that \(A\) assigns to \(r\), equals \(b\). An adversary that asks more than \(q\) encryption queries is stopped and guesses false.

noncomputable def cpaGame (F : K → X → Y) (A : CPAAdversary X Y R) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (K × (Fin q → X) × X × Bool × R)).map fun ω =>
    cpaGuess (F ω.1) ω.2.1 ω.2.2.1 ω.2.2.2.1 (A ω.2.2.2.2) == ω.2.2.2.1
Uses 2 · Used by 3
Statement usesCPA adversary · The adversary's guess in the CPA experiment
Used byCPA advantage · CPA encryption from a PRF, concrete security · The CPA reduction is exact with the real oracle

DefinitionCPA advantage#✓fully proved

Let \(K\), \(X\) and \(R\) be nonempty finite sets, \(Y\) an additive commutative group, \(q\) a natural number, \(F \colon K \to X \to Y\) a keyed function and \(A\) a CPA adversary with coins in \(R\). The CPA advantage of \(A\) is the real number \(|p - 1/2|\), where \(p\) is the probability that the CPA experiment for \(F\) and \(A\) with at most \(q\) encryption queries outputs true, that is, that \(A\) guesses the challenge bit.

noncomputable def cpaAdvantage (F : K → X → Y) (A : CPAAdversary X Y R) : ℝ :=
  |(cpaGame q F A true).toReal - 1 / 2|
Uses 2 · Used by 1
Statement usesCPA adversary · The CPA experiment
Used byCPA encryption from a PRF, concrete security

DefinitionSimulating the encryption oracle with a function oracle#✓fully proved

Let \(X\) be a set, \(Y\) an abelian group written additively, \(q \in \mathbb{N}\) and \(\rho : \{0, \dots, q - 1\} \to X\) the encryption randomness of the queries. Started at query index \(i \in \mathbb{N}\), the simulation turns an oracle algorithm with messages in \(Y\) as queries, answers in \(X \times Y\) and outputs in \(\beta\) into an oracle algorithm with queries in \(X\) and answers in \(Y\) that either fails or outputs the original output together with the next query index: if the original algorithm stops with output \(a\), the simulation stops with \((a, i)\); if it queries a message \(m\) and \(i < q\), the simulation queries \(\rho(i)\) and, on answer \(y\), continues by simulating the original algorithm on the answer \((\rho(i), y + m)\) from index \(i + 1\); if it queries a message and \(i \ge q\), the simulation stops with failure.

def simEnc {β : Type*} (ρ : Fin q → X) :
    OracleComp Y (X × Y) β → ℕ → OracleComp X Y (Option (β × ℕ))
  | .pure a, i => done (some (a, i))
  | .liftBind m k, i =>
    if h : i < q then query (ρ ⟨i, h⟩) fun y => simEnc ρ (k (ρ ⟨i, h⟩, y + m)) (i + 1)
    else done none
Uses 4 · Used by 3
Statement usesAdaptive oracle algorithms · The oracle algorithm that stops at once · Query step · The signature of one oracle
Used byThe CPA reduction is exact with the real oracle · The PRF distinguisher built from a CPA adversary · The CPA reduction against a random function

DefinitionThe PRF distinguisher built from a CPA adversary#✓fully proved

Let \(X\) and \(R\) be sets, \(Y\) an additive commutative group, \(q\) a natural number and \(A\) a CPA adversary with coins in \(R\) against an encryption oracle that takes messages in \(Y\) and returns ciphertexts in \(X \times Y\). With its own coins \((\rho, r_s, b, r)\), where \(\rho \colon \{0, \dots, q - 1\} \to X\), \(r_s \in X\), \(b\) is a bit and \(r \in R\), and with oracle access to a function \(O \colon X \to Y\), the distinguisher runs the algorithm \(A\) assigns to \(r\). It answers the encryption query with index \(i\), counting from \(0\) across both phases, for a message \(m\) by querying \(O\) at \(\rho_i\) and returning \((\rho_i, O(\rho_i) + m)\). When the first phase outputs messages \((m_0, m_1)\), it queries \(O\) at \(r_s\) and gives the second phase the challenge ciphertext \((r_s, O(r_s) + m_b)\), where \(m_b\) is \(m_1\) if \(b\) is true and \(m_0\) otherwise. It outputs true exactly when the adversary's guess equals \(b\), where an adversary that asks more than \(q\) encryption queries is stopped and guesses false.

def cpaReduction (A : CPAAdversary X Y R) (s : (Fin q → X) × X × Bool × R) :
    OracleComp X Y Bool :=
  PFunctor.FreeM.bind (simEnc s.1 (A s.2.2.2) 0) fun o =>
    match o with
    | none => done (false == s.2.2.1)
    | some p => query s.2.1 fun y =>
        PFunctor.FreeM.bind (simEnc s.1 (p.1.2 (s.2.1, y + pick p.1.1 s.2.2.1)) p.2) fun o' =>
          done ((o'.map Prod.fst).getD false == s.2.2.1)
Uses 7 · Used by 3
Statement usesAdaptive oracle algorithms · The oracle algorithm that stops at once · Query step · The signature of one oracle · CPA adversary · Selecting the challenge message by a bit · Simulating the encryption oracle with a function oracle
Used byCPA encryption from a PRF, concrete security · The CPA reduction is exact with the real oracle · The CPA reduction against a random function

TheoremThe CPA reduction is exact with the real oracle#✓fully proved

Let \(K\), \(X\) and \(R\) be nonempty finite sets, \(Y\) an additive commutative group, \(q\) a natural number and \(F \colon K \to X \to Y\) a keyed function. For every CPA adversary \(A\) with coins in \(R\), the CPA experiment for \(F\) and \(A\) with at most \(q\) encryption queries has the same output distribution as the real world of the PRF experiment for \(F\) run with the distinguisher built from \(A\) for \(q\) queries: with the oracle \(F_k\) for a uniform key \(k\), the reduction runs the CPA experiment exactly.

theorem cpaGame_eq_prfReal (F : K → X → Y) (A : CPAAdversary X Y R) :
    cpaGame q F A = prfReal F (cpaReduction q A)
Uses 15 · Used by 1
Statement usesCPA adversary · The CPA experiment · The PRF distinguisher built from a CPA adversary · Real world of the PRF experiment
Proof usesAdaptive oracle algorithms · The oracle algorithm that stops at once · Query step · Running an oracle algorithm · Running a sequential composition · The signature of one oracle · The adversary's guess in the CPA experiment · Encryption from a keyed function · Selecting the challenge message by a bit · Running an algorithm against the bounded encryption oracle · Simulating the encryption oracle with a function oracle
Used byCPA encryption from a PRF, concrete security

TheoremThe encryption oracle depends only on the encryption randomness#✓fully proved

Let \(Y\) be an additive commutative group, let \(\rho_0, \dots, \rho_{q-1} \in X\) be encryption randomness and let \(f, f' : X \to Y\) satisfy \(f(\rho_j) = f'(\rho_j)\) for every \(j < q\). Then for every oracle algorithm \(c\) and every natural number \(i\), running \(c\) against the encryption oracle built from \(f\), with query indices starting at \(i\), gives the same result as running it against the one built from \(f'\). Here the encryption oracle built from \(f\) answers a query \(m\) with index \(n < q\) by \((\rho_n, f(\rho_n) + m)\), and the run fails at a query with index \(n \ge q\).

theorem runEnc_congr {β : Type*} {f f' : X → Y} {ρ : Fin q → X} (h : ∀ j, f (ρ j) = f' (ρ j)) :
    ∀ (c : OracleComp Y (X × Y) β) (i : ℕ), runEnc f ρ c i = runEnc f' ρ c i
Uses 4 · Used by 1
Statement usesAdaptive oracle algorithms · Running an algorithm against the bounded encryption oracle
Proof usesThe signature of one oracle · Encryption from a keyed function
Used byThe CPA reduction against a random function

TheoremThe CPA reduction against a random function#✓fully proved

Let \(X\) be a finite nonempty set, \(Y\) a finite additive commutative group, \(q\) a natural number and \(A\) a CPA adversary with coins in a finite nonempty set. Let \(p\) be the probability that the CPA reduction built from \(A\) (whose encryption oracle answers at most \(q\) queries) outputs \(1\), that is, that \(A\) guesses the challenge bit, when its oracle is a uniformly random function \(X \to Y\) and its coins are uniform. Then \(|p - 1/2| \le q / (2|X|)\).

The success probability is exactly \(1/2\) unless the challenge randomness repeats the randomness of one of the at most \(q\) encryption queries.

theorem prfRand_cpaReduction (A : CPAAdversary X Y R) :
    |(prfRand (cpaReduction q A) true).toReal - 1 / 2| ≤ q / (2 * Fintype.card X)
Uses 15 · Used by 1
Statement usesCPA adversary · The PRF distinguisher built from a CPA adversary · Random world of the PRF experiment
Proof usesAdaptive oracle algorithms · The oracle algorithm that stops at once · Query step · Running an oracle algorithm · Running a sequential composition · The signature of one oracle · The adversary's guess in the CPA experiment · Encryption from a keyed function · Selecting the challenge message by a bit · Running an algorithm against the bounded encryption oracle · The encryption oracle depends only on the encryption randomness · Simulating the encryption oracle with a function oracle
Used byCPA encryption from a PRF, concrete security

TheoremCPA encryption from a PRF, concrete security#✓fully proved

Let \(K\), \(X\) and \(R\) be nonempty finite sets, \(Y\) a finite additive commutative group, \(q\) a natural number and \(F \colon K \to X \to Y\) a keyed function, used in the scheme \(\mathrm{Enc}_k(m) = (r, F_k(r) + m)\) with uniform randomness \(r \in X\). For every CPA adversary \(A\) with coins in \(R\), the CPA advantage of \(A\) in the experiment whose encryption oracle answers at most \(q\) queries is at most the PRF advantage of \(F\) against the distinguisher built from \(A\) plus \(q / (2 |X|)\).

This is the reduction of Katz and Lindell, Theorem 3.31, with the sharper statistical term \(q / (2 |X|)\) in place of \(q / |X|\).

theorem cpaAdvantage_le (F : K → X → Y) (A : CPAAdversary X Y R) :
    cpaAdvantage q F A ≤ prfAdvantage F (cpaReduction q A) + q / (2 * Fintype.card X)
Uses 10
Statement usesCPA adversary · CPA advantage · The PRF distinguisher built from a CPA adversary · PRF advantage
Proof usesAdaptive oracle algorithms · The CPA experiment · The CPA reduction is exact with the real oracle · Random world of the PRF experiment · The CPA reduction against a random function · Real world of the PRF experiment

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.