From c1edb60458977cbc342f06314f0407b89fcd905d Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Wed, 27 Nov 2024 23:10:42 +0000 Subject: [PATCH 1/8] sha2: fix some typos --- examples/Crypto/SHA-2/sha2Script.sml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index 010599149b..648d129e3b 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -44,7 +44,7 @@ Definition parse_block_def: else parse_block ((word_from_bin_list (TAKE 32 bits))::acc) (DROP 32 bits) Termination WF_REL_TAC`measure (LENGTH o SND)` \\ Cases \\ rw[] -QED +End val () = cv_auto_trans parse_block_def; @@ -54,7 +54,7 @@ Definition parse_message_def: parse_message (parse_block [] (TAKE 512 bits) :: acc) (DROP 512 bits) Termination WF_REL_TAC`measure (LENGTH o SND)` \\ Cases \\ rw[] -QED +End val () = cv_auto_trans parse_message_def; @@ -121,6 +121,7 @@ val () = cv_auto_trans initial_schedule_def; Definition process_block_def: process_block block +*) (* cv_eval``parse_message [] (pad_message [ From 3f159527596842b3c28b6571ba6c2785a62e187a Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Thu, 28 Nov 2024 23:17:15 +0000 Subject: [PATCH 2/8] Fix pad_message and prove cheat --- examples/Crypto/SHA-2/sha2Script.sml | 31 ++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index 648d129e3b..ffca2f339d 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -1,7 +1,7 @@ open HolKernel boolLib bossLib Parse - listTheory rich_listTheory arithmeticTheory - wordsTheory numposrepTheory byteTheory wordsLib - cv_transLib cv_stdTheory + listTheory rich_listTheory arithmeticTheory logrootTheory + bitTheory wordsTheory numposrepTheory byteTheory wordsLib + dividesTheory cv_transLib cv_stdTheory (* The SHA-2 Standard: https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf *) (* SHA-256 in particular (i.e. Section 6.2) *) @@ -21,7 +21,7 @@ val () = cv_auto_trans numposrepTheory.n2l_n2lA; Definition pad_message_def: pad_message bs = let l = LENGTH bs in - let n = l + 1 MOD 512 in + let n = (l + 1) MOD 512 in let k = if n <= 448 then 448 - n else 512 + 448 - n in let lb = PAD_LEFT 0 64 $ (if l = 0 then [] else REVERSE $ n2l 2 l) in let bits = MAP bool_to_bit bs in @@ -34,8 +34,27 @@ Theorem pad_message_length_multiple: LENGTH bs < 2 ** 64 ==> divides 512 $ LENGTH (pad_message bs) Proof - rw[pad_message_def, PAD_LEFT, LENGTH_n2l, ADD1] - \\ cheat + rewrite_tac[pad_message_def, PAD_LEFT, ADD1] + \\ strip_tac + \\ BasicProvers.LET_ELIM_TAC + \\ rw[Abbr`bits`] + \\ Cases_on`l = 0` \\ gs[Abbr`n`, Abbr`lb`, Abbr`k`] + \\ simp[LENGTH_n2l, ADD1, LOG2_def] + \\ `LOG2 l < 64` + by ( qspecl_then[`l`,`64`]mp_tac LT_TWOEXP \\ simp[] ) + \\ gs[LOG2_def] + \\ qspec_then `512` mp_tac DIVISION + \\ impl_tac >- rw[] + \\ disch_then(qspec_then`l + 1`mp_tac) + \\ strip_tac + \\ qpat_x_assum`l + 1 = _`(assume_tac o SYM) + \\ `(l + 1) MOD 512 = l + 1 - (l + 1) DIV 512 * 512` by simp[] + \\ pop_assum SUBST1_TAC + \\ IF_CASES_TAC + \\ simp[] + \\ irule DIVIDES_ADD_1 + \\ simp[] + \\ simp[divides_def] QED Definition parse_block_def: From 220cfa104b80d0713bba0f765572ce5182c4e58f Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 29 Nov 2024 10:56:31 +0000 Subject: [PATCH 3/8] Prove initial_schedule_loop_pre --- examples/Crypto/SHA-2/sha2Script.sml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index ffca2f339d..12382d6ddf 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -111,7 +111,7 @@ val () = cv_auto_trans sigma1_def; Definition initial_schedule_loop_def: initial_schedule_loop Ws t = - if t >= 64 \/ LENGTH Ws < t then + if t ≥ 64 ∨ t < 16 ∨ LENGTH Ws < t then REVERSE Ws else let Wt2 = EL 1 Ws; @@ -127,9 +127,13 @@ End val initial_schedule_loop_pre_def = cv_auto_trans_pre initial_schedule_loop_def; -(* Theorem initial_schedule_loop_pre[cv_pre]: - initial_schedule_loop_pre + ∀Ws t. initial_schedule_loop_pre Ws t +Proof + ho_match_mp_tac initial_schedule_loop_ind + \\ rw[initial_schedule_loop_def] + \\ rw[Once initial_schedule_loop_pre_def] +QED Definition initial_schedule_def: initial_schedule block = @@ -138,6 +142,7 @@ End val () = cv_auto_trans initial_schedule_def; +(* Definition process_block_def: process_block block *) From f73067adc351bb95e895a07d7ded027fea536f29 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 29 Nov 2024 12:34:04 +0000 Subject: [PATCH 4/8] Define SHA-256 Make it take nums instead of bools to start with. There is still something wrong with byte order or something here (comparing against test vectors). --- examples/Crypto/SHA-2/sha2Script.sml | 148 ++++++++++++++++++++++----- 1 file changed, 125 insertions(+), 23 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index 12382d6ddf..234ad973db 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -8,23 +8,15 @@ open HolKernel boolLib bossLib Parse val _ = new_theory"sha2"; -(* TODO: move *) -Definition bool_to_bit_def: - bool_to_bit b = if b then 1 else 0n -End - -val () = cv_auto_trans bool_to_bit_def; - (* TODO: move *) val () = cv_auto_trans numposrepTheory.n2l_n2lA; Definition pad_message_def: - pad_message bs = - let l = LENGTH bs in + pad_message bits = + let l = LENGTH bits in let n = (l + 1) MOD 512 in let k = if n <= 448 then 448 - n else 512 + 448 - n in let lb = PAD_LEFT 0 64 $ (if l = 0 then [] else REVERSE $ n2l 2 l) in - let bits = MAP bool_to_bit bs in bits ++ 1 :: REPLICATE k 0 ++ lb End @@ -37,7 +29,6 @@ Proof rewrite_tac[pad_message_def, PAD_LEFT, ADD1] \\ strip_tac \\ BasicProvers.LET_ELIM_TAC - \\ rw[Abbr`bits`] \\ Cases_on`l = 0` \\ gs[Abbr`n`, Abbr`lb`, Abbr`k`] \\ simp[LENGTH_n2l, ADD1, LOG2_def] \\ `LOG2 l < 64` @@ -78,16 +69,16 @@ End val () = cv_auto_trans parse_message_def; Definition initial_hash_value_def: - initial_hash_value : word32 list = [ - 0x6a09e667w; - 0xbb67ae85w; - 0x3c6ef372w; - 0xa54ff53aw; - 0x510e527fw; - 0x9b05688cw; - 0x1f83d9abw; - 0x5be0cd19w - ] + initial_hash_value = ( + 0x6a09e667w : word32, + 0xbb67ae85w : word32, + 0x3c6ef372w : word32, + 0xa54ff53aw : word32, + 0x510e527fw : word32, + 0x9b05688cw : word32, + 0x1f83d9abw : word32, + 0x5be0cd19w : word32 + ) End val () = cv_trans_deep_embedding EVAL initial_hash_value_def; @@ -109,6 +100,17 @@ End val () = cv_auto_trans sigma0_def; val () = cv_auto_trans sigma1_def; +Definition Sigma0_def: + Sigma0 (x: word32) = rotr 2 x ?? rotr 13 x ?? rotr 22 x +End + +Definition Sigma1_def: + Sigma1 (x: word32) = rotr 6 x ?? rotr 11 x ?? rotr 25 x +End + +val () = cv_auto_trans Sigma0_def; +val () = cv_auto_trans Sigma1_def; + Definition initial_schedule_loop_def: initial_schedule_loop Ws t = if t ≥ 64 ∨ t < 16 ∨ LENGTH Ws < t then @@ -142,9 +144,109 @@ End val () = cv_auto_trans initial_schedule_def; -(* +Definition K_def: + K: word32 list = [ + 0x428a2f98w; 0x71374491w; 0xb5c0fbcfw; 0xe9b5dba5w; 0x3956c25bw; 0x59f111f1w; 0x923f82a4w; 0xab1c5ed5w; + 0xd807aa98w; 0x12835b01w; 0x243185bew; 0x550c7dc3w; 0x72be5d74w; 0x80deb1few; 0x9bdc06a7w; 0xc19bf174w; + 0xe49b69c1w; 0xefbe4786w; 0x0fc19dc6w; 0x240ca1ccw; 0x2de92c6fw; 0x4a7484aaw; 0x5cb0a9dcw; 0x76f988daw; + 0x983e5152w; 0xa831c66dw; 0xb00327c8w; 0xbf597fc7w; 0xc6e00bf3w; 0xd5a79147w; 0x06ca6351w; 0x14292967w; + 0x27b70a85w; 0x2e1b2138w; 0x4d2c6dfcw; 0x53380d13w; 0x650a7354w; 0x766a0abbw; 0x81c2c92ew; 0x92722c85w; + 0xa2bfe8a1w; 0xa81a664bw; 0xc24b8b70w; 0xc76c51a3w; 0xd192e819w; 0xd6990624w; 0xf40e3585w; 0x106aa070w; + 0x19a4c116w; 0x1e376c08w; 0x2748774cw; 0x34b0bcb5w; 0x391c0cb3w; 0x4ed8aa4aw; 0x5b9cca4fw; 0x682e6ff3w; + 0x748f82eew; 0x78a5636fw; 0x84c87814w; 0x8cc70208w; 0x90befffaw; 0xa4506cebw; 0xbef9a3f7w; 0xc67178f2w; + ] +End + +val () = cv_trans_deep_embedding EVAL K_def; + +Definition Ch_def: + Ch (x:word32) y z = (x && y) ?? (¬x && z) +End + +val () = cv_auto_trans Ch_def; + +Definition Maj_def: + Maj (x:word32) y z = (x && y) ?? (x && z) ?? (y && z) +End + +val () = cv_auto_trans Maj_def; + +Definition step3_def: + step3 Ws (t, (a, b, c, d, e, f, g, h)) = let + t1 = h + Sigma1 e + Ch e f g + + if t < 64 then EL t K else 0w + + if t < LENGTH Ws then EL t Ws else 0w; + t2 = Sigma0 a + Maj a b c; + h = g; + g = f; + f = e; + e = d + t1; + d = c; + c = b; + b = a; + a = t1 + t2 in + (SUC t, (a, b, c, d, e, f, g, h)) +End + +val step3_pre_def = cv_auto_trans_pre step3_def; + +Theorem step3_pre[cv_pre]: + step3_pre Ws v +Proof + rw[step3_pre_def, K_def] +QED + Definition process_block_def: - process_block block + process_block hash block = let + Ws = initial_schedule block; + hs = FUNPOW (step3 Ws) 64 (0, hash); + in case (hash, hs) of ((a0,b0,c0,d0,e0,f0,g0,h0),(_,(a,b,c,d,e,f,g,h))) + => (a0+a, b0+b, c0+c, d0+d, e0+e, f0+f, g0+g, h0+h) +End + +val () = cv_auto_trans process_block_def; + +Definition process_blocks_def: + process_blocks bs = FOLDL process_block initial_hash_value bs +End + +val () = cv_auto_trans process_blocks_def; + +Definition SHA_256_def: + SHA_256 m : 256 word = let + p = pad_message m; + blocks = parse_message [] p + in + case process_blocks blocks of + (a, b, c, d, e, f, g, h) + => concat_word_list [h; g; f; e; d; c; b; a] +End + +val () = cv_auto_trans SHA_256_def; + +Definition SHA_256_bytes_def: + SHA_256_bytes (bs: word8 list) = + SHA_256 $ FLAT $ + MAP (PAD_RIGHT 0 8 o word_to_bin_list) bs +End + +val () = cv_auto_trans SHA_256_bytes_def; + +(* +cv_eval `` + parse_message [] $ + pad_message $ + FLAT $ MAP (PAD_RIGHT 0 8 o word_to_bin_list) ([97w; 98w; 99w]: word8 list) +`` + +Theorem SHA_256_bytes_abc: + SHA_256_bytes (MAP (n2w o ORD) "abc") = + 0xBA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015ADw +Proof + CONV_TAC(PATH_CONV"lrr"EVAL) + \\ (fn g => + top_goal() |> #2 |> lhs |> cv_eval + EVAL``ORD #"a"`` *) (* From 12f48eef151989eb1de1310f7c524880a3e8850c Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 29 Nov 2024 15:20:08 +0000 Subject: [PATCH 5/8] Attempt to debug some endianness issues in sha2 --- examples/Crypto/SHA-2/sha2Script.sml | 51 +++++++++++++++++++++++++--- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index 234ad973db..0797f285b5 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -51,7 +51,9 @@ QED Definition parse_block_def: parse_block acc bits = if NULL bits then REVERSE acc : word32 list - else parse_block ((word_from_bin_list (TAKE 32 bits))::acc) (DROP 32 bits) + else parse_block + ((word_from_bin_list $ REVERSE $ TAKE 32 bits)::acc) + (DROP 32 bits) Termination WF_REL_TAC`measure (LENGTH o SND)` \\ Cases \\ rw[] End @@ -139,7 +141,7 @@ QED Definition initial_schedule_def: initial_schedule block = - initial_schedule_loop block 16 + initial_schedule_loop (REVERSE block) 16 End val () = cv_auto_trans initial_schedule_def; @@ -227,18 +229,59 @@ val () = cv_auto_trans SHA_256_def; Definition SHA_256_bytes_def: SHA_256_bytes (bs: word8 list) = SHA_256 $ FLAT $ - MAP (PAD_RIGHT 0 8 o word_to_bin_list) bs + MAP (REVERSE o PAD_RIGHT 0 8 o word_to_bin_list) bs End val () = cv_auto_trans SHA_256_bytes_def; (* + cv_eval `` +let blocks = parse_message [] $ pad_message $ - FLAT $ MAP (PAD_RIGHT 0 8 o word_to_bin_list) ([97w; 98w; 99w]: word8 list) + FLAT $ MAP (REVERSE o PAD_RIGHT 0 8 o word_to_bin_list) ([97w; 98w; 99w]: word8 list) + ; + block = HD blocks; + Ws = initial_schedule block; + hashi = initial_hash_value; + hash0 = step3 Ws (0, hashi) +in (Ws, hash0) `` +t1 + t2 should be 5D6AEBCD but currently FC08884D +d + t1 should be FA2A4622 but currently 98C7E2A2 +d is A54FF53A + 54DA50E8 + FA2A4622 + + cv_eval``(0xA54FF53Aw:word32) + 0x54DA50E8w`` + 0xFA2A4622 + + 18-4 + 0xa +8 +0xFA2A4622 - 0xA54FF53A + +correct t1 is 0x54DA50E8w +current t1 is + cv_eval``0x5BE0CD19w + Sigma1 0x510e527fw + + Ch 0x510e527fw 0x9b05688cw 0x1f83d9abw`` + + cv_eval``Ch 0x510e527fw 0x9b05688cw 0x1f83d9abw`` + +current t2 is 0x8909AE5w + cv_eval``Sigma0 0x6A09E667w + Maj 0x6A09E667w 0xBB67AE85w 0x3C6EF372w`` + +cv_eval``(0x54DA50E8w:word32) + 0x8909AE5w`` + +correct t2 is 0xCAA988C3w + +cv_eval``(0x54DA50E8w:word32) + 0xCAA988C3w`` +1F83D9AB + + +cv_eval``EL 0 K`` + Theorem SHA_256_bytes_abc: SHA_256_bytes (MAP (n2w o ORD) "abc") = 0xBA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015ADw From 3aa3fab80f963db087ad23e86cff8d4a97ef8686 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sat, 30 Nov 2024 13:25:01 +0000 Subject: [PATCH 6/8] Fix bug, two SHA-256 tests now pass --- examples/Crypto/SHA-2/sha2Script.sml | 73 +++++----------------------- 1 file changed, 13 insertions(+), 60 deletions(-) diff --git a/examples/Crypto/SHA-2/sha2Script.sml b/examples/Crypto/SHA-2/sha2Script.sml index 0797f285b5..debe849281 100644 --- a/examples/Crypto/SHA-2/sha2Script.sml +++ b/examples/Crypto/SHA-2/sha2Script.sml @@ -176,8 +176,8 @@ val () = cv_auto_trans Maj_def; Definition step3_def: step3 Ws (t, (a, b, c, d, e, f, g, h)) = let t1 = h + Sigma1 e + Ch e f g + - if t < 64 then EL t K else 0w + - if t < LENGTH Ws then EL t Ws else 0w; + (if t < 64 then EL t K else 0w) + + (if t < LENGTH Ws then EL t Ws else 0w); t2 = Sigma0 a + Maj a b c; h = g; g = f; @@ -234,68 +234,21 @@ End val () = cv_auto_trans SHA_256_bytes_def; -(* - -cv_eval `` -let blocks = - parse_message [] $ - pad_message $ - FLAT $ MAP (REVERSE o PAD_RIGHT 0 8 o word_to_bin_list) ([97w; 98w; 99w]: word8 list) - ; - block = HD blocks; - Ws = initial_schedule block; - hashi = initial_hash_value; - hash0 = step3 Ws (0, hashi) -in (Ws, hash0) -`` - -t1 + t2 should be 5D6AEBCD but currently FC08884D -d + t1 should be FA2A4622 but currently 98C7E2A2 -d is A54FF53A - 54DA50E8 - FA2A4622 - - cv_eval``(0xA54FF53Aw:word32) + 0x54DA50E8w`` - 0xFA2A4622 - - 18-4 - 0xa +8 -0xFA2A4622 - 0xA54FF53A - -correct t1 is 0x54DA50E8w -current t1 is - cv_eval``0x5BE0CD19w + Sigma1 0x510e527fw + - Ch 0x510e527fw 0x9b05688cw 0x1f83d9abw`` - - cv_eval``Ch 0x510e527fw 0x9b05688cw 0x1f83d9abw`` - -current t2 is 0x8909AE5w - cv_eval``Sigma0 0x6A09E667w + Maj 0x6A09E667w 0xBB67AE85w 0x3C6EF372w`` - -cv_eval``(0x54DA50E8w:word32) + 0x8909AE5w`` - -correct t2 is 0xCAA988C3w - -cv_eval``(0x54DA50E8w:word32) + 0xCAA988C3w`` -1F83D9AB - - -cv_eval``EL 0 K`` - Theorem SHA_256_bytes_abc: SHA_256_bytes (MAP (n2w o ORD) "abc") = 0xBA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015ADw Proof CONV_TAC(PATH_CONV"lrr"EVAL) - \\ (fn g => - top_goal() |> #2 |> lhs |> cv_eval - EVAL``ORD #"a"`` -*) - -(* -cv_eval``parse_message [] (pad_message [ - F;T;T;F;F;F;F;T; F;T;T;F;F;F;T;F; F;T;T;F;F;F;T;T -])`` -*) + \\ (fn g => (g |> #2 |> lhs |> cv_eval |> ACCEPT_TAC) g) +QED + +Theorem SHA_256_bytes_two_blocks: + SHA_256_bytes (MAP (n2w o ORD) + "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq") = + 0x248D6A61D20638B8E5C026930C3E6039A33CE45964FF2167F6ECEDD419DB06C1w +Proof + CONV_TAC(PATH_CONV"lrr"EVAL) + \\ (fn g => (g |> #2 |> lhs |> cv_eval |> ACCEPT_TAC) g) +QED val _ = export_theory(); From 7dc6e0bcc2fb8f13a305a162859b0c2569a07bdc Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Tue, 3 Dec 2024 09:34:27 +0000 Subject: [PATCH 7/8] Add SHA-2 to selftest level 1 examples --- src/parallel_builds/core/Holmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile index fdf7c628d0..4ef8ca1c3f 100644 --- a/src/parallel_builds/core/Holmakefile +++ b/src/parallel_builds/core/Holmakefile @@ -32,7 +32,7 @@ ifdef HOLSELFTESTLEVEL # example directories to build at selftest level 1 EXDIRS = algebra/aat \ arm/arm6-verification arm/armv8-memory-model arm/experimental \ - CCS Crypto/RSA Hoare-for-divergence MLsyntax \ + CCS Crypto/RSA Crypto/SHA-2 Hoare-for-divergence MLsyntax \ PSL/1.01/executable-semantics PSL/1.1/official-semantics \ STE algorithms computability countchars dependability dev \ developers/ThmSetData \ From 2671dafc0ba36144c38be013ce39368b78ea600a Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Mon, 9 Dec 2024 10:09:47 +0000 Subject: [PATCH 8/8] Add Holmakefile with cv trans dependency --- examples/Crypto/SHA-2/Holmakefile | 1 + 1 file changed, 1 insertion(+) create mode 100644 examples/Crypto/SHA-2/Holmakefile diff --git a/examples/Crypto/SHA-2/Holmakefile b/examples/Crypto/SHA-2/Holmakefile new file mode 100644 index 0000000000..12a3526880 --- /dev/null +++ b/examples/Crypto/SHA-2/Holmakefile @@ -0,0 +1 @@ +INCLUDES = $(HOLDIR)/src/num/theories/cv_compute/automation