From cecc7468e808fd5f6816e32ededa842dd42f1862 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 6 Mar 2024 12:07:02 -0800 Subject: [PATCH 1/6] Add specification for Advanced Encryption Standard (AES) --- Arm/Insts/DPSFP/Crypto_aes.lean | 101 +------------- Specs/AES.lean | 226 ++++++++++++++++++++++++++++++++ Specs/AESCommon.lean | 152 ++++++++++++++------- Tests/AESSpecTest.lean | 42 ++++++ Tests/Tests.lean | 1 + 5 files changed, 374 insertions(+), 148 deletions(-) create mode 100644 Specs/AES.lean create mode 100644 Tests/AESSpecTest.lean diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean index 32a8d09b..406674e9 100644 --- a/Arm/Insts/DPSFP/Crypto_aes.lean +++ b/Arm/Insts/DPSFP/Crypto_aes.lean @@ -8,6 +8,7 @@ Author(s): Shilpi Goel, Yan Peng import Arm.Decode import Arm.Insts.Common import Arm.BitVec +import Specs.AESCommon ---------------------------------------------------------------------- @@ -15,52 +16,6 @@ namespace DPSFP open BitVec -def SBox := - -- F E D C B A 9 8 7 6 5 4 3 2 1 0 - [ 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- F - 0xdf2855cee9871e9b948ed9691198f8e1#128, -- E - 0x9e1dc186b95735610ef6034866b53e70#128, -- D - 0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- C - 0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- B - 0x79e4959162acd3c25c2406490a3a32e0#128, -- A - 0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- 9 - 0x73195d643d7ea7c41744975fec130ccd#128, -- 8 - 0xd2f3ff1021dab6bcf5389d928f40a351#128, -- 7 - 0xa89f3c507f02f94585334d43fbaaefd0#128, -- 6 - 0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- 5 - 0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- 4 - 0x75b227ebe28012079a059618c323c704#128, -- 3 - 0x1531d871f1e5a534ccf73f362693fdb7#128, -- 2 - 0xc072a49cafa2d4adf04759fa7dc982ca#128, -- 1 - 0x76abd7fe2b670130c56f6bf27b777c63#128 -- 0 - ] - -def AESShiftRows (op : BitVec 128) : BitVec 128 := - extractLsb 95 88 op ++ extractLsb 55 48 op ++ - extractLsb 15 8 op ++ extractLsb 103 96 op ++ - extractLsb 63 56 op ++ extractLsb 23 16 op ++ - extractLsb 111 104 op ++ extractLsb 71 64 op ++ - extractLsb 31 24 op ++ extractLsb 119 112 op ++ - extractLsb 79 72 op ++ extractLsb 39 32 op ++ - extractLsb 127 120 op ++ extractLsb 87 80 op ++ - extractLsb 47 40 op ++ extractLsb 7 0 op - -def AESSubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128) - : BitVec 128 := - if h₀ : 16 <= i then - out - else - let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat - let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBox - have h₁ : idx * 8 + 7 - idx * 8 = i * 8 + 7 - i * 8 := by omega - let out := BitVec.partInstall (i * 8 + 7) (i * 8) (h₁ ▸ val) out - have _ : 15 - i < 16 - i := by omega - AESSubBytes_aux (i + 1) op out - termination_by (16 - i) - -def AESSubBytes (op : BitVec 128) : BitVec 128 := - AESSubBytes_aux 0 op (BitVec.zero 128) - @[state_simp_rules] def exec_aese (inst : Crypto_aes_cls) (s : ArmState) : ArmState := @@ -69,7 +24,7 @@ def exec_aese let operand1 := read_sfp 128 inst.Rd s let operand2 := read_sfp 128 inst.Rn s let result := operand1 ^^^ operand2 - let result := AESSubBytes $ AESShiftRows result + let result := AESCommon.SubBytes $ AESCommon.ShiftRows result -- State Updates let s := write_sfp 128 inst.Rd result s let s := write_pc ((read_pc s) + 4#64) s @@ -125,58 +80,8 @@ def FFmul03 (b : BitVec 8) : BitVec 8 := have h : hi - lo + 1 = 8 := by omega h ▸ extractLsb hi lo $ BitVec.flatten FFmul_03 -def AESMixColumns_aux (c : Nat) - (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32) - (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32) - : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 := - if h₀ : 4 <= c then - (out0, out1, out2, out3) - else - let lo := c * 8 - let hi := lo + 7 - have h₁ : hi - lo + 1 = 8 := by omega - let in0_byte := h₁ ▸ extractLsb hi lo in0 - let in1_byte := h₁ ▸ extractLsb hi lo in1 - let in2_byte := h₁ ▸ extractLsb hi lo in2 - let in3_byte := h₁ ▸ extractLsb hi lo in3 - let val0 := h₁.symm ▸ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte) - let out0 := BitVec.partInstall hi lo val0 out0 - let val1 := h₁.symm ▸ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte) - let out1 := BitVec.partInstall hi lo val1 out1 - let val2 := h₁.symm ▸ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte) - let out2 := BitVec.partInstall hi lo val2 out2 - let val3 := h₁.symm ▸ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte) - let out3 := BitVec.partInstall hi lo val3 out3 - have _ : 3 - c < 4 - c := by omega - AESMixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3 - termination_by (4 - c) - def AESMixColumns (op : BitVec 128) : BitVec 128 := - let in0 := - extractLsb 103 96 op ++ extractLsb 71 64 op ++ - extractLsb 39 32 op ++ extractLsb 7 0 op - let in1 := - extractLsb 111 104 op ++ extractLsb 79 72 op ++ - extractLsb 47 40 op ++ extractLsb 15 8 op - let in2 := - extractLsb 119 112 op ++ extractLsb 87 80 op ++ - extractLsb 55 48 op ++ extractLsb 23 16 op - let in3 := - extractLsb 127 120 op ++ extractLsb 95 88 op ++ - extractLsb 63 56 op ++ extractLsb 31 24 op - let (out0, out1, out2, out3) := - (BitVec.zero 32, BitVec.zero 32, - BitVec.zero 32, BitVec.zero 32) - let (out0, out1, out2, out3) := - AESMixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3 - extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++ - extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++ - extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++ - extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++ - extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++ - extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++ - extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++ - extractLsb 7 0 out1 ++ extractLsb 7 0 out0 + AESCommon.MixColumns op FFmul02 FFmul03 @[state_simp_rules] def exec_aesmc diff --git a/Specs/AES.lean b/Specs/AES.lean new file mode 100644 index 00000000..21f7958e --- /dev/null +++ b/Specs/AES.lean @@ -0,0 +1,226 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +import Arm.BitVec +import Arm.Insts.DPSFP.Crypto_aes +import Specs.AESCommon + +-- References : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf +-- https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/aes-development/rijndael-ammended.pdf +-- +-------------------------------------------------- +-- The NIST specification has the following rounds: +-- +-- AddRoundKey key0 +-- for k in key1 to key9 +-- SubBytes +-- ShiftRows +-- MixColumns +-- AddRoundKey +-- SubBytes +-- ShiftRows +-- AddRoundKey key10 +-- +-- The Arm implementation has an optimization that shifts the rounds: +-- +-- for k in key0 to key8 +-- AddRoundKey + ShiftRows + SubBytes (AESE k) +-- MixColumns (AESMC) +-- AddRoundKey + ShiftRows + SubBytes (AESE key9) +-- AddRoundKey key10 +-- +-- Note: SubBytes and ShiftRows are commutative because +-- SubBytes is a byte-wise operation +-- +-------------------------------------------------- + +namespace AES + +open BitVec + +def WordSize := 32 +def BlockSize := 128 + +-- Maybe consider Lists vs Vectors? +-- https://github.com/joehendrix/lean-crypto/blob/323ee9b1323deed5240762f4029700a246ecd9d5/lib/Crypto/Vector.lean#L96 +def Rcon : List (BitVec WordSize) := +[ 0x00000001#32, + 0x00000002#32, + 0x00000004#32, + 0x00000008#32, + 0x00000010#32, + 0x00000020#32, + 0x00000040#32, + 0x00000080#32, + 0x0000001b#32, + 0x00000036#32 ] + +------------------------------------------------------- +-- types + +-- Key-Block-Round Combinations +structure KBR where + key_len : Nat + block_size : Nat + Nk := key_len / 32 + Nb := block_size / 32 + Nr : Nat + h : block_size = BlockSize +deriving DecidableEq, Repr + +def AES128KBR : KBR := + {key_len := 128, block_size := BlockSize, Nr := 10, h := by decide} +def AES192KBR : KBR := + {key_len := 192, block_size := BlockSize, Nr := 12, h := by decide} +def AES256KBR : KBR := + {key_len := 256, block_size := BlockSize, Nr := 14, h := by decide} + +def KeySchedule : Type := List (BitVec WordSize) + +-- Declare KeySchedule to be an instance HAppend +-- so we can apply `++` to KeySchedules propertly +instance : HAppend KeySchedule KeySchedule KeySchedule where + hAppend := List.append + +------------------------------------------------------- + +def sbox (ind : BitVec 8) : BitVec 8 := + match_bv ind with + | [x:4, y:4] => + have h : (x.toNat * 128 + y.toNat * 8 + 7) - (x.toNat * 128 + y.toNat * 8) + 1 = 8 := + by omega + h ▸ extractLsb + (x.toNat * 128 + y.toNat * 8 + 7) + (x.toNat * 128 + y.toNat * 8) $ BitVec.flatten AESCommon.SBOX + | _ => ind -- unreachable case + +-- Little endian +def RotWord (w : BitVec WordSize) : BitVec WordSize := + match_bv w with + | [a3:8, a2:8, a1:8, a0:8] => a0 ++ a3 ++ a2 ++ a1 + | _ => w -- unreachable case + +def SubWord (w : BitVec WordSize) : BitVec WordSize := + match_bv w with + | [a3:8, a2:8, a1:8, a0:8] => (sbox a3) ++ (sbox a2) ++ (sbox a1) ++ (sbox a0) + | _ => w -- unreachable case + +protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len) + (acc : KeySchedule) : KeySchedule := + if h₀ : Param.Nk ≤ i then acc + else + have h₁ : i * 32 + 32 - 1 - i * 32 + 1 = WordSize := by + simp only [WordSize]; omega + let wd := h₁ ▸ extractLsb (i * 32 + 32 - 1) (i * 32) key + let (x:KeySchedule) := [wd] + have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega + AES.InitKey (Param := Param) (i + 1) key (acc ++ x) + termination_by (Param.Nk - i) + +protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule) + : KeySchedule := + if h : 4 * Param.Nr + 4 ≤ i then + ks + else + let tmp := List.get! ks (i - 1) + let tmp := + if i % Param.Nk == 0 then + (SubWord (RotWord tmp)) ^^^ (List.get! Rcon $ (i / Param.Nk) - 1) + else if Param.Nk > 6 && i % Param.Nk == 4 then + SubWord tmp + else + tmp + let res := (List.get! ks (i - Param.Nk)) ^^^ tmp + let ks := List.append ks [ res ] + have _ : 4 * Param.Nr + 4 - (i + 1) < 4 * Param.Nr + 4 - i := by omega + AES.KeyExpansion_helper (Param := Param) (i + 1) ks + termination_by (4 * Param.Nr + 4 - i) + +def KeyExpansion {Param : KBR} (key : BitVec Param.key_len) + : KeySchedule := + let seeded := AES.InitKey (Param := Param) 0 key [] + AES.KeyExpansion_helper (Param := Param) Param.Nk seeded + +def SubBytes {Param : KBR} (state : BitVec Param.block_size) + : BitVec Param.block_size := + have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] + h ▸ AESCommon.SubBytes (h ▸ state) + +def ShiftRows {Param : KBR} (state : BitVec Param.block_size) + : BitVec Param.block_size := + have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] + h ▸ AESCommon.ShiftRows (h ▸ state) + +def XTimes (bv : BitVec 8) : BitVec 8 := + let res := extractLsb 6 0 bv ++ 0b0#1 + if extractLsb 7 7 bv == 0b0#1 then res else res ^^^ 0b00011011#8 + +def MixColumns {Param : KBR} (state : BitVec Param.block_size) + : BitVec Param.block_size := + have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] + let FFmul02 := fun (x : BitVec 8) => XTimes x + let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x + h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03 + +-- TODO : Prove the following lemma +theorem MixColumns_table_lookup_equiv {Param : KBR} + (state : BitVec Param.block_size): + have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] + MixColumns (Param := Param) state = h ▸ DPSFP.AESMixColumns (h ▸ state) := by + simp only [MixColumns, DPSFP.AESMixColumns] + have h₀ : (fun x => XTimes x) = DPSFP.FFmul02 := by + funext x + simp only [XTimes, DPSFP.FFmul02] + simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil, + Nat.reduceSucc, Nat.reduceMul] + sorry -- looks like a sat problem + have h₁ : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by + funext x + simp only [XTimes, DPSFP.FFmul03] + simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil, + Nat.reduceSucc, Nat.reduceMul] + sorry -- looks like a sat problem + rw [h₀, h₁] + +def AddRoundKey {Param : KBR} (state : BitVec Param.block_size) + (roundKey : BitVec Param.block_size) : BitVec Param.block_size := + state ^^^ roundKey + +protected def getKey {Param : KBR} (n : Nat) (w : KeySchedule) : BitVec Param.block_size := + let ind := 4 * n + have h : WordSize + WordSize + WordSize + WordSize = Param.block_size := by + simp only [WordSize, BlockSize, Param.h] + h ▸ ((List.get! w (ind + 3)) ++ (List.get! w (ind + 2)) ++ + (List.get! w (ind + 1)) ++ (List.get! w ind)) + +protected def AES_encrypt_with_ks_loop {Param : KBR} (round : Nat) + (state : BitVec Param.block_size) (w : KeySchedule) + : BitVec Param.block_size := + if Param.Nr ≤ round then + state + else + let state := SubBytes state + let state := ShiftRows state + let state := MixColumns state + let state := AddRoundKey state $ AES.getKey round w + AES.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w + termination_by (Param.Nr - round) + +def AES_encrypt_with_ks {Param : KBR} (input : BitVec Param.block_size) + (w : KeySchedule) : BitVec Param.block_size := + have h₀ : WordSize + WordSize + WordSize + WordSize = Param.block_size := by + simp only [WordSize, BlockSize, Param.h] + let state := AddRoundKey input $ (h₀ ▸ AES.getKey 0 w) + let state := AES.AES_encrypt_with_ks_loop (Param := Param) 1 state w + let state := SubBytes (Param := Param) state + let state := ShiftRows (Param := Param) state + AddRoundKey state $ h₀ ▸ AES.getKey Param.Nr w + +def AES_encrypt {Param : KBR} (input : BitVec Param.block_size) + (key : BitVec Param.key_len) : BitVec Param.block_size := + let ks := KeyExpansion (Param := Param) key + AES_encrypt_with_ks (Param := Param) input ks + +end AES diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean index dbfb20be..cffaae16 100644 --- a/Specs/AESCommon.lean +++ b/Specs/AESCommon.lean @@ -5,60 +5,112 @@ Author(s): Shilpi Goel -/ import Arm.BitVec -namespace aes_helpers +namespace AESCommon open BitVec -def aes_shift_rows (op : BitVec 128) : BitVec 128 := - let op_7_0 := extractLsb 7 0 op - let op_47_40 := extractLsb 47 40 op - let op_87_80 := extractLsb 87 80 op - let op_127_120 := extractLsb 127 120 op - let op_39_32 := extractLsb 39 32 op - let op_79_72 := extractLsb 79 72 op - let op_119_112 := extractLsb 119 112 op - let op_31_24 := extractLsb 31 24 op - let op_71_64 := extractLsb 71 64 op - let op_111_104 := extractLsb 111 104 op - let op_23_16 := extractLsb 23 16 op - let op_63_56 := extractLsb 63 56 op - let op_103_96 := extractLsb 103 96 op - let op_15_8 := extractLsb 15 8 op - let op_55_48 := extractLsb 55 48 op - let op_95_88 := extractLsb 95 88 op - (op_95_88 ++ op_55_48 ++ op_15_8 ++ op_103_96 ++ op_63_56 ++ - op_23_16 ++ op_111_104 ++ op_71_64 ++ op_31_24 ++ op_119_112 ++ - op_79_72 ++ op_39_32 ++ op_127_120 ++ op_87_80 ++ op_47_40 ++ - op_7_0) +------------------------------------------------------- +-- Constants --- S-box values -def gf2_list : List (BitVec 128) := - [ - 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- <127:0> - 0xdf2855cee9871e9b948ed9691198f8e1#128, -- <127:0> - 0x9e1dc186b95735610ef6034866b53e70#128, -- <127:0> - 0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- <127:0> - 0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- <127:0> - 0x79e4959162acd3c25c2406490a3a32e0#128, -- <127:0> - 0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- <127:0> - 0x73195d643d7ea7c41744975fec130ccd#128, -- <127:0> - 0xd2f3ff1021dab6bcf5389d928f40a351#128, -- <127:0> - 0xa89f3c507f02f94585334d43fbaaefd0#128, -- <127:0> - 0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- <127:0> - 0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- <127:0> - 0x75b227ebe28012079a059618c323c704#128, -- <127:0> - 0x1531d871f1e5a534ccf73f362693fdb7#128, -- <127:0> - 0xc072a49cafa2d4adf04759fa7dc982ca#128, -- <127:0> - 0x76abd7fe2b670130c56f6bf27b777c63#128 -- <127:0> - ] +def SBOX := + -- F E D C B A 9 8 7 6 5 4 3 2 1 0 + [ 0x16bb54b00f2d99416842e6bf0d89a18c#128, -- F + 0xdf2855cee9871e9b948ed9691198f8e1#128, -- E + 0x9e1dc186b95735610ef6034866b53e70#128, -- D + 0x8a8bbd4b1f74dde8c6b4a61c2e2578ba#128, -- C + 0x08ae7a65eaf4566ca94ed58d6d37c8e7#128, -- B + 0x79e4959162acd3c25c2406490a3a32e0#128, -- A + 0xdb0b5ede14b8ee4688902a22dc4f8160#128, -- 9 + 0x73195d643d7ea7c41744975fec130ccd#128, -- 8 + 0xd2f3ff1021dab6bcf5389d928f40a351#128, -- 7 + 0xa89f3c507f02f94585334d43fbaaefd0#128, -- 6 + 0xcf584c4a39becb6a5bb1fc20ed00d153#128, -- 5 + 0x842fe329b3d63b52a05a6e1b1a2c8309#128, -- 4 + 0x75b227ebe28012079a059618c323c704#128, -- 3 + 0x1531d871f1e5a534ccf73f362693fdb7#128, -- 2 + 0xc072a49cafa2d4adf04759fa7dc982ca#128, -- 1 + 0x76abd7fe2b670130c56f6bf27b777c63#128 -- 0 + ] -def bitvec_list_concat (xs : List (BitVec n)) : BitVec (n * List.length xs) := - match xs with - | [] => 0#0 - | x :: rest => - have h1: (n + n * List.length rest) = (n * List.length (x :: rest)) := by sorry - h1 ▸ (x ++ (bitvec_list_concat rest)) +def ShiftRows (op : BitVec 128) : BitVec 128 := + extractLsb 95 88 op ++ extractLsb 55 48 op ++ + extractLsb 15 8 op ++ extractLsb 103 96 op ++ + extractLsb 63 56 op ++ extractLsb 23 16 op ++ + extractLsb 111 104 op ++ extractLsb 71 64 op ++ + extractLsb 31 24 op ++ extractLsb 119 112 op ++ + extractLsb 79 72 op ++ extractLsb 39 32 op ++ + extractLsb 127 120 op ++ extractLsb 87 80 op ++ + extractLsb 47 40 op ++ extractLsb 7 0 op -def gf2 : BitVec (128 * 16) := bitvec_list_concat gf2_list +def SubBytes_aux (i : Nat) (op : BitVec 128) (out : BitVec 128) + : BitVec 128 := + if h₀ : 16 <= i then + out + else + let idx := (extractLsb (i * 8 + 7) (i * 8) op).toNat + let val := extractLsb (idx * 8 + 7) (idx * 8) $ BitVec.flatten SBOX + have h₁ : idx * 8 + 7 - idx * 8 = i * 8 + 7 - i * 8 := by omega + let out := BitVec.partInstall (i * 8 + 7) (i * 8) (h₁ ▸ val) out + have _ : 15 - i < 16 - i := by omega + SubBytes_aux (i + 1) op out + termination_by (16 - i) -end aes_helpers +def SubBytes (op : BitVec 128) : BitVec 128 := + SubBytes_aux 0 op (BitVec.zero 128) + +def MixColumns_aux (c : Nat) + (in0 : BitVec 32) (in1 : BitVec 32) (in2 : BitVec 32) (in3 : BitVec 32) + (out0 : BitVec 32) (out1 : BitVec 32) (out2 : BitVec 32) (out3 : BitVec 32) + (FFmul02 : BitVec 8 -> BitVec 8) (FFmul03 : BitVec 8 -> BitVec 8) + : BitVec 32 × BitVec 32 × BitVec 32 × BitVec 32 := + if h₀ : 4 <= c then + (out0, out1, out2, out3) + else + let lo := c * 8 + let hi := lo + 7 + have h₁ : hi - lo + 1 = 8 := by omega + let in0_byte := h₁ ▸ extractLsb hi lo in0 + let in1_byte := h₁ ▸ extractLsb hi lo in1 + let in2_byte := h₁ ▸ extractLsb hi lo in2 + let in3_byte := h₁ ▸ extractLsb hi lo in3 + let val0 := h₁.symm ▸ (FFmul02 in0_byte ^^^ FFmul03 in1_byte ^^^ in2_byte ^^^ in3_byte) + let out0 := BitVec.partInstall hi lo val0 out0 + let val1 := h₁.symm ▸ (FFmul02 in1_byte ^^^ FFmul03 in2_byte ^^^ in3_byte ^^^ in0_byte) + let out1 := BitVec.partInstall hi lo val1 out1 + let val2 := h₁.symm ▸ (FFmul02 in2_byte ^^^ FFmul03 in3_byte ^^^ in0_byte ^^^ in1_byte) + let out2 := BitVec.partInstall hi lo val2 out2 + let val3 := h₁.symm ▸ (FFmul02 in3_byte ^^^ FFmul03 in0_byte ^^^ in1_byte ^^^ in2_byte) + let out3 := BitVec.partInstall hi lo val3 out3 + have _ : 3 - c < 4 - c := by omega + MixColumns_aux (c + 1) in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 + termination_by (4 - c) + +def MixColumns (op : BitVec 128) (FFmul02 : BitVec 8 -> BitVec 8) + (FFmul03 : BitVec 8 -> BitVec 8) : BitVec 128 := + let in0 := + extractLsb 103 96 op ++ extractLsb 71 64 op ++ + extractLsb 39 32 op ++ extractLsb 7 0 op + let in1 := + extractLsb 111 104 op ++ extractLsb 79 72 op ++ + extractLsb 47 40 op ++ extractLsb 15 8 op + let in2 := + extractLsb 119 112 op ++ extractLsb 87 80 op ++ + extractLsb 55 48 op ++ extractLsb 23 16 op + let in3 := + extractLsb 127 120 op ++ extractLsb 95 88 op ++ + extractLsb 63 56 op ++ extractLsb 31 24 op + let (out0, out1, out2, out3) := + (BitVec.zero 32, BitVec.zero 32, + BitVec.zero 32, BitVec.zero 32) + let (out0, out1, out2, out3) := + MixColumns_aux 0 in0 in1 in2 in3 out0 out1 out2 out3 FFmul02 FFmul03 + extractLsb 31 24 out3 ++ extractLsb 31 24 out2 ++ + extractLsb 31 24 out1 ++ extractLsb 31 24 out0 ++ + extractLsb 23 16 out3 ++ extractLsb 23 16 out2 ++ + extractLsb 23 16 out1 ++ extractLsb 23 16 out0 ++ + extractLsb 15 8 out3 ++ extractLsb 15 8 out2 ++ + extractLsb 15 8 out1 ++ extractLsb 15 8 out0 ++ + extractLsb 7 0 out3 ++ extractLsb 7 0 out2 ++ + extractLsb 7 0 out1 ++ extractLsb 7 0 out0 + +end AESCommon diff --git a/Tests/AESSpecTest.lean b/Tests/AESSpecTest.lean new file mode 100644 index 00000000..a8e2fa64 --- /dev/null +++ b/Tests/AESSpecTest.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ + +import Specs.AES +import Arm.BitVec + +-- Reference : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf Section B + +-- Testing AES-128 encryption of one message block + +namespace AESSpecTest + +open BitVec + +-- The specification expects little-endian input +protected def input : BitVec 128 := + BitVec.flatten + [ 0x32#8, 0x43#8, 0xf6#8, 0xa8#8, + 0x88#8, 0x5a#8, 0x30#8, 0x8d#8, + 0x31#8, 0x31#8, 0x98#8, 0xa2#8, + 0xe0#8, 0x37#8, 0x07#8, 0x34#8 ].reverse + +protected def key : BitVec 128 := + BitVec.flatten + [ 0x2b#8, 0x7e#8, 0x15#8, 0x16#8, + 0x28#8, 0xae#8, 0xd2#8, 0xa6#8, + 0xab#8, 0xf7#8, 0x15#8, 0x88#8, + 0x09#8, 0xcf#8, 0x4f#8, 0x3c#8 ].reverse + +protected def output : BitVec 128 := + BitVec.flatten + [ 0x39#8, 0x25#8, 0x84#8, 0x1d#8, + 0x02#8, 0xdc#8, 0x09#8, 0xfb#8, + 0xdc#8, 0x11#8, 0x85#8, 0x97#8, + 0x19#8, 0x6a#8, 0x0b#8, 0x32#8 ].reverse + +example : AES.AES_encrypt (Param := AES.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide + +end AESSpecTest diff --git a/Tests/Tests.lean b/Tests/Tests.lean index a1ae7724..767bc04a 100644 --- a/Tests/Tests.lean +++ b/Tests/Tests.lean @@ -9,4 +9,5 @@ import «Tests».SHA512SpecTest -- import «Tests».SHA512StandardSpecTest import «Tests».SHA512ProgramTest import «Tests».LDSTTest +import «Tests».AESSpecTest From 9791f50a1d53d512beb32b2781efe756d43d6aa1 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 14 Mar 2024 18:01:34 -0700 Subject: [PATCH 2/6] Add specification for Galois/Counter Mode (GCM) --- Arm/Insts/DPSFP/Crypto_aes.lean | 6 +- Specs/AES.lean | 39 ++++--- Specs/AESCommon.lean | 2 +- Specs/GCM.lean | 198 ++++++++++++++++++++++++++++++++ Specs/Specs.lean | 2 + Tests/AESGCMSpecTest.lean | 166 ++++++++++++++++++++++++++ Tests/Tests.lean | 1 + 7 files changed, 390 insertions(+), 24 deletions(-) create mode 100644 Specs/GCM.lean create mode 100644 Tests/AESGCMSpecTest.lean diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean index 406674e9..c6cff4e3 100644 --- a/Arm/Insts/DPSFP/Crypto_aes.lean +++ b/Arm/Insts/DPSFP/Crypto_aes.lean @@ -52,8 +52,7 @@ def FFmul02 (b : BitVec 8) : BitVec 8 := ] let lo := b.toNat * 8 let hi := lo + 7 - have h : hi - lo + 1 = 8 := by omega - h ▸ extractLsb hi lo $ BitVec.flatten FFmul_02 + BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_02 def FFmul03 (b : BitVec 8) : BitVec 8 := let FFmul_03 := @@ -77,8 +76,7 @@ def FFmul03 (b : BitVec 8) : BitVec 8 := ] let lo := b.toNat * 8 let hi := lo + 7 - have h : hi - lo + 1 = 8 := by omega - h ▸ extractLsb hi lo $ BitVec.flatten FFmul_03 + BitVec.cast (by omega) $ extractLsb hi lo $ BitVec.flatten FFmul_03 def AESMixColumns (op : BitVec 128) : BitVec 128 := AESCommon.MixColumns op FFmul02 FFmul03 diff --git a/Specs/AES.lean b/Specs/AES.lean index 21f7958e..7eb13640 100644 --- a/Specs/AES.lean +++ b/Specs/AES.lean @@ -23,7 +23,7 @@ import Specs.AESCommon -- ShiftRows -- AddRoundKey key10 -- --- The Arm implementation has an optimization that shifts the rounds: +-- The Arm implementation has an optimization that commute intermediate steps: -- -- for k in key0 to key8 -- AddRoundKey + ShiftRows + SubBytes (AESE k) @@ -43,8 +43,9 @@ open BitVec def WordSize := 32 def BlockSize := 128 --- Maybe consider Lists vs Vectors? +-- General comment: Maybe consider Lists vs Vectors? -- https://github.com/joehendrix/lean-crypto/blob/323ee9b1323deed5240762f4029700a246ecd9d5/lib/Crypto/Vector.lean#L96 + def Rcon : List (BitVec WordSize) := [ 0x00000001#32, 0x00000002#32, @@ -96,7 +97,7 @@ def sbox (ind : BitVec 8) : BitVec 8 := (x.toNat * 128 + y.toNat * 8) $ BitVec.flatten AESCommon.SBOX | _ => ind -- unreachable case --- Little endian +-- Note: The RotWord function is written in little endian def RotWord (w : BitVec WordSize) : BitVec WordSize := match_bv w with | [a3:8, a2:8, a1:8, a0:8] => a0 ++ a3 ++ a2 ++ a1 @@ -154,8 +155,8 @@ def ShiftRows {Param : KBR} (state : BitVec Param.block_size) h ▸ AESCommon.ShiftRows (h ▸ state) def XTimes (bv : BitVec 8) : BitVec 8 := - let res := extractLsb 6 0 bv ++ 0b0#1 - if extractLsb 7 7 bv == 0b0#1 then res else res ^^^ 0b00011011#8 + let res := truncate 7 bv ++ 0b0#1 + if getLsb bv 7 then res ^^^ 0b00011011#8 else res def MixColumns {Param : KBR} (state : BitVec Param.block_size) : BitVec Param.block_size := @@ -164,25 +165,25 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size) let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03 --- TODO : Prove the following lemma +-- TODO: looks like a SAT/SMT problem +protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by + funext x + simp only [XTimes, DPSFP.FFmul02] + sorry + +-- TODO: looks like a SAT/SMT problem +protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by + funext x + simp only [XTimes, DPSFP.FFmul03] + sorry + + theorem MixColumns_table_lookup_equiv {Param : KBR} (state : BitVec Param.block_size): have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] MixColumns (Param := Param) state = h ▸ DPSFP.AESMixColumns (h ▸ state) := by simp only [MixColumns, DPSFP.AESMixColumns] - have h₀ : (fun x => XTimes x) = DPSFP.FFmul02 := by - funext x - simp only [XTimes, DPSFP.FFmul02] - simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil, - Nat.reduceSucc, Nat.reduceMul] - sorry -- looks like a sat problem - have h₁ : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by - funext x - simp only [XTimes, DPSFP.FFmul03] - simp only [Nat.reduceSub, Nat.reduceAdd, beq_iff_eq, Nat.sub_zero, List.length_cons, List.length_nil, - Nat.reduceSucc, Nat.reduceMul] - sorry -- looks like a sat problem - rw [h₀, h₁] + rw [AES.FFmul02_equiv, AES.FFmul03_equiv] def AddRoundKey {Param : KBR} (state : BitVec Param.block_size) (roundKey : BitVec Param.block_size) : BitVec Param.block_size := diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean index cffaae16..5d2f8c58 100644 --- a/Specs/AESCommon.lean +++ b/Specs/AESCommon.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Shilpi Goel +Author(s): Shilpi Goel, Yan Peng -/ import Arm.BitVec diff --git a/Specs/GCM.lean b/Specs/GCM.lean new file mode 100644 index 00000000..ed5d77f7 --- /dev/null +++ b/Specs/GCM.lean @@ -0,0 +1,198 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +import Arm.BitVec +import Arm.Insts.Common + +-- References: https://nvlpubs.nist.gov/nistpubs/legacy/sp/nistspecialpublication800-38d.pdf + +namespace GCM + +open BitVec + +def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120 + +/-- A Cipher type is a function that takes an input of size n and + a key of size m and returns an encrypted block of size n -/ +abbrev Cipher {n : Nat} {m : Nat} := BitVec n → BitVec m → BitVec n + +/-- The s-bit incrementing function -/ +def inc_s (s : Nat) (X : BitVec l) (H₀ : 0 < s) (H₁ : s < l) : BitVec l := + let msb_hi := l - 1 + let msb_lo := s + let lsb_hi := s - 1 + let lsb_lo := 0 + have h₁ : lsb_hi - lsb_lo + 1 = s := by omega + let upper := extractLsb msb_hi msb_lo X + let lower := h₁ ▸ (extractLsb lsb_hi lsb_lo X) + 0b1#s + have h₂ : msb_hi - msb_lo + 1 + s = l := by omega + h₂ ▸ (upper ++ lower) + +def mul_aux (i : Nat) (X : BitVec 128) (Z : BitVec 128) (V : BitVec 128) + : BitVec 128 := + if h : 128 ≤ i then + Z + else + let Xi := getMsb X i + let Z := if not Xi then Z else Z ^^^ V + let lsb_v := getLsb V 0 + let V := if not lsb_v then V >>> 1 else (V >>> 1) ^^^ R + mul_aux (i + 1) X Z V + termination_by (128 - i) + +/-- The GF(2^128) multiplication -/ +def mul (X : BitVec 128) (Y : BitVec 128) : BitVec 128 := + mul_aux 0 X 0b0#128 Y + +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 := i * 128 + let hi := lo + 127 + have h₀ : hi - lo + 1 = 128 := by omega + let Xi := extractLsb hi lo X + let res := rev_elems 128 8 (Y ^^^ (h₀ ▸ Xi)) (by decide) (by decide) + let H_rev := rev_elems 128 8 H (by decide) (by decide) + let Y := mul res H_rev + let Y := rev_elems 128 8 Y (by decide) (by decide) + 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 := i * 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 ICB_rev := rev_elems 128 8 ICB (by decide) (by decide) + let Yi := h ▸ Xi ^^^ CIPH ICB_rev 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_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 {m : Nat} (CIPH : Cipher (n := 128) (m := m)) + (K : BitVec m) (ICB : BitVec 128) (X : BitVec v) : (BitVec v) := + let n := GCM.ceiling_in_blocks v + GCTR_aux CIPH 0 n K ICB X $ BitVec.zero v + +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_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 {m : Nat} (CIPH : Cipher (n := 128) (m := m)) + (K : BitVec m) (IV : BitVec lv) (P : BitVec p) (A : BitVec a) (t : Nat) + : (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 := m) CIPH K ICB P + let u := GCM.ceiling_in_bits p - p + let v := GCM.ceiling_in_bits a - a + let block := rev_elems 64 8 (BitVec.ofNat 64 p) (by decide) (by decide) + ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide) + ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A + have h : 128 ∣ 64 + 64 + u + p + v + a := 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 := m) CIPH K J0 S + (C, T) + +def length_constraints (_IV : BitVec v) (_A : BitVec a) (_C : BitVec c) + : Bool := + 1 ≤ v && v ≤ 2^64 - 1 + && c ≤ 2^39 - 256 + && a ≤ 2^64 - 1 + +/-- GCM_AD : Galois Counter Mode Authenticated Decryption + GCM_AD returns none when decryption fails. -/ +def GCM_AD {m : Nat} (CIPH : Cipher (n := 128) (m := m)) + (K : BitVec m) (IV : BitVec lv) (C : BitVec c) (A : BitVec a) (T : BitVec t) + : Option (BitVec c) := + if not $ length_constraints IV C A then + none + else + let H := CIPH (BitVec.zero 128) K + let J0 := GCM.initialize_J0 H IV + let ICB := inc_s 32 J0 (by decide) (by decide) + let P := GCTR (m := m) CIPH K ICB C + let u := GCM.ceiling_in_bits c - c + let v := GCM.ceiling_in_bits a - a + let block := rev_elems 64 8 (BitVec.ofNat 64 c) (by decide) (by decide) + ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide) + ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A + have h : 128 ∣ 64 + 64 + u + c + v + a := by + rw [GCM.GCM_AE_DE_simplification1] + simp only [u, v] + simp only [GCM.ceiling_in_bits] + rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_blocks c) + (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 := m) CIPH K J0 S + if T == T' then some P else none + +end GCM diff --git a/Specs/Specs.lean b/Specs/Specs.lean index 8ef481da..9586f35f 100644 --- a/Specs/Specs.lean +++ b/Specs/Specs.lean @@ -5,3 +5,5 @@ Author(s): Shilpi Goel -/ import «Specs».SHA512 import «Specs».AESCommon +import «Specs».AES +import «Specs».GCM diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean new file mode 100644 index 00000000..2340aff3 --- /dev/null +++ b/Tests/AESGCMSpecTest.lean @@ -0,0 +1,166 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +import Arm.BitVec +import Specs.AES +import Specs.GCM + +-- Reference: https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf + +namespace AES256GCMSpecTest + +open BitVec + +def CIPH_128 : GCM.Cipher (n := 128) (m := 128) := + AES.AES_encrypt (Param := AES.AES128KBR) + +def GCM_AE_128 : BitVec 128 → BitVec lv → BitVec p → BitVec a → (t : Nat) + → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 128) CIPH_128 + +def GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t + → Option (BitVec c) := GCM.GCM_AD (m := 128) CIPH_128 + +def CIPH_256 : GCM.Cipher (n := 128) (m := 256) := + AES.AES_encrypt (Param := AES.AES256KBR) + +def GCM_AE_256 : BitVec 256 → BitVec lv → BitVec p → BitVec a → (t : Nat) + → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 256) CIPH_256 + +def GCM_AD_256 : BitVec 256 → BitVec lv → BitVec c → BitVec a → BitVec t + → Option (BitVec c) := GCM.GCM_AD (m := 256) CIPH_256 + +-- Test Vector 0 + +def K0 : BitVec 128 := 0 +def IV0 : BitVec 96 := 0 +def P0 : BitVec 0 := BitVec.nil +def A0 : BitVec 0 := BitVec.nil +def C0 : BitVec 0 := BitVec.nil +def T0 : BitVec 128 := rev_elems 128 8 0x58e2fccefa7e3061367f1d57a4e7455a#128 (by decide) (by decide) +example : GCM_AE_128 K0 IV0 P0 A0 128 = (C0, T0) := by native_decide +example : GCM_AD_128 K0 IV0 C0 A0 T0 = P0 := by native_decide + +-- Test Vector 1 + +def K1 : BitVec 128 := 0 +def IV1 : BitVec 96 := 0 +def P1 : BitVec 128 := 0 +def A1 : BitVec 0 := BitVec.nil +def C1 : BitVec 128 := rev_elems 128 8 0x0388dace60b6a392f328c2b971b2fe78#128 (by decide) (by decide) +def T1 : BitVec 128 := rev_elems 128 8 0xab6e47d42cec13bdf53a67b21257bddf#128 (by decide) (by decide) +example : GCM_AE_128 K1 IV1 P1 A1 128 = (C1, T1) := by native_decide +example : GCM_AD_128 K1 IV1 C1 A1 T1 = P1 := by native_decide + +-- Test Vector 2 + +def K2 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def IV2 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P2 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def A2 : BitVec 0 := BitVec.nil +def C2 : BitVec 512 := rev_elems 512 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 (by decide) (by decide) +def T2 : BitVec 128 := rev_elems 128 8 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 (by decide) (by decide) +example : GCM_AE_128 K2 IV2 P2 A2 128 = (C2, T2) := by native_decide +example : GCM_AD_128 K2 IV2 C2 A2 T2 = P2 := by native_decide + +-- Test Vector 3 + +def K3 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def IV3 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P3 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A3 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C3 : BitVec 480 := rev_elems 480 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480 (by decide) (by decide) +def T3 : BitVec 128 := rev_elems 128 8 0x5bc94fbc3221a5db94fae95ae7121a47#128 (by decide) (by decide) +example : GCM_AE_128 K3 IV3 P3 A3 128 = (C3, T3) := by native_decide +example : GCM_AD_128 K3 IV3 C3 A3 T3 = P3 := by native_decide + +-- Test Vector 4 + +def K4 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def IV4 : BitVec 64 := 0xcafebabefacedbad#64 +def P4 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A4 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C4 : BitVec 480 := rev_elems 480 8 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 (by decide) (by decide) +def T4 : BitVec 128 := rev_elems 128 8 0x3612d2e79e3b0785561be14aaca2fccb#128 (by decide) (by decide) +example : GCM_AE_128 K4 IV4 P4 A4 128 = (C4, T4) := by native_decide +example : GCM_AD_128 K4 IV4 C4 A4 T4 = P4 := by native_decide + +-- Test Vector 5 + +def K5 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def IV5 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 +def P5 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A5 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C5 : BitVec 480 := rev_elems 480 8 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 (by decide) (by decide) +def T5 : BitVec 128 := rev_elems 128 8 0x619cc5aefffe0bfa462af43c1699d050#128 (by decide) (by decide) +example : GCM_AE_128 K5 IV5 P5 A5 128 = (C5, T5) := by native_decide +example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide + +-- Test Vector 6 + +def K6 : BitVec 256 := 0 +def IV6 : BitVec 96 := 0 +def P6 : BitVec 0 := BitVec.nil +def A6 : BitVec 0 := BitVec.nil +def C6 : BitVec 0 := BitVec.nil +def T6 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide) +example : GCM_AE_256 K6 IV6 P6 A6 128 = (C6, T6) := by native_decide +example : GCM_AD_256 K6 IV6 C6 A6 T6 = P6 := by native_decide + +-- Test Vector 7 + +def K7 : BitVec 256 := 0 +def IV7 : BitVec 96 := 0 +def P7 : BitVec 128 := 0 +def A7 : BitVec 0 := BitVec.nil +def C7 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide) +def T7 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide) +example : GCM_AE_256 K7 IV7 P7 A7 128 = (C7, T7) := by native_decide +example : GCM_AD_256 K7 IV7 C7 A7 T7 = P7 := by native_decide + +-- Test Vector 8 + +def K8 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P8 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def A8 : BitVec 0 := BitVec.nil +def C8 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide) +def T8 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide) +example : GCM_AE_256 K8 IV8 P8 A8 128 = (C8, T8) := by native_decide +example : GCM_AD_256 K8 IV8 C8 A8 T8 = P8 := by native_decide + +-- Test Vector 9 + +def K9 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P9 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A9 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C9 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide) +def T9 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide) +example : GCM_AE_256 K9 IV9 P9 A9 128 = (C9, T9) := by native_decide +example : GCM_AD_256 K9 IV9 C9 A9 T9 = P9 := by native_decide + +-- Test Vector 10 (17) + +def K10 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV10 : BitVec 64:= 0xcafebabefacedbad#64 +def P10 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A10 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C10 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide) +def T10 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide) +example : GCM_AE_256 K10 IV10 P10 A10 128 = (C10, T10) := by native_decide +example : GCM_AD_256 K10 IV10 C10 A10 T10 = P10 := by native_decide + +-- Test Vector 11 + +def K11 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 +def P11 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A11 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C11 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide) +def T11 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide) +example : GCM_AE_256 K11 IV11 P11 A11 128 = (C11, T11) := by native_decide +example : GCM_AD_256 K11 IV11 C11 A11 T11 = P11 := by native_decide + +end AES256GCMSpecTest diff --git a/Tests/Tests.lean b/Tests/Tests.lean index 767bc04a..723c8577 100644 --- a/Tests/Tests.lean +++ b/Tests/Tests.lean @@ -10,4 +10,5 @@ import «Tests».SHA512SpecTest import «Tests».SHA512ProgramTest import «Tests».LDSTTest import «Tests».AESSpecTest +import «Tests».AESGCMSpecTest From 5e5c600507ba109249a3bea81b7a5912665a2ea1 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 2 Apr 2024 13:16:45 -0700 Subject: [PATCH 3/6] Fix function signatures and add tests for AES-192-GCM --- Specs/GCM.lean | 8 +- Tests/AESGCMSpecTest.lean | 159 ++++++++++++++++++++++++++++---------- 2 files changed, 121 insertions(+), 46 deletions(-) diff --git a/Specs/GCM.lean b/Specs/GCM.lean index ed5d77f7..5248624d 100644 --- a/Specs/GCM.lean +++ b/Specs/GCM.lean @@ -95,7 +95,7 @@ protected theorem bits_le_ceiling_in_bits (w : Nat) : omega /-- GCTR: encrypting/decrypting message x using Galois counter mode -/ -def GCTR {m : Nat} (CIPH : Cipher (n := 128) (m := m)) +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 GCTR_aux CIPH 0 n K ICB X $ BitVec.zero v @@ -134,8 +134,8 @@ protected theorem GCM_AE_DE_simplification2 (x * 128 - y) + y = x * 128 := by omega /-- GCM_AE : Galois Counter Mode Authenticated Encryption -/ -def GCM_AE {m : Nat} (CIPH : Cipher (n := 128) (m := m)) - (K : BitVec m) (IV : BitVec lv) (P : BitVec p) (A : BitVec a) (t : Nat) +def GCM_AE (CIPH : Cipher (n := 128) (m := m)) + (K : BitVec m) (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 @@ -167,7 +167,7 @@ def length_constraints (_IV : BitVec v) (_A : BitVec a) (_C : BitVec c) /-- GCM_AD : Galois Counter Mode Authenticated Decryption GCM_AD returns none when decryption fails. -/ -def GCM_AD {m : Nat} (CIPH : Cipher (n := 128) (m := m)) +def GCM_AD (CIPH : Cipher (n := 128) (m := m)) (K : BitVec m) (IV : BitVec lv) (C : BitVec c) (A : BitVec a) (T : BitVec t) : Option (BitVec c) := if not $ length_constraints IV C A then diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean index 2340aff3..9c9f094c 100644 --- a/Tests/AESGCMSpecTest.lean +++ b/Tests/AESGCMSpecTest.lean @@ -16,20 +16,29 @@ open BitVec def CIPH_128 : GCM.Cipher (n := 128) (m := 128) := AES.AES_encrypt (Param := AES.AES128KBR) -def GCM_AE_128 : BitVec 128 → BitVec lv → BitVec p → BitVec a → (t : Nat) - → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 128) 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 GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t - → Option (BitVec c) := GCM.GCM_AD (m := 128) CIPH_128 + → Option (BitVec c) := GCM.GCM_AD CIPH_128 + +def CIPH_192 : GCM.Cipher (n := 128) (m := 192) := +AES.AES_encrypt (Param := AES.AES192KBR) + +def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec a + → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_192 + +def GCM_AD_192 : BitVec 192 → BitVec lv → BitVec c → BitVec a → BitVec t + → Option (BitVec c) := GCM.GCM_AD CIPH_192 def CIPH_256 : GCM.Cipher (n := 128) (m := 256) := AES.AES_encrypt (Param := AES.AES256KBR) -def GCM_AE_256 : BitVec 256 → BitVec lv → BitVec p → BitVec a → (t : Nat) - → (BitVec p) × (BitVec t) := GCM.GCM_AE (m := 256) CIPH_256 +def GCM_AE_256 : BitVec 256 → (t : Nat) → BitVec lv → BitVec p → BitVec a + → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_256 def GCM_AD_256 : BitVec 256 → BitVec lv → BitVec c → BitVec a → BitVec t - → Option (BitVec c) := GCM.GCM_AD (m := 256) CIPH_256 + → Option (BitVec c) := GCM.GCM_AD CIPH_256 -- Test Vector 0 @@ -39,7 +48,7 @@ def P0 : BitVec 0 := BitVec.nil def A0 : BitVec 0 := BitVec.nil def C0 : BitVec 0 := BitVec.nil def T0 : BitVec 128 := rev_elems 128 8 0x58e2fccefa7e3061367f1d57a4e7455a#128 (by decide) (by decide) -example : GCM_AE_128 K0 IV0 P0 A0 128 = (C0, T0) := by native_decide +example : GCM_AE_128 K0 128 IV0 P0 A0 = (C0, T0) := by native_decide example : GCM_AD_128 K0 IV0 C0 A0 T0 = P0 := by native_decide -- Test Vector 1 @@ -50,7 +59,7 @@ def P1 : BitVec 128 := 0 def A1 : BitVec 0 := BitVec.nil def C1 : BitVec 128 := rev_elems 128 8 0x0388dace60b6a392f328c2b971b2fe78#128 (by decide) (by decide) def T1 : BitVec 128 := rev_elems 128 8 0xab6e47d42cec13bdf53a67b21257bddf#128 (by decide) (by decide) -example : GCM_AE_128 K1 IV1 P1 A1 128 = (C1, T1) := by native_decide +example : GCM_AE_128 K1 128 IV1 P1 A1 = (C1, T1) := by native_decide example : GCM_AD_128 K1 IV1 C1 A1 T1 = P1 := by native_decide -- Test Vector 2 @@ -61,7 +70,7 @@ def P2 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a95 def A2 : BitVec 0 := BitVec.nil def C2 : BitVec 512 := rev_elems 512 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 (by decide) (by decide) def T2 : BitVec 128 := rev_elems 128 8 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 (by decide) (by decide) -example : GCM_AE_128 K2 IV2 P2 A2 128 = (C2, T2) := by native_decide +example : GCM_AE_128 K2 128 IV2 P2 A2 = (C2, T2) := by native_decide example : GCM_AD_128 K2 IV2 C2 A2 T2 = P2 := by native_decide -- Test Vector 3 @@ -72,7 +81,7 @@ def P3 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a95 def A3 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) def C3 : BitVec 480 := rev_elems 480 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480 (by decide) (by decide) def T3 : BitVec 128 := rev_elems 128 8 0x5bc94fbc3221a5db94fae95ae7121a47#128 (by decide) (by decide) -example : GCM_AE_128 K3 IV3 P3 A3 128 = (C3, T3) := by native_decide +example : GCM_AE_128 K3 128 IV3 P3 A3 = (C3, T3) := by native_decide example : GCM_AD_128 K3 IV3 C3 A3 T3 = P3 := by native_decide -- Test Vector 4 @@ -83,7 +92,7 @@ def P4 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a95 def A4 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) def C4 : BitVec 480 := rev_elems 480 8 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 (by decide) (by decide) def T4 : BitVec 128 := rev_elems 128 8 0x3612d2e79e3b0785561be14aaca2fccb#128 (by decide) (by decide) -example : GCM_AE_128 K4 IV4 P4 A4 128 = (C4, T4) := by native_decide +example : GCM_AE_128 K4 128 IV4 P4 A4 = (C4, T4) := by native_decide example : GCM_AD_128 K4 IV4 C4 A4 T4 = P4 := by native_decide -- Test Vector 5 @@ -94,73 +103,139 @@ def P5 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a95 def A5 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) def C5 : BitVec 480 := rev_elems 480 8 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 (by decide) (by decide) def T5 : BitVec 128 := rev_elems 128 8 0x619cc5aefffe0bfa462af43c1699d050#128 (by decide) (by decide) -example : GCM_AE_128 K5 IV5 P5 A5 128 = (C5, T5) := by native_decide +example : GCM_AE_128 K5 128 IV5 P5 A5 = (C5, T5) := by native_decide example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide -- Test Vector 6 -def K6 : BitVec 256 := 0 +def K6 : BitVec 192 := 0 def IV6 : BitVec 96 := 0 def P6 : BitVec 0 := BitVec.nil def A6 : BitVec 0 := BitVec.nil def C6 : BitVec 0 := BitVec.nil -def T6 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide) -example : GCM_AE_256 K6 IV6 P6 A6 128 = (C6, T6) := by native_decide -example : GCM_AD_256 K6 IV6 C6 A6 T6 = P6 := by native_decide +def T6 : BitVec 128 := rev_elems 128 8 0xcd33b28ac773f74ba00ed1f312572435#128 (by decide) (by decide) +example : GCM_AE_192 K6 128 IV6 P6 A6 = (C6, T6) := by native_decide +example : GCM_AD_192 K6 IV6 C6 A6 T6 = P6 := by native_decide -- Test Vector 7 -def K7 : BitVec 256 := 0 +def K7 : BitVec 192 := 0 def IV7 : BitVec 96 := 0 def P7 : BitVec 128 := 0 def A7 : BitVec 0 := BitVec.nil -def C7 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide) -def T7 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide) -example : GCM_AE_256 K7 IV7 P7 A7 128 = (C7, T7) := by native_decide -example : GCM_AD_256 K7 IV7 C7 A7 T7 = P7 := by native_decide +def C7 : BitVec 128 := rev_elems 128 8 0x98e7247c07f0fe411c267e4384b0f600#128 (by decide) (by decide) +def T7 : BitVec 128 := rev_elems 128 8 0x2ff58d80033927ab8ef4d4587514f0fb#128 (by decide) (by decide) +example : GCM_AE_192 K7 128 IV7 P7 A7 = (C7, T7) := by native_decide +example : GCM_AD_192 K7 IV7 C7 A7 T7 = P7 := by native_decide -- Test Vector 8 -def K8 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K8 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 def P8 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) def A8 : BitVec 0 := BitVec.nil -def C8 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide) -def T8 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide) -example : GCM_AE_256 K8 IV8 P8 A8 128 = (C8, T8) := by native_decide -example : GCM_AD_256 K8 IV8 C8 A8 T8 = P8 := by native_decide +def C8 : BitVec 512 := rev_elems 512 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512 (by decide) (by decide) +def T8 : BitVec 128 := rev_elems 128 8 0x9924a7c8587336bfb118024db8674a14#128 (by decide) (by decide) +example : GCM_AE_192 K8 128 IV8 P8 A8 = (C8, T8) := by native_decide +example : GCM_AD_192 K8 IV8 C8 A8 T8 = P8 := by native_decide -- Test Vector 9 -def K9 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K9 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 def P9 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) def A9 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C9 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide) -def T9 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide) -example : GCM_AE_256 K9 IV9 P9 A9 128 = (C9, T9) := by native_decide -example : GCM_AD_256 K9 IV9 C9 A9 T9 = P9 := by native_decide +def C9 : BitVec 480 := rev_elems 480 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480 (by decide) (by decide) +def T9 : BitVec 128 := rev_elems 128 8 0x2519498e80f1478f37ba55bd6d27618c#128 (by decide) (by decide) +example : GCM_AE_192 K9 128 IV9 P9 A9 = (C9, T9) := by native_decide +example : GCM_AD_192 K9 IV9 C9 A9 T9 = P9 := by native_decide --- Test Vector 10 (17) +-- Test Vector 10 -def K10 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K10 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) def IV10 : BitVec 64:= 0xcafebabefacedbad#64 def P10 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) def A10 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C10 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide) -def T10 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide) -example : GCM_AE_256 K10 IV10 P10 A10 128 = (C10, T10) := by native_decide -example : GCM_AD_256 K10 IV10 C10 A10 T10 = P10 := by native_decide +def C10 : BitVec 480 := rev_elems 480 8 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480 (by decide) (by decide) +def T10 : BitVec 128 := rev_elems 128 8 0x65dcc57fcf623a24094fcca40d3533f8#128 (by decide) (by decide) +example : GCM_AE_192 K10 128 IV10 P10 A10 = (C10, T10) := by native_decide +example : GCM_AD_192 K10 IV10 C10 A10 T10 = P10 := by native_decide -- Test Vector 11 -def K11 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K11 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 def P11 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) def A11 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C11 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide) -def T11 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide) -example : GCM_AE_256 K11 IV11 P11 A11 128 = (C11, T11) := by native_decide -example : GCM_AD_256 K11 IV11 C11 A11 T11 = P11 := by native_decide +def C11 : BitVec 480 := rev_elems 480 8 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480 (by decide) (by decide) +def T11 : BitVec 128 := rev_elems 128 8 0xdcf566ff291c25bbb8568fc3d376a6d9#128 (by decide) (by decide) +example : GCM_AE_192 K11 128 IV11 P11 A11 = (C11, T11) := by native_decide +example : GCM_AD_192 K11 IV11 C11 A11 T11 = P11 := by native_decide + +-- Test Vector 12 + +def K12 : BitVec 256 := 0 +def IV12 : BitVec 96 := 0 +def P12 : BitVec 0 := BitVec.nil +def A12 : BitVec 0 := BitVec.nil +def C12 : BitVec 0 := BitVec.nil +def T12 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide) +example : GCM_AE_256 K12 128 IV12 P12 A12 = (C12, T12) := by native_decide +example : GCM_AD_256 K12 IV12 C12 A12 T12 = P12 := by native_decide + +-- Test Vector 13 + +def K13 : BitVec 256 := 0 +def IV13 : BitVec 96 := 0 +def P13 : BitVec 128 := 0 +def A13 : BitVec 0 := BitVec.nil +def C13 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide) +def T13 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide) +example : GCM_AE_256 K13 128 IV13 P13 A13 = (C13, T13) := by native_decide +example : GCM_AD_256 K13 IV13 C13 A13 T13 = P13 := by native_decide + +-- Test Vector 14 + +def K14 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV14 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P14 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def A14 : BitVec 0 := BitVec.nil +def C14 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide) +def T14 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide) +example : GCM_AE_256 K14 128 IV14 P14 A14 = (C14, T14) := by native_decide +example : GCM_AD_256 K14 IV14 C14 A14 T14 = P14 := by native_decide + +-- Test Vector 15 + +def K15 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV15 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 +def P15 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A15 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C15 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide) +def T15 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide) +example : GCM_AE_256 K15 128 IV15 P15 A15 = (C15, T15) := by native_decide +example : GCM_AD_256 K15 IV15 C15 A15 T15 = P15 := by native_decide + +-- Test Vector 16 + +def K16 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV16 : BitVec 64:= 0xcafebabefacedbad#64 +def P16 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A16 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C16 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide) +def T16 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide) +example : GCM_AE_256 K16 128 IV16 P16 A16 = (C16, T16) := by native_decide +example : GCM_AD_256 K16 IV16 C16 A16 T16 = P16 := by native_decide + +-- Test Vector 17 + +def K17 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def IV17 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 +def P17 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) +def A17 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) +def C17 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide) +def T17 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide) +example : GCM_AE_256 K17 128 IV17 P17 A17 = (C17, T17) := by native_decide +example : GCM_AD_256 K17 IV17 C17 A17 T17 = P17 := by native_decide end AES256GCMSpecTest From 8e461ee813ae0546f779c7b2a2f081ab51e594b3 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 3 Apr 2024 17:10:29 -0700 Subject: [PATCH 4/6] Develop tactics for verifying table lookup --- Specs/AES.lean | 18 +++-- Tactics/Enum_bv.lean | 167 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 178 insertions(+), 7 deletions(-) create mode 100644 Tactics/Enum_bv.lean diff --git a/Specs/AES.lean b/Specs/AES.lean index 7eb13640..a97c6604 100644 --- a/Specs/AES.lean +++ b/Specs/AES.lean @@ -6,6 +6,7 @@ Author(s): Yan Peng import Arm.BitVec import Arm.Insts.DPSFP.Crypto_aes import Specs.AESCommon +import Tactics.Enum_bv -- References : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf -- https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/aes-development/rijndael-ammended.pdf @@ -165,18 +166,21 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size) let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03 --- TODO: looks like a SAT/SMT problem +set_option maxRecDepth 3000 in +set_option maxHeartbeats 300000 in +set_option profiler true in protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by funext x - simp only [XTimes, DPSFP.FFmul02] - sorry + enum_bv 8 x + -- sorry --- TODO: looks like a SAT/SMT problem +set_option maxRecDepth 3000 in +set_option maxHeartbeats 300000 in +set_option profiler true in protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by funext x - simp only [XTimes, DPSFP.FFmul03] - sorry - + enum_bv 8 x + -- sorry theorem MixColumns_table_lookup_equiv {Param : KBR} (state : BitVec Param.block_size): diff --git a/Tactics/Enum_bv.lean b/Tactics/Enum_bv.lean new file mode 100644 index 00000000..672b3559 --- /dev/null +++ b/Tactics/Enum_bv.lean @@ -0,0 +1,167 @@ +/- +Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author(s): Yan Peng +-/ +import Lean.Elab +import Lean.Expr + +open BitVec + +theorem le_and_ne_implies_lt (x : Nat) (y : Nat) (h0 : x ≠ y) (h1 : x ≤ y): x < y := by + have h : x < y ∨ x = y := by apply Nat.lt_or_eq_of_le h1 + cases h + · assumption + · contradiction + +-- An example +-- def carry_less_add (x : BitVec 2) : BitVec 2 := x ^^^ 0b1#2 +-- def lookup_cla (x : BitVec 2) : BitVec 2 := +-- BitVec.cast (by omega) $ +-- if x.toNat == 0 then 0b01#2 +-- else if x.toNat == 1 then 0b0#2 +-- else if x.toNat == 2 then 0b11#2 +-- else 0b10#2 + +-- theorem example_lemma_expanded : carry_less_add = lookup_cla := by +-- funext x +-- by_cases h₀ : x = BitVec.ofNat 2 0 +-- case pos => +-- simp only [h₀] +-- decide +-- case neg => +-- by_cases h₁ : x = BitVec.ofNat 2 1 +-- case pos => +-- simp only [h₁] +-- decide +-- case neg => +-- by_cases h₂ : x = BitVec.ofNat 2 2 +-- case pos => +-- simp [h₂] +-- decide +-- case neg => +-- by_cases h₃ : x = BitVec.ofNat 2 3 +-- case pos => +-- simp [h₃] +-- decide +-- case neg => +-- rw [← ne_eq, toNat_ne] at * +-- have p4 : x.toNat < 4 := by +-- exact isLt x +-- have p3' : x.toNat ≤ 3 := by +-- apply Nat.le_of_lt_succ +-- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p4] +-- have p3 : x.toNat < 3 := by +-- apply le_and_ne_implies_lt +-- · exact h₃ +-- · simp only [p3'] +-- have p2' : x.toNat ≤ 2 := by +-- apply Nat.le_of_lt_succ +-- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p3] +-- have p2 : x.toNat < 2 := by +-- apply le_and_ne_implies_lt +-- · exact h₂ +-- · simp only [p2'] +-- have p1' : x.toNat ≤ 1 := by +-- apply Nat.le_of_lt_succ +-- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p2] +-- have p1 : x.toNat < 1 := by +-- apply le_and_ne_implies_lt +-- · exact h₁ +-- · simp only [p1'] +-- have p0' : x.toNat ≤ 0 := by +-- apply Nat.le_of_lt_succ +-- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p1] +-- have p0 : x.toNat = 0 := by +-- exact Nat.eq_zero_of_le_zero p0' +-- contradiction + +partial def shrink (i : Nat) (N : Nat) (var : Lean.Ident) + : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do + let i_str := toString i + let i_num := Lean.Syntax.mkNumLit i_str + if i = N then + let p_name := + Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str) + let rest ← shrink (i - 1) N var + `(tactic| + (have $p_name:ident : BitVec.toNat $var:ident < $i_num:num := by + exact isLt $var:ident + $rest:tactic)) + else + let i_pre := toString (i + 1) + let p_pre := + Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_pre) + let p_name1 := + Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str ++ "'") + let p_name2 := + Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str) + if i ≤ 0 then + `(tactic| + (have $p_name1:ident : BitVec.toNat $var:ident ≤ $i_num:num := by + apply Nat.le_of_lt_succ + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, $p_pre:ident] + clear $p_pre:ident + have $p_name2:ident : BitVec.toNat $var:ident = $i_num:num := by + exact Nat.eq_zero_of_le_zero $p_name1:ident + clear $p_name1:ident)) + else + let h_name := + Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("h" ++ i_str) + let rest ← shrink (i - 1) N var + `(tactic| + (have $p_name1:ident : BitVec.toNat $var:ident ≤ $i_num:num := by + apply Nat.le_of_lt_succ + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, $p_pre:ident] + clear $p_pre:ident + have $p_name2:ident : BitVec.toNat $var:ident < $i_num:num := by + apply le_and_ne_implies_lt + · exact $h_name:ident + · simp only [$p_name1:ident] + clear $p_name1:ident + $rest:tactic)) + +def enum_last_case (n : Nat) (var : Lean.Ident) + : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do + let shrink_tac ← shrink (2 ^ n) (2 ^ n) var + `(tactic| + (rw [← ne_eq, toNat_ne] at * + $shrink_tac:tactic + contradiction) + ) + +partial def enum_cases_syntax (i : Nat) (n : Nat) (var : Lean.Ident) + : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do + if 2 ^ n ≤ i + then let last ← enum_last_case n var + `(tactic| $last:tactic) + else + let i_str := toString i + let h_name := Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("h" ++ i_str) + let i_num := Lean.Syntax.mkNumLit i_str + let n_num := Lean.Syntax.mkNumLit $ toString n + let rest ← enum_cases_syntax (i + 1) n var + `(tactic| + (by_cases $h_name:ident : $var:ident = (BitVec.ofNat $n_num:num $i_num:num) + · simp only [$h_name:ident]; decide + · $rest:tactic + done + ) + ) + +def enum_bv_fn (n : Lean.Syntax.NumLit) (var : Lean.Ident): + Lean.Elab.Tactic.TacticM Unit := + Lean.Elab.Tactic.withMainContext do + Lean.Elab.Tactic.evalTactic (← + enum_cases_syntax 0 n.getNat var + ) + +-- Establishing a theorem through enumeration of all values of a bit-vector +-- Assumption: the theorem has only one free variable of type `BitVec n` +elab "enum_bv" n:num var:ident : tactic => do + enum_bv_fn n var + +-- theorem example_lemma : carry_less_add = lookup_cla := by +-- funext x +-- enum_bv 2 x + From 2dd7061e89708ad080763b9e11a7126beb07efe4 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 11 Apr 2024 15:39:18 -0700 Subject: [PATCH 5/6] Changes addressing review from Hanno Becker --- Specs/{AES.lean => AESArm.lean} | 44 ++++----- Specs/GCM.lean | 76 ++++++++-------- Specs/Specs.lean | 2 +- Tactics/Enum_bv.lean | 1 - Tests/AESGCMSpecTest.lean | 156 ++++++++++++++++++-------------- Tests/AESSpecTest.lean | 4 +- 6 files changed, 147 insertions(+), 136 deletions(-) rename Specs/{AES.lean => AESArm.lean} (88%) diff --git a/Specs/AES.lean b/Specs/AESArm.lean similarity index 88% rename from Specs/AES.lean rename to Specs/AESArm.lean index a97c6604..fc8e1633 100644 --- a/Specs/AES.lean +++ b/Specs/AESArm.lean @@ -37,7 +37,7 @@ import Tactics.Enum_bv -- -------------------------------------------------- -namespace AES +namespace AESArm open BitVec @@ -118,7 +118,7 @@ protected def InitKey {Param : KBR} (i : Nat) (key : BitVec Param.key_len) let wd := h₁ ▸ extractLsb (i * 32 + 32 - 1) (i * 32) key let (x:KeySchedule) := [wd] have _ : Param.Nk - (i + 1) < Param.Nk - i := by omega - AES.InitKey (Param := Param) (i + 1) key (acc ++ x) + AESArm.InitKey (Param := Param) (i + 1) key (acc ++ x) termination_by (Param.Nk - i) protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule) @@ -137,13 +137,13 @@ protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule) let res := (List.get! ks (i - Param.Nk)) ^^^ tmp let ks := List.append ks [ res ] have _ : 4 * Param.Nr + 4 - (i + 1) < 4 * Param.Nr + 4 - i := by omega - AES.KeyExpansion_helper (Param := Param) (i + 1) ks + AESArm.KeyExpansion_helper (Param := Param) (i + 1) ks termination_by (4 * Param.Nr + 4 - i) def KeyExpansion {Param : KBR} (key : BitVec Param.key_len) : KeySchedule := - let seeded := AES.InitKey (Param := Param) 0 key [] - AES.KeyExpansion_helper (Param := Param) Param.Nk seeded + let seeded := AESArm.InitKey (Param := Param) 0 key [] + AESArm.KeyExpansion_helper (Param := Param) Param.Nk seeded def SubBytes {Param : KBR} (state : BitVec Param.block_size) : BitVec Param.block_size := @@ -166,28 +166,28 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size) let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03 -set_option maxRecDepth 3000 in -set_option maxHeartbeats 300000 in -set_option profiler true in +-- set_option maxRecDepth 3000 in +-- set_option maxHeartbeats 300000 in +-- set_option profiler true in protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by funext x - enum_bv 8 x - -- sorry + -- enum_bv 8 x + sorry -set_option maxRecDepth 3000 in -set_option maxHeartbeats 300000 in -set_option profiler true in +-- set_option maxRecDepth 3000 in +-- set_option maxHeartbeats 300000 in +-- set_option profiler true in protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by funext x - enum_bv 8 x - -- sorry + -- enum_bv 8 x + sorry theorem MixColumns_table_lookup_equiv {Param : KBR} (state : BitVec Param.block_size): have h : Param.block_size = 128 := by simp only [Param.h, BlockSize] MixColumns (Param := Param) state = h ▸ DPSFP.AESMixColumns (h ▸ state) := by simp only [MixColumns, DPSFP.AESMixColumns] - rw [AES.FFmul02_equiv, AES.FFmul03_equiv] + rw [AESArm.FFmul02_equiv, AESArm.FFmul03_equiv] def AddRoundKey {Param : KBR} (state : BitVec Param.block_size) (roundKey : BitVec Param.block_size) : BitVec Param.block_size := @@ -209,23 +209,23 @@ protected def AES_encrypt_with_ks_loop {Param : KBR} (round : Nat) let state := SubBytes state let state := ShiftRows state let state := MixColumns state - let state := AddRoundKey state $ AES.getKey round w - AES.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w + let state := AddRoundKey state $ AESArm.getKey round w + AESArm.AES_encrypt_with_ks_loop (Param := Param) (round + 1) state w termination_by (Param.Nr - round) def AES_encrypt_with_ks {Param : KBR} (input : BitVec Param.block_size) (w : KeySchedule) : BitVec Param.block_size := have h₀ : WordSize + WordSize + WordSize + WordSize = Param.block_size := by simp only [WordSize, BlockSize, Param.h] - let state := AddRoundKey input $ (h₀ ▸ AES.getKey 0 w) - let state := AES.AES_encrypt_with_ks_loop (Param := Param) 1 state w + let state := AddRoundKey input $ (h₀ ▸ AESArm.getKey 0 w) + let state := AESArm.AES_encrypt_with_ks_loop (Param := Param) 1 state w let state := SubBytes (Param := Param) state let state := ShiftRows (Param := Param) state - AddRoundKey state $ h₀ ▸ AES.getKey Param.Nr w + AddRoundKey state $ h₀ ▸ AESArm.getKey Param.Nr w def AES_encrypt {Param : KBR} (input : BitVec Param.block_size) (key : BitVec Param.key_len) : BitVec Param.block_size := let ks := KeyExpansion (Param := Param) key AES_encrypt_with_ks (Param := Param) input ks -end AES +end AESArm diff --git a/Specs/GCM.lean b/Specs/GCM.lean index 5248624d..620845d4 100644 --- a/Specs/GCM.lean +++ b/Specs/GCM.lean @@ -12,6 +12,9 @@ namespace GCM open BitVec +/-- NIST Special Publication 800-38D, page 11-12. + This constant represents, up to x^127, the polynomial for defining GF(2^128) + -/ def R : (BitVec 128) := 0b11100001#8 ++ 0b0#120 /-- A Cipher type is a function that takes an input of size n and @@ -51,14 +54,12 @@ def GHASH_aux (i : Nat) (H : BitVec 128) (X : BitVec n) (Y : BitVec 128) if n / 128 ≤ i then Y else - let lo := i * 128 + 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 := rev_elems 128 8 (Y ^^^ (h₀ ▸ Xi)) (by decide) (by decide) - let H_rev := rev_elems 128 8 H (by decide) (by decide) - let Y := mul res H_rev - let Y := rev_elems 128 8 Y (by decide) (by decide) + let res := Y ^^^ (h₀ ▸ Xi) + let Y := mul res H GHASH_aux (i + 1) H X Y h termination_by (n / 128 - i) @@ -72,15 +73,11 @@ def GCTR_aux (CIPH : Cipher (n := 128) (m := m)) if n ≤ i then Y else - let lo := i * 128 + 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 ICB_rev := rev_elems 128 8 ICB (by decide) (by decide) - let Yi := h ▸ Xi ^^^ CIPH ICB_rev K - -- partInstall ignores val indexes that exceeds length of Y + let Yi := h ▸ Xi ^^^ CIPH ICB K 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 @@ -90,15 +87,23 @@ protected def ceiling_in_blocks (w : Nat) := (w - 1) / 128 + 1 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] + w ≤ (GCM.ceiling_in_bits w) := by + simp only [GCM.ceiling_in_bits, 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 - GCTR_aux CIPH 0 n K ICB X $ BitVec.zero v + let b := GCM.ceiling_in_bits v + let s := b - v + let h : v + s = b := by + simp only [s] + apply Nat.add_sub_cancel' + (by simp only [b]; apply GCM.bits_le_ceiling_in_bits) + 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): @@ -116,22 +121,15 @@ protected def initialize_J0 (H : BitVec 128) (IV : BitVec lv) := 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) + let block := IV ++ (BitVec.zero (s + 64)) ++ (BitVec.ofNat 64 lv) + GHASH H block h₂ 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 + 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 + (y : Nat) (x : Nat) (h : y ≤ x): + (x - y) + y = x := by omega /-- GCM_AE : Galois Counter Mode Authenticated Encryption -/ def GCM_AE (CIPH : Cipher (n := 128) (m := m)) @@ -143,17 +141,16 @@ def GCM_AE (CIPH : Cipher (n := 128) (m := m)) let C := GCTR (m := m) CIPH K ICB P let u := GCM.ceiling_in_bits p - p let v := GCM.ceiling_in_bits a - a - let block := rev_elems 64 8 (BitVec.ofNat 64 p) (by decide) (by decide) - ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide) - ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A - have h : 128 ∣ 64 + 64 + u + p + v + a := by + 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) + rw [GCM.GCM_AE_DE_simplification2 p (GCM.ceiling_in_bits p) (by apply GCM.bits_le_ceiling_in_bits)] - rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a) + rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a) (by apply GCM.bits_le_ceiling_in_bits)] + simp only [GCM.ceiling_in_bits] omega let S := GHASH H block h let T := truncate t $ GCTR (m := m) CIPH K J0 S @@ -179,17 +176,16 @@ def GCM_AD (CIPH : Cipher (n := 128) (m := m)) let P := GCTR (m := m) CIPH K ICB C let u := GCM.ceiling_in_bits c - c let v := GCM.ceiling_in_bits a - a - let block := rev_elems 64 8 (BitVec.ofNat 64 c) (by decide) (by decide) - ++ rev_elems 64 8 (BitVec.ofNat 64 a) (by decide) (by decide) - ++ BitVec.zero u ++ C ++ BitVec.zero v ++ A - have h : 128 ∣ 64 + 64 + u + c + v + a := by + let block := A ++ BitVec.zero v ++ C ++ BitVec.zero u + ++ (BitVec.ofNat 64 a) ++ (BitVec.ofNat 64 c) + have h : 128 ∣ a + v + c + 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 c (GCM.ceiling_in_blocks c) + rw [GCM.GCM_AE_DE_simplification2 c (GCM.ceiling_in_bits c) (by apply GCM.bits_le_ceiling_in_bits)] - rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_blocks a) + rw [GCM.GCM_AE_DE_simplification2 a (GCM.ceiling_in_bits a) (by apply GCM.bits_le_ceiling_in_bits)] + simp only [GCM.ceiling_in_bits] omega let S := GHASH H block h let T' := truncate t $ GCTR (m := m) CIPH K J0 S diff --git a/Specs/Specs.lean b/Specs/Specs.lean index 9586f35f..57e638db 100644 --- a/Specs/Specs.lean +++ b/Specs/Specs.lean @@ -5,5 +5,5 @@ Author(s): Shilpi Goel -/ import «Specs».SHA512 import «Specs».AESCommon -import «Specs».AES +import «Specs».AESArm import «Specs».GCM diff --git a/Tactics/Enum_bv.lean b/Tactics/Enum_bv.lean index 672b3559..474e4f69 100644 --- a/Tactics/Enum_bv.lean +++ b/Tactics/Enum_bv.lean @@ -164,4 +164,3 @@ elab "enum_bv" n:num var:ident : tactic => do -- theorem example_lemma : carry_less_add = lookup_cla := by -- funext x -- enum_bv 2 x - diff --git a/Tests/AESGCMSpecTest.lean b/Tests/AESGCMSpecTest.lean index 9c9f094c..8f17f107 100644 --- a/Tests/AESGCMSpecTest.lean +++ b/Tests/AESGCMSpecTest.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ import Arm.BitVec -import Specs.AES +import Specs.AESArm import Specs.GCM -- Reference: https://csrc.nist.rip/groups/ST/toolkit/BCM/documents/proposedmodes/gcm/gcm-spec.pdf @@ -13,8 +13,18 @@ namespace AES256GCMSpecTest open BitVec +-- Reversing bytes in inputs and output because AES uses little-endian +def revCIPH (CIPH : BitVec n -> BitVec m -> BitVec n) + (h₀ : 8 ∣ n) (h₁ : 8 ∣ m) (p : BitVec n) (k : BitVec m) := + (rev_elems n 8 + (CIPH (rev_elems n 8 p h₀ (by decide)) (rev_elems m 8 k h₁ (by decide))) + h₀ (by decide)) + +def CIPH_128' : GCM.Cipher (n := 128) (m := 128) := + AESArm.AES_encrypt (Param := AESArm.AES128KBR) + def CIPH_128 : GCM.Cipher (n := 128) (m := 128) := - AES.AES_encrypt (Param := AES.AES128KBR) + revCIPH CIPH_128' (by decide) (by decide) def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec a → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_128 @@ -22,8 +32,11 @@ def GCM_AE_128 : BitVec 128 → (t : Nat) → BitVec lv → BitVec p → BitVec def GCM_AD_128 : BitVec 128 → BitVec lv → BitVec c → BitVec a → BitVec t → Option (BitVec c) := GCM.GCM_AD CIPH_128 +def CIPH_192' : GCM.Cipher (n := 128) (m := 192) := + AESArm.AES_encrypt (Param := AESArm.AES192KBR) + def CIPH_192 : GCM.Cipher (n := 128) (m := 192) := -AES.AES_encrypt (Param := AES.AES192KBR) + revCIPH CIPH_192' (by decide) (by decide) def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec a → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_192 @@ -31,8 +44,11 @@ def GCM_AE_192 : BitVec 192 → (t : Nat) → BitVec lv → BitVec p → BitVec def GCM_AD_192 : BitVec 192 → BitVec lv → BitVec c → BitVec a → BitVec t → Option (BitVec c) := GCM.GCM_AD CIPH_192 +def CIPH_256' : GCM.Cipher (n := 128) (m := 256) := + AESArm.AES_encrypt (Param := AESArm.AES256KBR) + def CIPH_256 : GCM.Cipher (n := 128) (m := 256) := - AES.AES_encrypt (Param := AES.AES256KBR) + revCIPH CIPH_256' (by decide) (by decide) def GCM_AE_256 : BitVec 256 → (t : Nat) → BitVec lv → BitVec p → BitVec a → (BitVec p) × (BitVec t) := GCM.GCM_AE CIPH_256 @@ -47,7 +63,7 @@ def IV0 : BitVec 96 := 0 def P0 : BitVec 0 := BitVec.nil def A0 : BitVec 0 := BitVec.nil def C0 : BitVec 0 := BitVec.nil -def T0 : BitVec 128 := rev_elems 128 8 0x58e2fccefa7e3061367f1d57a4e7455a#128 (by decide) (by decide) +def T0 : BitVec 128 := 0x58e2fccefa7e3061367f1d57a4e7455a#128 example : GCM_AE_128 K0 128 IV0 P0 A0 = (C0, T0) := by native_decide example : GCM_AD_128 K0 IV0 C0 A0 T0 = P0 := by native_decide @@ -57,52 +73,52 @@ def K1 : BitVec 128 := 0 def IV1 : BitVec 96 := 0 def P1 : BitVec 128 := 0 def A1 : BitVec 0 := BitVec.nil -def C1 : BitVec 128 := rev_elems 128 8 0x0388dace60b6a392f328c2b971b2fe78#128 (by decide) (by decide) -def T1 : BitVec 128 := rev_elems 128 8 0xab6e47d42cec13bdf53a67b21257bddf#128 (by decide) (by decide) +def C1 : BitVec 128 := 0x0388dace60b6a392f328c2b971b2fe78#128 +def T1 : BitVec 128 := 0xab6e47d42cec13bdf53a67b21257bddf#128 example : GCM_AE_128 K1 128 IV1 P1 A1 = (C1, T1) := by native_decide example : GCM_AD_128 K1 IV1 C1 A1 T1 = P1 := by native_decide -- Test Vector 2 -def K2 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def K2 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128 def IV2 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P2 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def P2 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 def A2 : BitVec 0 := BitVec.nil -def C2 : BitVec 512 := rev_elems 512 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 (by decide) (by decide) -def T2 : BitVec 128 := rev_elems 128 8 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 (by decide) (by decide) +def C2 : BitVec 512 := 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091473f5985#512 +def T2 : BitVec 128 := 0x4d5c2af327cd64a62cf35abd2ba6fab4#128 example : GCM_AE_128 K2 128 IV2 P2 A2 = (C2, T2) := by native_decide example : GCM_AD_128 K2 IV2 C2 A2 T2 = P2 := by native_decide -- Test Vector 3 -def K3 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def K3 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128 def IV3 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P3 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A3 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C3 : BitVec 480 := rev_elems 480 8 0x42831ec2217774244b7221b784d0d49ce3aa212f2c02a4e035c17e2329aca12e21d514b25466931c7d8f6a5aac84aa051ba30b396a0aac973d58e091#480 (by decide) (by decide) -def T3 : BitVec 128 := rev_elems 128 8 0x5bc94fbc3221a5db94fae95ae7121a47#128 (by decide) (by decide) +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 example : GCM_AD_128 K3 IV3 C3 A3 T3 = P3 := by native_decide -- Test Vector 4 -def K4 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def K4 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128 def IV4 : BitVec 64 := 0xcafebabefacedbad#64 -def P4 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A4 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C4 : BitVec 480 := rev_elems 480 8 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 (by decide) (by decide) -def T4 : BitVec 128 := rev_elems 128 8 0x3612d2e79e3b0785561be14aaca2fccb#128 (by decide) (by decide) +def P4 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A4 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C4 : BitVec 480 := 0x61353b4c2806934a777ff51fa22a4755699b2a714fcdc6f83766e5f97b6c742373806900e49f24b22b097544d4896b424989b5e1ebac0f07c23f4598#480 +def T4 : BitVec 128 := 0x3612d2e79e3b0785561be14aaca2fccb#128 example : GCM_AE_128 K4 128 IV4 P4 A4 = (C4, T4) := by native_decide example : GCM_AD_128 K4 IV4 C4 A4 T4 = P4 := by native_decide -- Test Vector 5 -def K5 : BitVec 128 := rev_elems 128 8 0xfeffe9928665731c6d6a8f9467308308#128 (by decide) (by decide) +def K5 : BitVec 128 := 0xfeffe9928665731c6d6a8f9467308308#128 def IV5 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 -def P5 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A5 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C5 : BitVec 480 := rev_elems 480 8 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 (by decide) (by decide) -def T5 : BitVec 128 := rev_elems 128 8 0x619cc5aefffe0bfa462af43c1699d050#128 (by decide) (by decide) +def P5 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A5 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C5 : BitVec 480 := 0x8ce24998625615b603a033aca13fb894be9112a5c3a211a8ba262a3cca7e2ca701e4a9a4fba43c90ccdcb281d48c7c6fd62875d2aca417034c34aee5#480 +def T5 : BitVec 128 := 0x619cc5aefffe0bfa462af43c1699d050#128 example : GCM_AE_128 K5 128 IV5 P5 A5 = (C5, T5) := by native_decide example : GCM_AD_128 K5 IV5 C5 A5 T5 = P5 := by native_decide @@ -113,7 +129,7 @@ def IV6 : BitVec 96 := 0 def P6 : BitVec 0 := BitVec.nil def A6 : BitVec 0 := BitVec.nil def C6 : BitVec 0 := BitVec.nil -def T6 : BitVec 128 := rev_elems 128 8 0xcd33b28ac773f74ba00ed1f312572435#128 (by decide) (by decide) +def T6 : BitVec 128 := 0xcd33b28ac773f74ba00ed1f312572435#128 example : GCM_AE_192 K6 128 IV6 P6 A6 = (C6, T6) := by native_decide example : GCM_AD_192 K6 IV6 C6 A6 T6 = P6 := by native_decide @@ -123,52 +139,52 @@ def K7 : BitVec 192 := 0 def IV7 : BitVec 96 := 0 def P7 : BitVec 128 := 0 def A7 : BitVec 0 := BitVec.nil -def C7 : BitVec 128 := rev_elems 128 8 0x98e7247c07f0fe411c267e4384b0f600#128 (by decide) (by decide) -def T7 : BitVec 128 := rev_elems 128 8 0x2ff58d80033927ab8ef4d4587514f0fb#128 (by decide) (by decide) +def C7 : BitVec 128 := 0x98e7247c07f0fe411c267e4384b0f600#128 +def T7 : BitVec 128 := 0x2ff58d80033927ab8ef4d4587514f0fb#128 example : GCM_AE_192 K7 128 IV7 P7 A7 = (C7, T7) := by native_decide example : GCM_AD_192 K7 IV7 C7 A7 T7 = P7 := by native_decide -- Test Vector 8 -def K8 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) +def K8 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 def IV8 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P8 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def P8 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 def A8 : BitVec 0 := BitVec.nil -def C8 : BitVec 512 := rev_elems 512 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512 (by decide) (by decide) -def T8 : BitVec 128 := rev_elems 128 8 0x9924a7c8587336bfb118024db8674a14#128 (by decide) (by decide) +def C8 : BitVec 512 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710acade256#512 +def T8 : BitVec 128 := 0x9924a7c8587336bfb118024db8674a14#128 example : GCM_AE_192 K8 128 IV8 P8 A8 = (C8, T8) := by native_decide example : GCM_AD_192 K8 IV8 C8 A8 T8 = P8 := by native_decide -- Test Vector 9 -def K9 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) +def K9 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 def IV9 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P9 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A9 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C9 : BitVec 480 := rev_elems 480 8 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480 (by decide) (by decide) -def T9 : BitVec 128 := rev_elems 128 8 0x2519498e80f1478f37ba55bd6d27618c#128 (by decide) (by decide) +def P9 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A9 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C9 : BitVec 480 := 0x3980ca0b3c00e841eb06fac4872a2757859e1ceaa6efd984628593b40ca1e19c7d773d00c144c525ac619d18c84a3f4718e2448b2fe324d9ccda2710#480 +def T9 : BitVec 128 := 0x2519498e80f1478f37ba55bd6d27618c#128 example : GCM_AE_192 K9 128 IV9 P9 A9 = (C9, T9) := by native_decide example : GCM_AD_192 K9 IV9 C9 A9 T9 = P9 := by native_decide -- Test Vector 10 -def K10 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) +def K10 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 def IV10 : BitVec 64:= 0xcafebabefacedbad#64 -def P10 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A10 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C10 : BitVec 480 := rev_elems 480 8 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480 (by decide) (by decide) -def T10 : BitVec 128 := rev_elems 128 8 0x65dcc57fcf623a24094fcca40d3533f8#128 (by decide) (by decide) +def P10 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A10 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C10 : BitVec 480 := 0x0f10f599ae14a154ed24b36e25324db8c566632ef2bbb34f8347280fc4507057fddc29df9a471f75c66541d4d4dad1c9e93a19a58e8b473fa0f062f7#480 +def T10 : BitVec 128 := 0x65dcc57fcf623a24094fcca40d3533f8#128 example : GCM_AE_192 K10 128 IV10 P10 A10 = (C10, T10) := by native_decide example : GCM_AD_192 K10 IV10 C10 A10 T10 = P10 := by native_decide -- Test Vector 11 -def K11 : BitVec 192 := rev_elems 192 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 (by decide) (by decide) +def K11 : BitVec 192 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c#192 def IV11 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 -def P11 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A11 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C11 : BitVec 480 := rev_elems 480 8 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480 (by decide) (by decide) -def T11 : BitVec 128 := rev_elems 128 8 0xdcf566ff291c25bbb8568fc3d376a6d9#128 (by decide) (by decide) +def P11 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A11 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C11 : BitVec 480 := 0xd27e88681ce3243c4830165a8fdcf9ff1de9a1d8e6b447ef6ef7b79828666e4581e79012af34ddd9e2f037589b292db3e67c036745fa22e7e9b7373b#480 +def T11 : BitVec 128 := 0xdcf566ff291c25bbb8568fc3d376a6d9#128 example : GCM_AE_192 K11 128 IV11 P11 A11 = (C11, T11) := by native_decide example : GCM_AD_192 K11 IV11 C11 A11 T11 = P11 := by native_decide @@ -179,7 +195,7 @@ def IV12 : BitVec 96 := 0 def P12 : BitVec 0 := BitVec.nil def A12 : BitVec 0 := BitVec.nil def C12 : BitVec 0 := BitVec.nil -def T12 : BitVec 128 := rev_elems 128 8 0x530f8afbc74536b9a963b4f1c4cb738b#128 (by decide) (by decide) +def T12 : BitVec 128 := 0x530f8afbc74536b9a963b4f1c4cb738b#128 example : GCM_AE_256 K12 128 IV12 P12 A12 = (C12, T12) := by native_decide example : GCM_AD_256 K12 IV12 C12 A12 T12 = P12 := by native_decide @@ -189,52 +205,52 @@ def K13 : BitVec 256 := 0 def IV13 : BitVec 96 := 0 def P13 : BitVec 128 := 0 def A13 : BitVec 0 := BitVec.nil -def C13 : BitVec 128 := rev_elems 128 8 0xcea7403d4d606b6e074ec5d3baf39d18#128 (by decide) (by decide) -def T13 : BitVec 128 := rev_elems 128 8 0xd0d1c8a799996bf0265b98b5d48ab919#128 (by decide) (by decide) +def C13 : BitVec 128 := 0xcea7403d4d606b6e074ec5d3baf39d18#128 +def T13 : BitVec 128 := 0xd0d1c8a799996bf0265b98b5d48ab919#128 example : GCM_AE_256 K13 128 IV13 P13 A13 = (C13, T13) := by native_decide example : GCM_AD_256 K13 IV13 C13 A13 T13 = P13 := by native_decide -- Test Vector 14 -def K14 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K14 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 def IV14 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P14 : BitVec 512 := rev_elems 512 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 (by decide) (by decide) +def P14 : BitVec 512 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b391aafd255#512 def A14 : BitVec 0 := BitVec.nil -def C14 : BitVec 512 := rev_elems 512 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 (by decide) (by decide) -def T14 : BitVec 128 := rev_elems 128 8 0xb094dac5d93471bdec1a502270e3cc6c#128 (by decide) (by decide) +def C14 : BitVec 512 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662898015ad#512 +def T14 : BitVec 128 := 0xb094dac5d93471bdec1a502270e3cc6c#128 example : GCM_AE_256 K14 128 IV14 P14 A14 = (C14, T14) := by native_decide example : GCM_AD_256 K14 IV14 C14 A14 T14 = P14 := by native_decide -- Test Vector 15 -def K15 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K15 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 def IV15 : BitVec 96 := 0xcafebabefacedbaddecaf888#96 -def P15 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A15 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C15 : BitVec 480 := rev_elems 480 8 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 (by decide) (by decide) -def T15 : BitVec 128 := rev_elems 128 8 0x76fc6ece0f4e1768cddf8853bb2d551b#128 (by decide) (by decide) +def P15 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A15 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C15 : BitVec 480 := 0x522dc1f099567d07f47f37a32a84427d643a8cdcbfe5c0c97598a2bd2555d1aa8cb08e48590dbb3da7b08b1056828838c5f61e6393ba7a0abcc9f662#480 +def T15 : BitVec 128 := 0x76fc6ece0f4e1768cddf8853bb2d551b#128 example : GCM_AE_256 K15 128 IV15 P15 A15 = (C15, T15) := by native_decide example : GCM_AD_256 K15 IV15 C15 A15 T15 = P15 := by native_decide -- Test Vector 16 -def K16 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K16 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 def IV16 : BitVec 64:= 0xcafebabefacedbad#64 -def P16 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A16 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C16 : BitVec 480 := rev_elems 480 8 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 (by decide) (by decide) -def T16 : BitVec 128 := rev_elems 128 8 0x3a337dbf46a792c45e454913fe2ea8f2#128 (by decide) (by decide) +def P16 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A16 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C16 : BitVec 480 := 0xc3762df1ca787d32ae47c13bf19844cbaf1ae14d0b976afac52ff7d79bba9de0feb582d33934a4f0954cc2363bc73f7862ac430e64abe499f47c9b1f#480 +def T16 : BitVec 128 := 0x3a337dbf46a792c45e454913fe2ea8f2#128 example : GCM_AE_256 K16 128 IV16 P16 A16 = (C16, T16) := by native_decide example : GCM_AD_256 K16 IV16 C16 A16 T16 = P16 := by native_decide -- Test Vector 17 -def K17 : BitVec 256 := rev_elems 256 8 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 (by decide) (by decide) +def K17 : BitVec 256 := 0xfeffe9928665731c6d6a8f9467308308feffe9928665731c6d6a8f9467308308#256 def IV17 : BitVec 480 := 0x9313225df88406e555909c5aff5269aa6a7a9538534f7da1e4c303d2a318a728c3c0c95156809539fcf0e2429a6b525416aedbf5a0de6a57a637b39b#480 -def P17 : BitVec 480 := rev_elems 480 8 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 (by decide) (by decide) -def A17 : BitVec 160 := rev_elems 160 8 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 (by decide) (by decide) -def C17 : BitVec 480 := rev_elems 480 8 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 (by decide) (by decide) -def T17 : BitVec 128 := rev_elems 128 8 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 (by decide) (by decide) +def P17 : BitVec 480 := 0xd9313225f88406e5a55909c5aff5269a86a7a9531534f7da2e4c303d8a318a721c3c0c95956809532fcf0e2449a6b525b16aedf5aa0de657ba637b39#480 +def A17 : BitVec 160 := 0xfeedfacedeadbeeffeedfacedeadbeefabaddad2#160 +def C17 : BitVec 480 := 0x5a8def2f0c9e53f1f75d7853659e2a20eeb2b22aafde6419a058ab4f6f746bf40fc0c3b780f244452da3ebf1c5d82cdea2418997200ef82e44ae7e3f#480 +def T17 : BitVec 128 := 0xa44a8266ee1c8eb0c8b5d4cf5ae9f19a#128 example : GCM_AE_256 K17 128 IV17 P17 A17 = (C17, T17) := by native_decide example : GCM_AD_256 K17 IV17 C17 A17 T17 = P17 := by native_decide diff --git a/Tests/AESSpecTest.lean b/Tests/AESSpecTest.lean index a8e2fa64..7564955b 100644 --- a/Tests/AESSpecTest.lean +++ b/Tests/AESSpecTest.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author(s): Yan Peng -/ -import Specs.AES +import Specs.AESArm import Arm.BitVec -- Reference : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf Section B @@ -37,6 +37,6 @@ protected def output : BitVec 128 := 0xdc#8, 0x11#8, 0x85#8, 0x97#8, 0x19#8, 0x6a#8, 0x0b#8, 0x32#8 ].reverse -example : AES.AES_encrypt (Param := AES.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide +example : AESArm.AES_encrypt (Param := AESArm.AES128KBR) AESSpecTest.input AESSpecTest.key = AESSpecTest.output := by native_decide end AESSpecTest From 3e467665db87d752bedf25dbfd58ada3668747f4 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 15 Apr 2024 11:28:22 -0700 Subject: [PATCH 6/6] Update proofs for FFmul02_equiv and FFmul03_equiv --- Specs/AESArm.lean | 32 ++++++--- Tactics/Enum_bv.lean | 166 ------------------------------------------- 2 files changed, 21 insertions(+), 177 deletions(-) delete mode 100644 Tactics/Enum_bv.lean diff --git a/Specs/AESArm.lean b/Specs/AESArm.lean index fc8e1633..13bede96 100644 --- a/Specs/AESArm.lean +++ b/Specs/AESArm.lean @@ -6,7 +6,6 @@ Author(s): Yan Peng import Arm.BitVec import Arm.Insts.DPSFP.Crypto_aes import Specs.AESCommon -import Tactics.Enum_bv -- References : https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.197-upd1.pdf -- https://csrc.nist.gov/csrc/media/projects/cryptographic-standards-and-guidelines/documents/aes-development/rijndael-ammended.pdf @@ -166,21 +165,32 @@ def MixColumns {Param : KBR} (state : BitVec Param.block_size) let FFmul03 := fun (x : BitVec 8) => x ^^^ XTimes x h ▸ AESCommon.MixColumns (h ▸ state) FFmul02 FFmul03 --- set_option maxRecDepth 3000 in --- set_option maxHeartbeats 300000 in --- set_option profiler true in +-- Convert bitvector quantification into bounded natural number quantification +theorem P_of_bv_to_of_nat {n : Nat} {P : BitVec n -> Prop}: + (∀(x : Nat), x < 2^n → P (BitVec.ofNat n x)) → + ∀(p : BitVec n), P p := by + intro H p + let x := p.toNat + have p_eq : p = x#n := by simp only [x, BitVec.ofNat_toNat, truncate_eq] + simp only [p_eq] + apply H + apply BitVec.isLt + +set_option maxRecDepth 1000 in protected theorem FFmul02_equiv : (fun x => XTimes x) = DPSFP.FFmul02 := by funext x - -- enum_bv 8 x - sorry + let P := fun (x : BitVec 8) => XTimes x = DPSFP.FFmul02 x + apply @P_of_bv_to_of_nat 8 P + simp only [P] + decide --- set_option maxRecDepth 3000 in --- set_option maxHeartbeats 300000 in --- set_option profiler true in +set_option maxRecDepth 1000 in protected theorem FFmul03_equiv : (fun x => x ^^^ XTimes x) = DPSFP.FFmul03 := by funext x - -- enum_bv 8 x - sorry + let P := fun (x : BitVec 8) => x ^^^ XTimes x = DPSFP.FFmul03 x + apply @P_of_bv_to_of_nat 8 P + simp only [P] + decide theorem MixColumns_table_lookup_equiv {Param : KBR} (state : BitVec Param.block_size): diff --git a/Tactics/Enum_bv.lean b/Tactics/Enum_bv.lean deleted file mode 100644 index 474e4f69..00000000 --- a/Tactics/Enum_bv.lean +++ /dev/null @@ -1,166 +0,0 @@ -/- -Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author(s): Yan Peng --/ -import Lean.Elab -import Lean.Expr - -open BitVec - -theorem le_and_ne_implies_lt (x : Nat) (y : Nat) (h0 : x ≠ y) (h1 : x ≤ y): x < y := by - have h : x < y ∨ x = y := by apply Nat.lt_or_eq_of_le h1 - cases h - · assumption - · contradiction - --- An example --- def carry_less_add (x : BitVec 2) : BitVec 2 := x ^^^ 0b1#2 --- def lookup_cla (x : BitVec 2) : BitVec 2 := --- BitVec.cast (by omega) $ --- if x.toNat == 0 then 0b01#2 --- else if x.toNat == 1 then 0b0#2 --- else if x.toNat == 2 then 0b11#2 --- else 0b10#2 - --- theorem example_lemma_expanded : carry_less_add = lookup_cla := by --- funext x --- by_cases h₀ : x = BitVec.ofNat 2 0 --- case pos => --- simp only [h₀] --- decide --- case neg => --- by_cases h₁ : x = BitVec.ofNat 2 1 --- case pos => --- simp only [h₁] --- decide --- case neg => --- by_cases h₂ : x = BitVec.ofNat 2 2 --- case pos => --- simp [h₂] --- decide --- case neg => --- by_cases h₃ : x = BitVec.ofNat 2 3 --- case pos => --- simp [h₃] --- decide --- case neg => --- rw [← ne_eq, toNat_ne] at * --- have p4 : x.toNat < 4 := by --- exact isLt x --- have p3' : x.toNat ≤ 3 := by --- apply Nat.le_of_lt_succ --- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p4] --- have p3 : x.toNat < 3 := by --- apply le_and_ne_implies_lt --- · exact h₃ --- · simp only [p3'] --- have p2' : x.toNat ≤ 2 := by --- apply Nat.le_of_lt_succ --- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p3] --- have p2 : x.toNat < 2 := by --- apply le_and_ne_implies_lt --- · exact h₂ --- · simp only [p2'] --- have p1' : x.toNat ≤ 1 := by --- apply Nat.le_of_lt_succ --- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p2] --- have p1 : x.toNat < 1 := by --- apply le_and_ne_implies_lt --- · exact h₁ --- · simp only [p1'] --- have p0' : x.toNat ≤ 0 := by --- apply Nat.le_of_lt_succ --- simp only [Nat.succ_eq_add_one, Nat.reduceAdd, p1] --- have p0 : x.toNat = 0 := by --- exact Nat.eq_zero_of_le_zero p0' --- contradiction - -partial def shrink (i : Nat) (N : Nat) (var : Lean.Ident) - : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do - let i_str := toString i - let i_num := Lean.Syntax.mkNumLit i_str - if i = N then - let p_name := - Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str) - let rest ← shrink (i - 1) N var - `(tactic| - (have $p_name:ident : BitVec.toNat $var:ident < $i_num:num := by - exact isLt $var:ident - $rest:tactic)) - else - let i_pre := toString (i + 1) - let p_pre := - Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_pre) - let p_name1 := - Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str ++ "'") - let p_name2 := - Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("p" ++ i_str) - if i ≤ 0 then - `(tactic| - (have $p_name1:ident : BitVec.toNat $var:ident ≤ $i_num:num := by - apply Nat.le_of_lt_succ - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, $p_pre:ident] - clear $p_pre:ident - have $p_name2:ident : BitVec.toNat $var:ident = $i_num:num := by - exact Nat.eq_zero_of_le_zero $p_name1:ident - clear $p_name1:ident)) - else - let h_name := - Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("h" ++ i_str) - let rest ← shrink (i - 1) N var - `(tactic| - (have $p_name1:ident : BitVec.toNat $var:ident ≤ $i_num:num := by - apply Nat.le_of_lt_succ - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, $p_pre:ident] - clear $p_pre:ident - have $p_name2:ident : BitVec.toNat $var:ident < $i_num:num := by - apply le_and_ne_implies_lt - · exact $h_name:ident - · simp only [$p_name1:ident] - clear $p_name1:ident - $rest:tactic)) - -def enum_last_case (n : Nat) (var : Lean.Ident) - : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do - let shrink_tac ← shrink (2 ^ n) (2 ^ n) var - `(tactic| - (rw [← ne_eq, toNat_ne] at * - $shrink_tac:tactic - contradiction) - ) - -partial def enum_cases_syntax (i : Nat) (n : Nat) (var : Lean.Ident) - : Lean.Elab.Tactic.TacticM (Lean.TSyntax `tactic) := do - if 2 ^ n ≤ i - then let last ← enum_last_case n var - `(tactic| $last:tactic) - else - let i_str := toString i - let h_name := Lean.mkIdent $ Lean.Name.mkStr Lean.Name.anonymous ("h" ++ i_str) - let i_num := Lean.Syntax.mkNumLit i_str - let n_num := Lean.Syntax.mkNumLit $ toString n - let rest ← enum_cases_syntax (i + 1) n var - `(tactic| - (by_cases $h_name:ident : $var:ident = (BitVec.ofNat $n_num:num $i_num:num) - · simp only [$h_name:ident]; decide - · $rest:tactic - done - ) - ) - -def enum_bv_fn (n : Lean.Syntax.NumLit) (var : Lean.Ident): - Lean.Elab.Tactic.TacticM Unit := - Lean.Elab.Tactic.withMainContext do - Lean.Elab.Tactic.evalTactic (← - enum_cases_syntax 0 n.getNat var - ) - --- Establishing a theorem through enumeration of all values of a bit-vector --- Assumption: the theorem has only one free variable of type `BitVec n` -elab "enum_bv" n:num var:ident : tactic => do - enum_bv_fn n var - --- theorem example_lemma : carry_less_add = lookup_cla := by --- funext x --- enum_bv 2 x