2.2. GCM
Definition2.2.1
\todo
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)) (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 (0 : BitVec 96) ad.1.2 m
decrypt := fun k ad c => gcmDecrypt prp.toBlockCipher k (0 : BitVec 96) ad.1.2 c
uses Definition 2.1.1 · github #21
Lean code for Definition2.2.1●1 definition
Associated Lean declarations
-
gcmOneTimeAEAD[complete]
Associated Lean declarations
-
gcmOneTimeAEAD[complete]
-
defdefined in SecureMessaging/AEAD/FromGCM/Construction.leancomplete
def gcmOneTimeAEAD {K : Type} (prp : PRPScheme K (BitVec 128)) (L : ℕ) (_hL : ValidMsgLength L) : AEADScheme ProbComp (BitVec L) SupportedAAD K (BitVec L × BitVec 128)
def gcmOneTimeAEAD {K : Type} (prp : PRPScheme K (BitVec 128)) (L : ℕ) (_hL : ValidMsgLength L) : AEADScheme ProbComp (BitVec L) SupportedAAD K (BitVec L × BitVec 128)
One-time-key GCM as an `AEADScheme` (ACD19 interface). The IV is fixed to `0`; this is sound because `keygen` draws a fresh key per encryption, so the `(key, IV)` pair is never reused (GCM's uniqueness requirement, NIST §8). For a multi-invocation interface call `gcmEncrypt`/`gcmDecrypt` directly. `prp` supplies the block cipher and key generation; the mode itself uses only `prp.toBlockCipher` (the PRP→PRF switch lives in the security reduction). The AEAD key is the block-cipher key `K`, with no IV bundled in, and the ciphertext is `(C, T)`. The message is fixed to `BitVec L` so the ciphertext `BitVec L × BitVec 128` is a `SampleableType`, as the IND-CCA game needs; `SupportedAAD` and `_hL : ValidMsgLength L` keep the domain within NIST's supported lengths. `_hL` records the length requirement at construction but is unused in the body (correctness supplies its own), hence `nolint`.
Theorem2.2.2
Group: GCM. (2)
Statement uses 2
Associated Lean declarations
-
gcmOneTimeAEAD_correct[complete]
\todo
theorem gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128)) {L : ℕ}
(hL : ValidMsgLength L) :
(gcmOneTimeAEAD prp L hL).Correct
uses Definition 2.2.1 · Definition 2.1.3 · github #22
Lean code for Theorem2.2.2●1 theorem
Associated Lean declarations
-
gcmOneTimeAEAD_correct[complete]
Associated Lean declarations
-
gcmOneTimeAEAD_correct[complete]
-
theoremdefined in SecureMessaging/AEAD/FromGCM/Correctness.leancomplete
theorem gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128)) {L : ℕ} (hL : ValidMsgLength L) : (gcmOneTimeAEAD prp L hL).Correct
theorem gcmOneTimeAEAD_correct {K : Type} (prp : PRPScheme K (BitVec 128)) {L : ℕ} (hL : ValidMsgLength L) : (gcmOneTimeAEAD prp L hL).Correct
`gcmOneTimeAEAD` satisfies the ACD19 `AEADScheme.Correct`, given that the message length is supported (`hL`).
Theorem2.2.3
Group: GCM. (2)
Statement uses 2
Lean status
- No associated Lean code or declarations.
References:
-
Dworkin (2007)