Secure Messaging

7.2. Pseudorandom Permutations🔗

Definition7.2.1
uses 0
Used by 5
Reverse dependency previews
Preview
Definition 2.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
GitHub#240

A block cipher on a key space \mathcal K and a block space \mathcal X is a pair of maps \mathsf{perm}, \mathsf{perm}^{-1} : \mathcal K \times \mathcal X \to \mathcal X with \mathsf{perm}^{-1}(k, \mathsf{perm}(k, x)) = x and \mathsf{perm}(k, \mathsf{perm}^{-1}(k, x)) = x for all k and x. A PRP scheme is a block cipher together with a key generation algorithm \mathsf{keygen}. Its PRP advantage against an adversary \adv is

\mathsf{Adv}^{\textsf{prp}}_{\textsf{PRP}}(\adv) = \Bigl|\, \Pr\bigl[\Exp{\textsf{prp}\text{-}\textsf{real}}{\textsf{PRP}}(\adv) = 1\bigr] - \Pr\bigl[\Exp{\textsf{prp}\text{-}\textsf{ideal}}{\textsf{PRP}}(\adv) = 1\bigr] \,\Bigr|

for the experiments below, where \mathsf{Perm}(\mathcal X) is the set of permutations of \mathcal X.

block cipher

structure BlockCipher (K X : Type) where /-- The forward cipher function `CIPHₖ`. -/ perm : K → X → X /-- The inverse cipher function `CIPHₖ⁻¹`. -/ invPerm : K → X → X /-- `perm k` and `invPerm k` are mutually inverse for every key `k`. -/ correct : ∀ k x, invPerm k (perm k x) = x ∧ perm k (invPerm k x) = x

PRP scheme

structure PRPScheme (K X : Type) extends BlockCipher K X where /-- Randomized key generation. -/ keygen : ProbComp K
\Exp{\textsf{prp}\text{-}\textsf{real}}{\textsf{PRP}}(\adv)

k \sample \mathsf{keygen};\quad b' \gets \adv^{\mathsf{perm}\ k};\quad \Return b'

\Exp{\textsf{prp}\text{-}\textsf{ideal}}{\textsf{PRP}}(\adv)

\pi \sample \mathsf{Perm}(\mathcal X);\quad b' \gets \adv^{\pi};\quad \Return b'

PRP advantage

noncomputable def prpAdvantage [SampleableType (Equiv.Perm X)] (prp : PRPScheme K X) (adversary : PRPAdversary X) : ℝ := |(Pr[= true | prpRealExp prp adversary]).toReal - (Pr[= true | prpIdealExp adversary]).toReal|
Lean code for Definition7.2.1●3 definitions
  • structure(3 fields)defined in ToVCVio/CryptoFoundations/PRP.lean
    complete
    structure BlockCipher (K X : Type) : Type
    structure BlockCipher (K X : Type) : Type
    A block cipher (NIST SP 800-38D §5.1): a keyed permutation on `X`, given as
forward/inverse functions that are mutually inverse for every key (`correct`).

    Fields

    perm : K → X → X
    The forward cipher function `CIPHₖ`. 
    invPerm : K → X → X
    The inverse cipher function `CIPHₖ⁻¹`. 
    correct : ∀ (k : K) (x : X), self.invPerm k (self.perm k x) = x ∧ self.perm k (self.invPerm k x) = x
    `perm k` and `invPerm k` are mutually inverse for every key `k`.
  • structure(extends 1, 4 fields)defined in ToVCVio/CryptoFoundations/PRP.lean
    complete
    structure PRPScheme (K X : Type) : Type
    structure PRPScheme (K X : Type) : Type
    A pseudorandom permutation scheme: a `BlockCipher` plus randomized key
generation (`keygen`).

    Extends

    • BlockCipher K X

    Fields

    perm : K → X → X
    Inherited from
    1. BlockCipher
    invPerm : K → X → X
    Inherited from
    1. BlockCipher
    correct : ∀ (k : K) (x : X), self.invPerm k (self.perm k x) = x ∧ self.perm k (self.invPerm k x) = x
    Inherited from
    1. BlockCipher
    keygen : ProbComp K
    Randomized key generation.
  • defdefined in ToVCVio/CryptoFoundations/PRP.lean
    complete
    def PRPScheme.prpAdvantage {K X : Type} [SampleableType (Equiv.Perm X)]
  (prp : PRPScheme K X) (adversary : PRPScheme.PRPAdversary X) : ℝ
    def PRPScheme.prpAdvantage {K X : Type}
  [SampleableType (Equiv.Perm X)]
  (prp : PRPScheme K X)
  (adversary : PRPScheme.PRPAdversary X) :
  ℝ
    The PRP advantage of an adversary: the absolute difference between the probabilities that
it outputs `true` in the real and in the ideal experiment.

References:

  • Bellare and Rogaway (2006) — the PRP/PRF switching lemma.

  • Dworkin (2007) — the block cipher as a prerequisite of GCM (§5.1).