Add specification for AES-GCM

[pennyannn]

Description:

This PR adds specification for AES-GCM, including specification for AES-encrypt, GCTR, GHASH, GCM-AE and GCM-AD. The specification is written based on NIST standard for AES and GCM.

This PR also adds tests for AES and AES-GCM specifications.

Testing:

make all succeeds and cosim tests pass on Graviton2 and Graviton3.

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

[aqjune-aws]

Hi Yann, I want to review this pull request by doing these two checks:

1. Checking the consistency between signatures of the Lean functions and the human-written specifications in https://nvlpubs.nist.gov/nistpubs/legacy/sp/nistspecialpublication800-38d.pdf . I left a few comments regarding this. I did not dive into the every detail since the functions are large & there are test vectors.
2. Checking the validity of test vectors, esp. with respect to the test vectors in https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf .

I have a question about AES-GCM test vectors - does AWS-LC have its own test-vectors for AES-GCM? Or are the test sets equivalent to the test vectors in the pdf document?

[aqjune-aws]

One minor comment in PR description:

... GCM-AE and GCM-DE

GCM-AE and GCM-AD, maybe? :)

[pennyannn]

I have a question about AES-GCM test vectors - does AWS-LC have its own test-vectors for AES-GCM? Or are the test sets equivalent to the test vectors in the pdf document?

Yes, AWS-LC has its own test vectors, see https://github.com/aws/aws-lc/tree/main/crypto/cipher_extra/test
The AWS-LC tests are more comprehensive. It includes the tests from the document https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf

[aqjune-aws]

I compared the test vectors in Tests/*Test.lean with the vectors written in the pdf files and they matched.
I will recommend waiting for comments from one more reviewers.

[hanno-becker]

I am happy to have a look as well, assuming it is OK if the review takes a few days (I am not well-versed with Lean, plus other commitments).

[hanno-becker]

@pennyannn Thank you for this work, and for giving me time to review, which was a very interesting way to get a glimpse of LNSym and Lean. I hope subsequent reviews will be quicker.

I don't have any blocking comments, only this suggestion: The deviation(s) from the spec in terms of byte ordering is quite confusing. Could one not map the spec to Lean 1-1, and introduce a byte-reversing wrapper at the very end?

[hanno-becker]

This is what I had in mind, in the example of GCM encrypt, and only checked insofar as a single test vector goes.

It follows the specification more closely by avoiding byte reversals. Instead, only CIPH_128 needs flipping in the end.

@pennyannn I don't know if this style would cause issues elsewhere, so I'm not necessarily suggesting all definitions be reworked like this. But it might be useful to keep definitions in the style below around for closer proximity to the spec.

def GHASH_aux (i : Nat) (H : BitVec 128) (X : BitVec n) (Y : BitVec 128)
  (h : 128 ∣ n) : BitVec 128 :=
  if n / 128 ≤ i then
    Y
  else
    let lo := (n/128 - 1 - i) * 128
    let hi := lo + 127
    have h₀ : hi - lo + 1 = 128 := by omega
    let Xi := extractLsb hi lo X
    let res := (Y ^^^ (h₀ ▸ Xi))
    let Y := mul res H
    GHASH_aux (i + 1) H X Y h
  termination_by (n / 128 - i)

/-- GHASH: hashing message X using Galois field multiplication -/
def GHASH (H : BitVec 128) (X : BitVec n) (h : 128 ∣ n) : BitVec 128 :=
  GHASH_aux 0 H X (BitVec.zero 128) h

def GCTR_aux (CIPH : Cipher (n := 128) (m := m))
  (i : Nat) (n : Nat) (K : BitVec m) (ICB : BitVec 128)
  (X : BitVec v) (Y : BitVec v) : BitVec v :=
  if n ≤ i then
    Y
  else
    let lo := (n - i - 1) * 128
    let hi := lo + 127
    have h : hi - lo + 1 = 128 := by omega
    -- extractLsb will fill upper bits with zeros if hi >= len X
    let Xi := extractLsb hi lo X
    -- reversing counter because AES expects little-endian
    let Yi := h ▸ Xi ^^^ (CIPH ICB K)
    -- partInstall ignores val indexes that exceeds length of Y
    let Y := BitVec.partInstall hi lo (h.symm ▸ Yi) Y
    let ICB := inc_s 32 ICB (by omega) (by omega)
    GCTR_aux CIPH (i + 1) n K ICB X Y
  termination_by (n - i)

--protected def ceiling_in_blocks (w : Nat) := (w - 1) / 128 + 1
protected def ceiling_in_blocks (w : Nat) := (w + 127) / 128
protected def ceiling_in_bits (w : Nat) := (GCM.ceiling_in_blocks w) * 128

protected theorem bits_le_ceiling_in_bits (w : Nat) :
  w ≤ (GCM.ceiling_in_blocks w) * 128 := by
  simp only [GCM.ceiling_in_blocks]
  omega

/-- GCTR: encrypting/decrypting message x using Galois counter mode -/
def GCTR (CIPH : Cipher (n := 128) (m := m))
  (K : BitVec m) (ICB : BitVec 128) (X : BitVec v) : (BitVec v) :=
  let n := GCM.ceiling_in_blocks v
  let b := GCM.ceiling_in_bits v
  let s := b - v
  let h : v + s = b := by sorry
  let X' : BitVec b := h ▸ (shiftLeftZeroExtend X s)
  let R := GCTR_aux CIPH 0 n K ICB X' $ BitVec.zero b
  truncate v $ R >>> s

protected theorem initialize_J0_simplification
  (lv : Nat) (x : Nat) (h : lv ≤ x * 128):
  lv + (x * 128 - lv + 64) + 64  = x * 128 + 128 := by omega

protected def initialize_J0 (H : BitVec 128) (IV : BitVec lv) :=
  if h₀ : lv == 96
  then have h₁ : lv + 31 + 1 = 128 := by
         simp only [Nat.succ.injEq]
         exact Nat.eq_of_beq_eq_true h₀
       h₁ ▸ (IV ++ BitVec.zero 31 ++ 0b1#1)
  else let s := GCM.ceiling_in_bits lv - lv
       have h₂ : 128 ∣ (lv + (s + 64) + 64) := by
         simp only [s, GCM.ceiling_in_bits]
         rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
             (by apply GCM.bits_le_ceiling_in_bits)]
         omega
       have h₃ : 8 ∣ (lv + (s + 64) + 64) := by
         simp only [s, GCM.ceiling_in_bits]
         rw [GCM.initialize_J0_simplification lv (GCM.ceiling_in_blocks lv)
             (by apply GCM.bits_le_ceiling_in_bits)]
         omega
       let block := rev_elems (lv + (s + 64 ) + 64) 8
                      (IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv))
                      h₃ (by decide)
       rev_elems 128 8 (GHASH H block h₂) (by decide) (by decide)

protected theorem GCM_AE_DE_simplification1 (a : Nat) (v : Nat) (p : Nat) (u : Nat) :
  64 + 64 + u + p + v + a = 128 + (u + p) + (v + a) := by omega

protected theorem GCM_AE_DE_simplification1' (a : Nat) (v : Nat) (p : Nat) (u : Nat) :
  a + v + p + u + 64 + 64 = 128 + (u + p) + (v + a) := by omega

protected theorem GCM_AE_DE_simplification2
  (y : Nat) (x : Nat) (h : y ≤ x * 128):
  (x * 128 - y) + y = x * 128 := by omega

/-- GCM_AE : Galois Counter Mode Authenticated Encryption -/
def GCM_AE (CIPH : Cipher (n := 128) (m := 128))
  (K : BitVec 128) (t : Nat) (IV : BitVec lv) (P : BitVec p) (A : BitVec a)
  : (BitVec p) × (BitVec t) :=
  let H := CIPH (BitVec.zero 128) K
  let J0 : BitVec 128 := GCM.initialize_J0 H IV
  let ICB := inc_s 32 J0 (by decide) (by decide)
  let C := GCTR (m := 128) CIPH K ICB P
  let u := GCM.ceiling_in_bits p - p
  let v := GCM.ceiling_in_bits a - a
  let block :=     A
                ++ BitVec.zero v
                ++ C
                ++ BitVec.zero u
                ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 p)
  have h : 128 ∣ a + v + p + u + 64 + 64 := by
    rw [GCM.GCM_AE_DE_simplification1']
    simp only [u, v]
    simp only [GCM.ceiling_in_bits]
    rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_blocks p)
        (by apply GCM.bits_le_ceiling_in_bits)]
    rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a)
        (by apply GCM.bits_le_ceiling_in_bits)]
    omega
  let S := GHASH H block h
  let T := truncate t $ GCTR (m := 128) CIPH K J0 S
  (C, T)

def CIPH_128 : GCM.Cipher (n := 128) (m := 128) :=
  AES.AES_encrypt (Param := AES.AES128KBR)

def revCIPH (CIPH : BitVec n -> BitVec m -> BitVec n) (p : BitVec n) (k : BitVec m) :=
  (rev_elems n 8 (CIPH (rev_elems n 8 p (by sorry) (by sorry))
                         (rev_elems m 8 k (by sorry) (by sorry)))
       (by sorry) (by sorry))

def CIPH_128' : GCM.Cipher (n := 128) (m := 128) :=
  revCIPH CIPH_128

def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec a
  → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_128'

def K3   : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128
def IV3  : BitVec 96  := 0xcafebabefacedbaddecaf888#96
def P3   : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480
def A3   : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160
def C3   : BitVec 480 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480
def T3   : BitVec 128 := 0x5bc94fbc3221a5db94fae95ae7121a47#128

example : GCM_AE_128 K3 128 IV3 P3 A3 = (C3, T3) := by native_decide

[pennyannn]

Hi @hanno-becker , it's such a genius idea for getting rid of all the byte reversing functions. By treating the blocks from most significant block to least significant block, we essentially get rid of all the byte reversing functions (they sort of cancels out in the original version because of double reversing)! The code now looks just like the NIST specification. This is wonderful!
The only place we need to do byte-reversing is when calling AES and that is extracted into a single function revCIPH.
Thank you so much for suggesting this optimization!

I have updated the code to reflect all your comments. Let me know what you think.

[hanno-becker]

Thanks @pennyannn, LGTM!

[shigoel]

Thanks, @pennyannn, @hanno-becker, and @aqjune-aws!