Secure Messaging

2.1. AEAD Definitions🔗

Definition2.1.1
uses 0
Used by 6
Reverse dependency previews
Preview
Definition 2.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\todo

structure AEADScheme (m : Type → Type u) [Monad m] (M AD K C : Type) where /-- Sample a fresh symmetric key. -/ keygen : m K /-- Deterministic encryption: `Enc(K, a, m) = e`. -/ encrypt : K → AD → M → C /-- Deterministic authenticated decryption: `Dec(K, a, e) = some m` or `none`. -/ decrypt : K → AD → C → Option M

github #192

Lean code for Definition2.1.1●1 definition
  • structure(3 fields)defined in SecureMessaging/AEAD/Defs.lean
    complete
    structure AEADScheme.{u} (m : Type → Type u) [Monad m] (M AD K C : Type) : Type u
    structure AEADScheme.{u} (m : Type → Type u)
  [Monad m] (M AD K C : Type) : Type u
    An authenticated encryption with associated data (AEAD) scheme with
message space `M`, associated-data space `AD`, key space `K`, and ciphertext space `C`.

Definition 1 of [ACD19].

    Fields

    keygen : m K
    Sample a fresh symmetric key. 
    encrypt : K → AD → M → C
    Deterministic encryption: `Enc(K, a, m) = e`. 
    decrypt : K → AD → C → Option M
    Deterministic authenticated decryption: `Dec(K, a, e) = some m` or `none`.
Definition2.1.2
uses 1used by 1✓L∃∀N

\todo

\Oenc(a,m)\gamestate\; (e^*\text{ - challenge ciphertext}, b\text{ - challenge bit})

\pif\;e^*\neq\bot\;\pthen\;\Return\bot

\pif\;b\;\pthen\;e^* \sample \mathcal C\;\pelse\;e^* \gets \Enc(K,a,m);\quad \Return e^*

def oracleEncrypt [SampleableType C] (ae : AEADScheme ProbComp M AD K C) (b : Bool) (k : K) : QueryImpl (AD × M →ₒ Option C) (StateT (Option C) ProbComp) := fun (a, m) => do match (← get) with | some _ => pure none | none => let eStar ← if b then liftM ($ᵗ C : ProbComp C) else pure (ae.encrypt k a m) set (some eStar) return some eStar
\Odec(a,e)\gamestate\; (e^*\text{ - challenge ciphertext}, b\text{ - challenge bit})

\pif\;b\,\vee\,e{ = }e^*\;\pthen\;\Return\bot\;\pelse\;\Return \Dec(K,a,e)

def oracleDecrypt [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (b : Bool) (k : K) : QueryImpl (AD × C →ₒ Option M) (StateT (Option C) ProbComp) := fun (a, e) => do if b || (← get) == some e then pure none else pure (ae.decrypt k a e)

uses Definition 2.1.1

Lean code for Definition2.1.2●2 definitions
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.oracleEncrypt {M AD K C : Type} [SampleableType C]
  (ae : AEADScheme ProbComp M AD K C) (b : Bool) (k : K) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option C)
    (StateT (Option C) ProbComp)
    def AEADScheme.oracleEncrypt {M AD K C : Type}
  [SampleableType C]
  (ae : AEADScheme ProbComp M AD K C)
  (b : Bool) (k : K) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦ Option C)
    (StateT (Option C) ProbComp)
    One-time encryption oracle `encrypt(a, m)` (Figure 1 of [ACD19], middle column).
First call: if `b = false`, sets `e* ← Enc(K, a, m)`;
            if `b = true`,  sets `e* ←$ C`.
            Returns `some e*`.
Subsequent calls: returns `none` (one-time oracle).
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.oracleDecrypt {M AD K C : Type} [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C) (b : Bool) (k : K) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option M)
    (StateT (Option C) ProbComp)
    def AEADScheme.oracleDecrypt {M AD K C : Type}
  [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (b : Bool) (k : K) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦ Option M)
    (StateT (Option C) ProbComp)
    Decryption oracle `decrypt(a, e)` (Figure 1 of [ACD19], right column).
`if e = e* or b = 1 return ⊥; return Dec(K, a, e)`.
When `eStar = none` (pre-challenge), the `e = e*` check is trivially false.

Note: the challenge guard compares the **ciphertext `e` only**, ignoring the
associated data `a` — faithful to ACD19 Def 2 / Fig 1 (the target notion here).
Definition2.1.3
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 2.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\todo

def Correct (ae : AEADScheme m M AD K C) : Prop := ∀ (k : K) (a : AD) (msg : M), ae.decrypt k a (ae.encrypt k a msg) = some msg

uses Definition 2.1.1 · github #193

Lean code for Definition2.1.3●1 definition
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.Correct.{u} {m : Type → Type u} [Monad m] {M AD K C : Type}
  (ae : AEADScheme m M AD K C) : Prop
    def AEADScheme.Correct.{u} {m : Type → Type u}
  [Monad m] {M AD K C : Type}
  (ae : AEADScheme m M AD K C) : Prop
    An AEAD scheme is correct if decryption always recovers the plaintext:
`∀ K a m, Dec(K, a, Enc(K, a, m)) = m`.
Definition2.1.4
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 6
Reverse dependency previews
Preview
Definition 2.1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\todo

Let \O = \{\Oenc, \Odec\} and denote by \adv^{\O} an adversary with oracle access to \O.

specification for oracle \O types

abbrev aeadOneTimeCCASpec (AD M C : Type) := unifSpec + (AD × M →ₒ Option C) + (AD × C →ₒ Option M)

specification for oracle set \O

def aeadSecurityImpl [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (b : Bool) (k : K) : QueryImpl (aeadOneTimeCCASpec AD M C) (StateT (Option C) ProbComp) := oracleUnif C + oracleEncrypt ae b k + oracleDecrypt ae b k

type of adversaries with oracle access

abbrev OneTimeCCAAdversary (AD M C : Type) := OracleComp (aeadOneTimeCCASpec AD M C) Bool
\Exp{\textsf{1\text{-}CCA}}{\textsf{AEAD}}(\adv)

K \sample \mathcal K;\quad b \sample \bit;\quad b' \gets \adv^{\O};\quad \Return(b'=b)

def securityExp [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (adversary : OneTimeCCAAdversary AD M C) : ProbComp Bool := do let k ← ae.keygen let b ← $ᵗ Bool let (b', _) ← (simulateQ (aeadSecurityImpl ae b k) adversary).run none return (b == b')

uses Definition 2.1.1 · Definition 2.1.2 · github #194

Lean code for Definition2.1.4●3 definitions
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.securityExp {M AD K C : Type} [SampleableType C]
  [DecidableEq C] (ae : AEADScheme ProbComp M AD K C)
  (adversary : AEADScheme.OneTimeCCAAdversary AD M C) : ProbComp Bool
    def AEADScheme.securityExp {M AD K C : Type}
  [SampleableType C] [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (adversary :
    AEADScheme.OneTimeCCAAdversary AD M
      C) :
  ProbComp Bool
    **One-time IND-CCA experiment** (Figure 1 + Definition 2 of [ACD19]).

`init`:   `K ←$ K; e* ← ⊥; b ←$ {0, 1}`
`run`:    `b' ← A^{encrypt, decrypt}`
`output`: `b' = b`
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.aeadSecurityImpl {M AD K C : Type} [SampleableType C]
  [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (b : Bool)
  (k : K) :
  QueryImpl (AEADScheme.aeadOneTimeCCASpec AD M C)
    (StateT (Option C) ProbComp)
    def AEADScheme.aeadSecurityImpl
  {M AD K C : Type} [SampleableType C]
  [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (b : Bool) (k : K) :
  QueryImpl
    (AEADScheme.aeadOneTimeCCASpec AD M C)
    (StateT (Option C) ProbComp)
    Complete oracle set for the one-time IND-CCA game (Figure 1 of [ACD19]).
  • abbrevdefined in SecureMessaging/AEAD/Defs.lean
    complete
    abbrev AEADScheme.OneTimeCCAAdversary (AD M C : Type) : Type
    abbrev AEADScheme.OneTimeCCAAdversary
  (AD M C : Type) : Type
    One-time IND-CCA adversary for an AEAD scheme: a single computation with
access to `encrypt` and `decrypt` oracles, outputting a guess bit `b'`.
Matches the adversary `A` in ACD19 Figure 1 + Definition 2.
Definition2.1.5
uses 1used by 1✓L∃∀N

\todo

\mathsf{decryptQueryBound}(\adv, q_d) asserts that the adversary \adv makes at most q_d queries to the decryption oracle \Odec (the tag-guessing term q_d/|T| in the EtM security bound is stated against this bound).

def decryptQueryBound (adv : OneTimeCCAAdversary AD M C) (q_d : ℕ) : Prop := adv.IsQueryBoundP (· matches Sum.inr _) q_d

uses Definition 2.1.4

Lean code for Definition2.1.5●1 definition
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.decryptQueryBound {M AD C : Type}
  (adv : AEADScheme.OneTimeCCAAdversary AD M C) (q_d : ℕ) : Prop
    def AEADScheme.decryptQueryBound
  {M AD C : Type}
  (adv :
    AEADScheme.OneTimeCCAAdversary AD M C)
  (q_d : ℕ) : Prop
    Structural bound on the number of decrypt-oracle queries made by a
one-time IND-CCA adversary. `decryptQueryBound adv q_d` asserts that `adv`
makes at most `q_d` queries to the decrypt oracle (index `.inr _` in
`aeadOneTimeCCASpec`), with no constraint on encryption or uniform-sampling
queries. Built on VCVio's `IsQueryBoundP`.
Definition2.1.6
uses 1used by 1✓L∃∀N

\todo

\mathsf{Adv}^{\textsf{guess}}_{\textsf{AEAD}}(\adv) = \Bigl|\, \Pr[\,b' = b\,] - \tfrac{1}{2} \,\Bigr|

noncomputable def guessAdvantage [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (adversary : OneTimeCCAAdversary AD M C) : ℝ := |(Pr[= true | securityExp ae adversary]).toReal - 1 / 2|

uses Definition 2.1.4

Lean code for Definition2.1.6●1 definition
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.guessAdvantage {M AD K C : Type} [SampleableType C]
  [DecidableEq C] (ae : AEADScheme ProbComp M AD K C)
  (adversary : AEADScheme.OneTimeCCAAdversary AD M C) : ℝ
    def AEADScheme.guessAdvantage
  {M AD K C : Type} [SampleableType C]
  [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (adversary :
    AEADScheme.OneTimeCCAAdversary AD M
      C) :
  ℝ
    One-time IND-CCA guess advantage: `|Pr[b' = b] - 1/2|`.
Definition2.1.7
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 2.1.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\todo

\mathsf{Adv}^{\textsf{dist}}_{\textsf{AEAD}}(\adv) = \Bigl|\, \Pr[\mathsf{AEAD_{rand}} = 1] - \Pr[\mathsf{AEAD_{real}} = 1] \,\Bigr|

Stated over the two fixed-bit experiments, each returning the adversary's raw guess b': \mathsf{AEAD_{real}} fixes b = 0 and \mathsf{AEAD_{rand}} fixes b = 1. This is the advantage the Encrypt-then-MAC security theorem bounds.

security experiment with a fixed challenge bit

def securityExpFixedBit [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (adversary : OneTimeCCAAdversary AD M C) (b : Bool) : ProbComp Bool := do let k ← ae.keygen let (b', _) ← (simulateQ (aeadSecurityImpl ae b k) adversary).run none return b'

distinguishing advantage over the two fixed-bit experiments

noncomputable def distAdvantage [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (adversary : OneTimeCCAAdversary AD M C) : ℝ := |(Pr[= true | securityExpFixedBit ae adversary true]).toReal - (Pr[= true | securityExpFixedBit ae adversary false]).toReal|

uses Definition 2.1.4

Lean code for Definition2.1.7●2 definitions
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.distAdvantage {M AD K C : Type} [SampleableType C]
  [DecidableEq C] (ae : AEADScheme ProbComp M AD K C)
  (adversary : AEADScheme.OneTimeCCAAdversary AD M C) : ℝ
    def AEADScheme.distAdvantage {M AD K C : Type}
  [SampleableType C] [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (adversary :
    AEADScheme.OneTimeCCAAdversary AD M
      C) :
  ℝ
    One-time IND-CCA distinguishing advantage:
`|Pr[AEAD_rand = 1] - Pr[AEAD_real = 1]|`.

Here `AEAD_real` is `securityExpFixedBit ae adversary false` and `AEAD_rand`
is `securityExpFixedBit ae adversary true`.
  • defdefined in SecureMessaging/AEAD/Defs.lean
    complete
    def AEADScheme.securityExpFixedBit {M AD K C : Type} [SampleableType C]
  [DecidableEq C] (ae : AEADScheme ProbComp M AD K C)
  (adversary : AEADScheme.OneTimeCCAAdversary AD M C) (b : Bool) :
  ProbComp Bool
    def AEADScheme.securityExpFixedBit
  {M AD K C : Type} [SampleableType C]
  [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (adversary :
    AEADScheme.OneTimeCCAAdversary AD M C)
  (b : Bool) : ProbComp Bool
    Security experiment with a fixed challenge bit `b` (not sampled uniformly).
The branch `b = false` is `AEAD_real`; the branch `b = true` is `AEAD_rand`.
Returns the adversary's raw guess `b'` (not `b == b'`).
Theorem2.1.8
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

\todo

\mathsf{Adv}^{\textsf{guess}}_{\textsf{AEAD}}(\adv) = \tfrac{1}{2}\,\mathsf{Adv}^{\textsf{dist}}_{\textsf{AEAD}}(\adv)

lemma guessAdvantage_eq_distAdvantage_div_two [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C) (adversary : OneTimeCCAAdversary AD M C) : guessAdvantage ae adversary = distAdvantage ae adversary / 2

uses Definition 2.1.6 · Definition 2.1.7

Lean code for Theorem2.1.8●1 theorem
  • theoremdefined in SecureMessaging/AEAD/Defs.lean
    complete
    theorem AEADScheme.guessAdvantage_eq_distAdvantage_div_two {M AD K C : Type}
  [SampleableType C] [DecidableEq C] (ae : AEADScheme ProbComp M AD K C)
  (adversary : AEADScheme.OneTimeCCAAdversary AD M C) :
  ae.guessAdvantage adversary = ae.distAdvantage adversary / 2
    theorem AEADScheme.guessAdvantage_eq_distAdvantage_div_two
  {M AD K C : Type} [SampleableType C]
  [DecidableEq C]
  (ae : AEADScheme ProbComp M AD K C)
  (adversary :
    AEADScheme.OneTimeCCAAdversary AD M
      C) :
  ae.guessAdvantage adversary =
    ae.distAdvantage adversary / 2
    The guess advantage equals half the distinguishing advantage:
`guessAdvantage = distAdvantage / 2`.

References: