2.2. GCM
GCM authenticated encryption from NIST SP 800-38D, used as a one-time AEAD scheme built on a
pseudorandom permutation, with a fixed public 96-bit initialisation vector iv. The key is
the permutation's key. Encryption returns the encrypted message together with an
authentication tag computed over the associated data and the encrypted message; decryption
recomputes the tag and rejects on mismatch.
The scheme's domain is the NIST-supported length range. A plaintext/ciphertext
bit-length is supported when it is at most 2^39 - 256 and byte-aligned:
@[reducible] def ValidMsgLength (lenC : ℕ) : Prop := lenC ≤ 2 ^ 39 - 256 ∧ 8 ∣ lenC
and the associated data is any byte-aligned bit-string of length at most 2^64 - 1:
@[reducible] def ValidAADLength (lenA : ℕ) : Prop := lenA ≤ 2 ^ 64 - 1 ∧ 8 ∣ lenAabbrev SupportedAAD := { x : (a : ℕ) × BitVec a // ValidAADLength x.1 }def gcmOneTimeAEAD {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ)
(_hL : ValidMsgLength L) :
AEADScheme ProbComp (BitVec L) SupportedAAD
K (BitVec L × BitVec 128) where
keygen := prp.keygen
encrypt := fun k ad m => gcmEncrypt prp.toBlockCipher k iv ad.1.2 m
decrypt := fun k ad c => gcmDecrypt prp.toBlockCipher k iv ad.1.2 cLean code for Definition2.2.1●1 definition
Associated Lean declarations
-
GCM.gcmOneTimeAEAD[complete]
-
GCM.gcmOneTimeAEAD[complete]
-
defdefined in SecureMessaging/AEAD/FromGCM/Construction.leancomplete
def GCM.gcmOneTimeAEAD {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ) (_hL : GCM.ValidMsgLength L) : AEADScheme ProbComp (BitVec L) GCM.SupportedAAD K (BitVec L × BitVec 128)
def GCM.gcmOneTimeAEAD {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ) (_hL : GCM.ValidMsgLength L) : AEADScheme ProbComp (BitVec L) GCM.SupportedAAD K (BitVec L × BitVec 128)
GCM under the block cipher of `prp` with a fixed public IV `iv`. A fixed IV is safe here because each key encrypts only one message, so no `(key, IV)` pair repeats.
\todo
theorem gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128))
(iv : BitVec 96) {L : ℕ} (hL : ValidMsgLength L) :
(gcmOneTimeAEAD prp iv L hL).CorrectLean code for Theorem2.2.2●1 theorem
Associated Lean declarations
-
GCM.gcmOneTimeAEAD_correct[complete]
-
GCM.gcmOneTimeAEAD_correct[complete]
-
theoremdefined in SecureMessaging/AEAD/FromGCM/Correctness.leancomplete
theorem GCM.gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) {L : ℕ} (hL : GCM.ValidMsgLength L) : (GCM.gcmOneTimeAEAD prp iv L hL).Correct
theorem GCM.gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) {L : ℕ} (hL : GCM.ValidMsgLength L) : (GCM.gcmOneTimeAEAD prp iv L hL).Correct
`gcmOneTimeAEAD` satisfies the ACD19 `AEADScheme.Correct`, given that the message length is supported (`hL`).
For every PRP scheme P on 128-bit blocks, every 96-bit IV iv, every
supported message length L and every adversary \adv making at most q_d decryption
queries,
\mathsf{Adv}^{\textsf{dist}}_{\textsf{GCM}}(\adv)
\le \mathsf{Adv}^{\textsf{prp}}_{P}(B)
+ \frac{(n+2)(n+1)}{2^{129}}
+ q_d \cdot \frac{2^{57} + n + 1}{2^{128}}
where n = \lceil L/128 \rceil and B = \mathsf{prfReduction}\ iv\ L\ \adv.
theorem gcmOneTimeAEAD_security (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ)
(hL : ValidMsgLength L)
(adv : OneTimeCCAAdversary SupportedAAD (BitVec L) (BitVec L × BitVec 128))
(q_d : ℕ) (hq : AEADScheme.decryptQueryBound adv q_d) :
let blocks : ℕ := (L + 127) / 128
let reduction := prfReduction iv L adv
let switchingBound : ℝ := ((blocks : ℝ) + 2) * ((blocks : ℝ) + 1) / 2 ^ 129
let forgeryBound : ℝ := (q_d : ℝ) * ((2 ^ 57 + (blocks : ℝ) + 1) / 2 ^ 128)
AEADScheme.distAdvantage (gcmOneTimeAEAD prp iv L hL) adv ≤
PRPScheme.prpAdvantage prp reduction + switchingBound + forgeryBoundLean code for Theorem2.2.3●1 theorem
Associated Lean declarations
-
GCM.gcmOneTimeAEAD_security[complete]
-
GCM.gcmOneTimeAEAD_security[complete]
-
theoremdefined in SecureMessaging/AEAD/FromGCM/Security.leancomplete
theorem GCM.gcmOneTimeAEAD_security {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ) (hL : GCM.ValidMsgLength L) (adv : AEADScheme.OneTimeCCAAdversary GCM.SupportedAAD (BitVec L) (BitVec L × BitVec 128)) (q_d : ℕ) (hq : AEADScheme.decryptQueryBound adv q_d) : have blocks := (L + 127) / 128; have reduction := GCM.prfReduction iv L adv; have switchingBound := (↑blocks + 2) * (↑blocks + 1) / 2 ^ 129; have forgeryBound := ↑q_d * ((2 ^ 57 + ↑blocks + 1) / 2 ^ 128); (GCM.gcmOneTimeAEAD prp iv L hL).distAdvantage adv ≤ prp.prpAdvantage reduction + switchingBound + forgeryBound
theorem GCM.gcmOneTimeAEAD_security {K : Type} (prp : PRPScheme K (BitVec 128)) (iv : BitVec 96) (L : ℕ) (hL : GCM.ValidMsgLength L) (adv : AEADScheme.OneTimeCCAAdversary GCM.SupportedAAD (BitVec L) (BitVec L × BitVec 128)) (q_d : ℕ) (hq : AEADScheme.decryptQueryBound adv q_d) : have blocks := (L + 127) / 128; have reduction := GCM.prfReduction iv L adv; have switchingBound := (↑blocks + 2) * (↑blocks + 1) / 2 ^ 129; have forgeryBound := ↑q_d * ((2 ^ 57 + ↑blocks + 1) / 2 ^ 128); (GCM.gcmOneTimeAEAD prp iv L hL).distAdvantage adv ≤ prp.prpAdvantage reduction + switchingBound + forgeryBound
**One-time IND-CCA security of GCM.** Let - `gcmOneTimeAEAD prp iv L hL` be GCM with block cipher `prp`, 96-bit IV `iv` and `L`-bit messages, and - `adv` be a one-time IND-CCA adversary against it making at most `q_d` decryption queries. Then ```text Adv^{ot-cca-ror}(adv) ≤ Adv^{prp}(B) + (n + 2)(n + 1) / 2¹²⁹ + q_d · (2⁵⁷ + n + 1) / 2¹²⁸ ``` where `B` (`reduction`) is the adversary `prfReduction iv L adv` against `prp`, and `n = ⌈L/128⌉` (`blocks`) is the number of message blocks. The first term is the PRP advantage of `B`. The second, `switchingBound`, is the cost of replacing the random permutation by a random function. The third, `forgeryBound`, bounds the probability that a decryption query forges a valid tag; its `2⁵⁷ + n + 1` is `maxBlocks L`.
References:
-
Dworkin (2007)