Theory FIPS180_4
theory FIPS180_4
imports Words
begin
text ‹ https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf
In this theory, we translate the NIST standard 180-4, the Secure Hash Standard, to Isabelle. We
aim to adhere as closely to the written standard as possible, including function and variable
names and overall document structure. It should be clear to any reader, regardless of their
experience with Isabelle, that this exactly matches the standard. We will include direct
quotations from the standard to aid the reader.
We have translated the Secure Hash Standard so that each of the Secure Hash Algorithms is
a function from natural numbers to natural numbers. This allows us the flexibility to apply
the SHA definition to any implementation, whether that implementation acts on natural numbers, bit
strings, octet (i.e., byte) strings, or (generically) n-bit word strings. See the final section
below, called Octets, for versions of the secure hash algorithms as functions on octets.
"This Standard specifies secure hash algorithms, SHA-1, SHA-224, SHA-256, SHA-384, SHA-512,
SHA-512/224 and SHA-512/256. All of the algorithms are iterative, one-way hash functions that can
process a message to produce a condensed representation called a message digest. These algorithms
enable the determination of a message's integrity: any change to the message will, with a very high
probability, result in a different message digest. This property is useful in the generation and
verification of digital signatures and message authentication codes, and in the generation of
random numbers or bits.
Each algorithm can be described in two stages: preprocessing and hash computation. Preprocessing
involves padding a message, parsing the padded message into m-bit blocks, and setting initialization
values to be used in the hash computation. The hash computation generates a message schedule from
the padded message and uses that schedule, along with functions, constants, and word operations to
iteratively generate a series of hash values. The final hash value generated by the hash
computation is used to determine the message digest.
The algorithms differ most significantly in the security strengths that are provided for the data
being hashed. The security strengths of these hash functions and the system as a whole when
each of them is used with other cryptographic algorithms, such as digital signature algorithms
and keyed-hash message authentication codes, can be found in [SP 800-57] and [SP 800-107].
Additionally, the algorithms differ in terms of the size of the blocks and words of data that are
used during hashing or message digest sizes. Figure 1 presents the basic properties of these hash
algorithms.
Algorithm Message Size Block Size Word Size Message Digest Size
SHA-1 < 2^64 512 32 160
SHA-224 < 2^64 512 32 224
SHA-256 < 2^64 512 32 256
SHA-384 < 2^128 1024 64 384
SHA-512 < 2^128 1024 64 512
SHA-512/224 < 2^128 1024 64 224
SHA-512/256 < 2^128 1024 64 256
"›
section ‹2. Definitions›
text ‹"Left-shift operation, where x << n is obtained by discarding the left-most n bits of the
word x and then padding the result with n zeroes on the right." So we need to know the word size w
for x in order to discard the top n out of w bits. For this standard, the word size is either
w = 32 or w = 64.›
definition SHL :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"SHL w n x = (x mod 2^(w-n)) * 2^n"
abbreviation SHL32 :: "nat ⇒ nat ⇒ nat" where
"SHL32 n x ≡ SHL 32 n x"
abbreviation SHL64 :: "nat ⇒ nat ⇒ nat" where
"SHL64 n x ≡ SHL 64 n x"
lemma SHL_0:
assumes "x < 2^w"
shows "SHL w 0 x = x"
by (simp add: SHL_def assms)
lemma SHL_w: "SHL w w x = 0"
by (simp add: SHL_def)
lemma SHL_n_ge_w:
assumes "w ≤ n"
shows "SHL w n x = 0"
by (simp add: SHL_def assms)
lemma SHL_bnd:
assumes "n < w"
shows "SHL w n x < 2^w"
using assms by (simp add: SHL_def flip: mult_exp_mod_exp_eq)
lemma SHL_mod: "(SHL w n x) mod 2^n = 0"
by (simp add: SHL_def)
lemma SHL_div: "(SHL w n x) div 2^n < 2^(w-n)"
by (simp add: SHL_def)
text ‹"Right-shift operation, where x >> n is obtained by discarding the right-most n bits of the
word x and then padding the result with n zeroes on the left." Here we do not need to know the
word size w.›
definition SHR :: "nat ⇒ nat ⇒ nat" where
"SHR n x = x div 2^n"
lemma SHR_0: "SHR 0 x = x"
by (simp add: SHR_def)
lemma SHR_w:
assumes "x < 2^w"
shows "SHR w x = 0"
by (simp add: SHR_def assms)
lemma SHR_n_ge_w:
assumes "x < 2^w" "w ≤ n"
shows "SHR n x = 0"
by (metis SHR_w assms div_less dual_order.strict_trans2 le_less_linear power_diff power_not_zero
zero_neq_numeral)
lemma SHR_less: "SHR n x ≤ x"
by (simp add: SHR_def)
lemma SHR_bnd1:
assumes "x < 2^w"
shows "SHR n x < 2^w"
by (meson SHR_less assms dual_order.trans leD leI)
lemma SHR_bnd2:
assumes "x ≤ 2^w"
shows "SHR n x ≤ 2^(w-n)"
proof -
have 1: "x div 2^n ≤ 2^w div 2^n" using assms(1) div_le_mono by presburger
have 2: "(2::nat)^w div 2^n ≤ 2^(w-n)" by (simp add: exp_div_exp_eq)
show ?thesis using SHR_def 1 2 by auto
qed
text ‹"The rotate left (circular left shift) operation, where x is a w-bit word and n is an integer
with 0 <= n < w, is defined b ROTL n x =(x << n) \/ (x >> w - n)." ›
definition ROTL :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"ROTL w n x = (SHL w n x) + (SHR (w-n) x)"
abbreviation ROTL32 :: "nat ⇒ nat ⇒ nat" where
"ROTL32 n x ≡ ROTL 32 n x"
abbreviation ROTL64 :: "nat ⇒ nat ⇒ nat" where
"ROTL64 n x ≡ ROTL 64 n x"
lemma ROTL_0:
assumes "x < 2^w"
shows "ROTL w 0 x = x"
by (simp add: ROTL_def SHL_0 SHR_w assms)
lemma ROTL_OR:
assumes "x < 2^w" "n < w"
shows "ROTL w n x = (SHL w n x) OR (SHR (w-n) x)"
proof -
have 1: "SHR (w-n) x < 2^n"
by (metis SHR_def assms le_add_diff_inverse less_imp_le less_mult_imp_div_less power_add)
let ?m = "(x mod 2^(w-n))"
have 2: "SHL w n x = ?m * 2^n" using SHL_def by fast
have 3: "?m * 2^n + (SHR (w-n) x) = ?m * 2^n OR (SHR (w-n) x)"
by (simp add: 1 OR_sum_nat_hilo_2 mult.commute)
show ?thesis using 2 3 ROTL_def by presburger
qed
lemma ROTL_bnd:
assumes "n < w" "x < 2^w"
shows "ROTL w n x < 2^w"
using ROTL_OR SHL_bnd SHR_bnd1 assms nat_OR_upper by presburger
text ‹"The rotate right (circular right shift) operation, where x is a w-bit word and n is an
integer with 0 <= n < w, is defined by ROTR n x =(x >> n) \/ (x << w - n)." ›
definition ROTR :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"ROTR w n x = (SHR n x) + (SHL w (w-n) x)"
abbreviation ROTR32 :: "nat ⇒ nat ⇒ nat" where
"ROTR32 n x ≡ ROTR 32 n x"
abbreviation ROTR64 :: "nat ⇒ nat ⇒ nat" where
"ROTR64 n x ≡ ROTR 64 n x"
lemma ROTL_ROTR_eq:
assumes "n ≤ w"
shows "ROTL w n x = ROTR w (w-n) x"
using ROTL_def ROTR_def assms by force
lemma ROTR_ROTL_eq:
assumes "n ≤ w"
shows "ROTR w n x = ROTL w (w-n) x"
using ROTL_def ROTR_def assms by force
lemma ROTR_0: "ROTR w 0 x = x"
by (simp add: ROTR_def SHL_w SHR_0)
lemma ROTR_OR:
assumes "x < 2^w" "n < w"
shows "ROTR w n x = (SHR n x) OR (SHL w (w-n) x)"
proof -
have 0: "w - (w - n) = n" using assms(2) by fastforce
have 1: "ROTR w n x = ROTL w (w-n) x" by (meson ROTR_ROTL_eq assms(2) nat_less_le)
have 2: "ROTL w (w-n) x = (SHL w (w-n) x) OR (SHR n x)"
by (metis 0 ROTL_OR ROTL_def SHL_w add_cancel_left_left assms(1) diff_is_0_eq' diff_zero
not_le or.commute or.right_neutral)
show ?thesis using 1 2 or.commute by auto
qed
lemma ROTR_bnd:
assumes "n < w" "x < 2^w"
shows "ROTR w n x < 2^w"
by (metis ROTL_bnd ROTR_0 ROTR_ROTL_eq assms diff_less less_nat_zero_code less_or_eq_imp_le
nat_neq_iff)
section ‹4. Functions and Constants›
subsection ‹4.1 Functions›
text ‹NOT for a natural number (nat) with a bit length w or less.›
definition wNOT :: "nat ⇒ nat ⇒ nat" where
"wNOT w x = (2^w - 1) XOR x"
abbreviation NOT32 :: "nat ⇒ nat" where
"NOT32 x ≡ wNOT 32 x"
abbreviation NOT64 :: "nat ⇒ nat" where
"NOT64 x ≡ wNOT 64 x"
lemma wNOT_wNOT: "wNOT w (wNOT w x) = x"
by (metis wNOT_def nat_xor_inv xor.commute)
lemma wNOT_bnd:
assumes "x < 2^w"
shows "wNOT w x < 2^w"
by (simp add: assms nat_XOR_upper wNOT_def)
lemma wNOT_XOR:
assumes "x < 2^w"
shows "x XOR (wNOT w x) = 2^w - 1"
using nat_xor_inv wNOT_def by presburger
text ‹Choose›
definition Ch :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
"Ch w x y z = (x AND y) XOR ((wNOT w x) AND z)"
abbreviation Ch32 :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"Ch32 x y z ≡ Ch 32 x y z"
abbreviation Ch64 :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"Ch64 x y z ≡ Ch 64 x y z"
lemma Ch_asymm: "Ch w x y z = Ch w (wNOT w x) z y"
by (simp add: Ch_def wNOT_wNOT xor.commute)
lemma Ch_bnd:
assumes "x < 2^w" "y < 2^w" "z < 2^w"
shows "Ch w x y z < 2^w"
by (simp add: Ch_def and_nat_def assms(1) nat_XOR_upper wNOT_bnd)
lemma Ch_fst:
assumes "y < 2^w" "z < 2^w"
shows "Ch w (2^w-1) y z = y"
by (metis Ch_asymm Ch_def and.commute assms(1) mask_nat_def mod_less take_bit_eq_mask
take_bit_nat_def wNOT_def xor.right_neutral zero_and_eq)
lemma Ch_snd:
assumes "y < 2^w" "z < 2^w"
shows "Ch w 0 y z = z"
by (metis (no_types) Ch_asymm Ch_fst assms wNOT_def xor.comm_neutral)
text ‹Parity›
definition Parity :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"Parity x y z = x XOR y XOR z"
lemma Parity_symm:
"Parity x y z = Parity x z y ∧ Parity x y z = Parity z y x ∧ Parity x y z = Parity y x z ∧
Parity x y z = Parity z x y ∧ Parity x y z = Parity y z x"
by (simp add: Parity_def xor.commute xor.left_commute)
lemma Parity_bnd:
assumes "x < 2^w" "y < 2^w" "z < 2^w"
shows "Parity x y z < 2^w"
by (simp add: Parity_def assms nat_XOR_upper)
lemma Parity_2same: "Parity x y y = x"
using Parity_def Parity_symm nat_xor_inv by presburger
lemma Parity_wNOT:
assumes "x < 2^w" "y < 2^w"
shows "Parity x y (wNOT w y) = wNOT w x"
using Parity_def assms(2) wNOT_XOR wNOT_def xor.commute by force
text ‹Majority vote›
definition Maj :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"Maj x y z = (x AND y) XOR (x AND z) XOR (y AND z)"
lemma Maj_symm:
"Maj x y z = Maj x z y ∧ Maj x y z = Maj z y x ∧ Maj x y z = Maj y x z ∧
Maj x y z = Maj z x y ∧ Maj x y z = Maj y z x"
by (simp add: Maj_def and.commute xor.commute xor.left_commute)
lemma Maj_bnd:
assumes "x < 2^w" "y < 2^w"
shows "Maj x y z < 2^w"
by (simp add: Maj_def and_nat_def assms nat_XOR_upper)
lemma Maj_3same: "Maj x x x = x"
by (metis (no_types) Maj_def and.idem nat_xor_inv)
lemma Maj_2same: "Maj x y y = y"
by (simp add: Maj_def xor_nat_def)
subsubsection ‹4.1.1 SHA-1 Functions›
text ‹"SHA-1 uses a sequence of logical functions, f0, f1,..., f79. Each function ft, where
0 ≤ t ≤ 79, operates on three 32-bit words, x, y, and z, and produces a 32-bit word as output."›
definition SHA1_ft :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
"SHA1_ft t x y z =
( if (t ≤ 19) then (Ch32 x y z)
else if (t ≤ 39) then (Parity x y z)
else if (t ≤ 59) then (Maj x z y)
else (Parity x y z)
)"
lemma SHA1_ft_bnd:
assumes "x < 2^32" "y < 2^32" "z < 2^32"
shows "SHA1_ft t x y z < 2^32"
using Ch_bnd Maj_bnd Parity_bnd SHA1_ft_def assms by presburger
subsubsection ‹4.1.2 SHA-224 and SHA-256 Functions›
text ‹"SHA-224 and SHA-256 both use six logical functions, where each function operates on 32-bit
words, which are represented as x, y, and z. The result of each function is a new 32-bit word."›
definition Sigma256_0 :: "nat ⇒ nat" where
"Sigma256_0 x = (ROTR32 2 x) XOR (ROTR32 13 x) XOR (ROTR32 22 x)"
definition Sigma256_1 :: "nat ⇒ nat" where
"Sigma256_1 x = (ROTR32 6 x) XOR (ROTR32 11 x) XOR (ROTR32 25 x)"
definition sigma256_0 :: "nat ⇒ nat" where
"sigma256_0 x = (ROTR32 7 x) XOR (ROTR32 18 x) XOR (SHR 3 x)"
definition sigma256_1 :: "nat ⇒ nat" where
"sigma256_1 x = (ROTR32 17 x) XOR (ROTR32 19 x) XOR (SHR 10 x)"
lemma Sigma256s_bnd:
assumes "x < 2^32" "a < 32" "b < 32" "c < 32"
shows "(ROTR32 a x) XOR (ROTR32 b x) XOR (ROTR32 c x) < 2^32"
by (meson ROTR_bnd assms nat_XOR_upper)
lemma Sigma256_0_bnd:
assumes "x < 2^32"
shows "Sigma256_0 x < 2^32"
by (metis Sigma256s_bnd Sigma256_0_def assms numeral_less_iff semiring_norm(76,78,81))
lemma Sigma256_1_bnd:
assumes "x < 2^32"
shows "Sigma256_1 x < 2^32"
by (metis Sigma256s_bnd Sigma256_1_def assms numeral_less_iff semiring_norm(76,78,81))
lemma sigma256s_bnd:
assumes "x < 2^32" "a < 32" "b < 32" "c < 32"
shows "(ROTR32 a x) XOR (ROTR32 b x) XOR (SHR c x) < 2^32"
using ROTR_bnd SHR_bnd1 assms nat_XOR_upper by presburger
lemma sigma256_0_bnd:
assumes "x < 2^32"
shows "sigma256_0 x < 2^32"
by (metis sigma256s_bnd sigma256_0_def assms numeral_less_iff semiring_norm(76,78,81))
lemma sigma256_1_bnd:
assumes "x < 2^32"
shows "sigma256_1 x < 2^32"
by (metis sigma256s_bnd sigma256_1_def assms numeral_less_iff semiring_norm(76,78,81))
subsubsection ‹4.1.3 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 Functions›
text ‹"SHA-384, SHA-512, SHA-512/224 and SHA-512/256 use six logical functions, where each
function operates on 64-bit words, which are represented as x, y, and z. The result of each
function is a new 64-bit word."›
definition Sigma512_0 :: "nat ⇒ nat" where
"Sigma512_0 x = (ROTR64 28 x) XOR (ROTR64 34 x) XOR (ROTR64 39 x)"
definition Sigma512_1 :: "nat ⇒ nat" where
"Sigma512_1 x = (ROTR64 14 x) XOR (ROTR64 18 x) XOR (ROTR64 41 x)"
definition sigma512_0 :: "nat ⇒ nat" where
"sigma512_0 x = (ROTR64 1 x) XOR (ROTR64 8 x) XOR (SHR 7 x)"
definition sigma512_1 :: "nat ⇒ nat" where
"sigma512_1 x = (ROTR64 19 x) XOR (ROTR64 61 x) XOR (SHR 6 x)"
lemma Sigma512s_bnd:
assumes "x < 2^64" "a < 64" "b < 64" "c < 64"
shows "(ROTR64 a x) XOR (ROTR64 b x) XOR (ROTR64 c x) < 2^64"
by (meson ROTR_bnd assms nat_XOR_upper)
lemma Sigma512_0_bnd:
assumes "x < 2^64"
shows "Sigma512_0 x < 2^64"
using Sigma512s_bnd Sigma512_0_def assms numeral_less_iff semiring_norm(76,78,81) by auto
lemma Sigma512_1_bnd:
assumes "x < 2^64"
shows "Sigma512_1 x < 2^64"
using Sigma512s_bnd Sigma512_1_def assms numeral_less_iff semiring_norm(76,78,81) by simp
lemma sigma512s_bnd:
assumes "x < 2^64" "a < 64" "b < 64" "c < 64"
shows "(ROTR64 a x) XOR (ROTR64 b x) XOR (SHR c x) < 2^64"
using ROTR_bnd SHR_bnd1 assms nat_XOR_upper by presburger
lemma sigma512_0_bnd:
assumes "x < 2^64"
shows "sigma512_0 x < 2^64"
using sigma512s_bnd sigma512_0_def assms numeral_less_iff semiring_norm(76,78,81) by auto
lemma sigma512_1_bnd:
assumes "x < 2^64"
shows "sigma512_1 x < 2^64"
by (metis sigma512s_bnd sigma512_1_def assms numeral_less_iff semiring_norm(76,78,81))
subsection ‹4.2 Constants›
subsubsection ‹4.2.1 SHA-1 Constants›
text ‹"SHA-1 uses a sequence of eighty constant 32-bit words, K0, K1,..., K79, which are given by"›
definition SHA1_Kt :: "nat ⇒ nat" where
"SHA1_Kt t =
( if (t ≤ 19) then (0x5a827999)
else if (t ≤ 39) then (0x6ed9eba1)
else if (t ≤ 59) then (0x8f1bbcdc)
else (0xca62c1d6)
)"
lemma SHA1_Kt_bnd: "SHA1_Kt t < 2^32"
unfolding SHA1_Kt_def apply (cases t) by auto
subsubsection ‹4.2.2 SHA-224 and SHA-256 Constants›
text ‹"SHA-224 and SHA-256 use the same sequence of sixty-four constant 32-bit words, K_0^{256},
K_1^{256}, ..., K_63^{256}. These words represent the first thirty-two bits of the fractional
parts of the cube roots of the first sixty-four prime numbers. In hex, these constant words are
(from left to right)"›
definition K256list :: "nat list" where
"K256list =
[0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5,
0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3,
0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc,
0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7,
0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13,
0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3,
0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5,
0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208,
0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2]"
lemma K256_bnd1:
assumes "k ∈ set K256list"
shows "k < 2^32"
using assms unfolding K256list_def apply (cases k) by auto
lemma K256_bnd2:
assumes "i < length K256list"
shows "K256list ! i < 2^32"
using K256_bnd1 assms nth_mem by blast
lemma K256_len [simp]: "length K256list = 64"
unfolding K256list_def by simp
subsubsection ‹4.2.3 SHA-384, SHA-512, SHA-512/224 and SHA-512/256 Constants›
text ‹SHA-384, SHA-512, SHA-512/224 and SHA-512/256 use the same sequence of eighty constant
64-bit words, K_0^{512}, K_1^{512}, ..., K_79^{512}. These words represent the first sixty-four
bits of the fractional parts of the cube roots of the first eighty prime numbers. In hex, these
constant words are (from left to right)›
definition K512list :: "nat list" where
"K512list =
[0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]"
lemma K512_bnd1:
assumes "k ∈ set K512list"
shows "k < 2^64"
using assms unfolding K512list_def apply (cases k) by auto
lemma K512_bnd2:
assumes "i < length K512list"
shows "K512list ! i < 2^64"
using K512_bnd1 assms nth_mem by blast
lemma K512_len [simp]: "length K512list = 80"
unfolding K512list_def by simp
section ‹5. Preprocessing›
subsection ‹5.1/2 Padding and Parsing the Message›
text ‹Note for reasons of convenience, we combine sections 5.1 "Padding the Message" and 5.2
"Parsing the Message" of the FIPS standard into this combined Isabelle section.
From section 5.1:
"The purpose of this padding is to ensure that the padded message is a multiple of 512 or
1024 bits, depending on the algorithm. Padding can be inserted before hash computation begins on
a message, or at any other time during the hash computation prior to processing the block(s) that
will contain the padding."
The padding for the 32-bit-word SHAs and the padding for the 64-bit-word SHAs are very similar.
We define it generically here. From the standard sections 5.1.1 and 5.1.2 only differ in the
values of X and Y:
"Suppose that the length of the message, M, is l bits. Append the bit ``1'' to the end of the
message, followed by k zero bits, where k is the smallest, non-negative solution to the equation
l + 1 + k = [X] mod [X+Y]. Then append the [Y]-bit block that is equal to the number l expressed
using a binary representation."
For us, the message M is viewed as a natural number. We don't know how many leading zero bits are
intended in the bit string version of the message. So we need to be told l, the number of bits of
the message, where bit_length M <= l.
Then section 5.2 states only: "The message and its padding must be parsed into N m-bit blocks."
where N is the number of blocks in the padded message and m is (X+Y). For the SHA1 group of
hash algorithms, m = X+Y = 512. For the SHA512 group, m = X+Y = 1024. Each block is further
parsed into 16 words. For the SHA1 group, the word size is 32 bits, and 32 * 16 = 512. For the
SHA512 group, the word size is 64 and 64 * 16 = 1024. So we introduce the variable W in the
following locale to represent the word size and the only thing we need to know about W at the
moment is that W divides X+Y. Here we skip the step of parsing into blocks. The output of this
parsing is a list of W-bit numbers (words).
›
locale SHA_PadParse =
fixes X Y W :: nat
assumes XYWpos : "0 < X" "0 < Y" "0 < W"
and Wdvd : "W dvd (X+Y)"
begin
definition SHApadding_k :: "nat ⇒ nat" where
"SHApadding_k l =
( let x = (l + 1) mod (X+Y) in
( if x ≤ X then X - x
else X + (X+Y) - x) )"
text ‹First we implement "padding the message" as natural-number arithmetic.›
definition SHApadded :: "nat ⇒ nat ⇒ nat" where
"SHApadded M l = ( let k = (SHApadding_k l) in (2*M + 1)*2^(k+Y) + l )"
definition SHApadded_len :: "nat ⇒ nat" where
"SHApadded_len l = l + 1 + (SHApadding_k l) + Y"
definition SHApadded_numBlocks :: "nat ⇒ nat" where
"SHApadded_numBlocks l = (SHApadded_len l) div (X+Y)"
text ‹We can also define "padding the message" as concatenating strings of bits. Below we prove
that this corresponds to the above arithmetic definition. We include this definition, and the
proof of equality, merely to demonstrate that these definitions exactly match the standard.›
definition SHApadded_asBits :: "nat ⇒ nat ⇒ bits" where
"SHApadded_asBits M l = ( let k = (SHApadding_k l) in
(nat_to_bits_len M l) @ [1] @ (replicate k 0) @ (nat_to_bits_len l Y) )"
definition SHApadded_numWords :: "nat ⇒ nat" where
"SHApadded_numWords l = (SHApadded_numBlocks l) * ((X+Y) div W)"
definition SHA_PaddedParsed :: "nat ⇒ nat ⇒ words" where
"SHA_PaddedParsed M l = nat_to_words_len W (SHApadded M l) (SHApadded_numWords l)"
text ‹The input message M and bit length l only make sense if M < 2^l. Also the padding only works
correctly when l has at most Y bits.›
definition SHA_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA_inputValid M l ≡ (M < 2^l) ∧ (l < 2^Y)"
lemma SHApadding_len_mod1: "(l + 1 + (SHApadding_k l)) mod (X+Y) = X"
proof -
let ?x = "(l + 1) mod (X+Y)"
have 0: "?x < (X+Y)"
by (meson add_pos_pos XYWpos(1,2) mod_less_divisor)
show ?thesis proof (cases "?x ≤ X")
case T0: True
have T1: "SHApadding_k l = X - ?x"
using SHApadding_k_def T0 by presburger
have T2: "(l + 1 + (SHApadding_k l)) mod (X+Y) = (?x + (X - ?x)) mod (X+Y)"
using T1 by presburger
have T3: "(?x + (X - ?x)) mod (X+Y) = X mod (X+Y)"
by (metis T0 le_add_diff_inverse)
show ?thesis by (metis T2 T3 mod_less XYWpos(2) less_add_same_cancel1)
next
case F0: False
have F1: "SHApadding_k l = X + (X+Y) - ?x"
using F0 SHApadding_k_def by presburger
have F2: "(l + 1 + (SHApadding_k l)) mod (X+Y) = (?x + (X + (X+Y) - ?x)) mod (X+Y)"
using F1 by presburger
have F3: "(?x + (X + (X+Y) - ?x)) = X + (X+Y)" using 0 by simp
have F4: "(?x + (X + (X+Y) - ?x)) mod (X+Y) = X mod (X+Y)" using F3 by force
show ?thesis by (metis F2 F4 mod_less XYWpos(2) less_add_same_cancel1)
qed
qed
lemma SHApadding_len_mod2: "(l + 1 + (SHApadding_k l) + Y) mod (X+Y) = 0"
by (metis SHApadding_len_mod1 mod_add_left_eq mod_self)
lemma SHApadded_len_mod: "SHApadded_len l mod (X+Y) = 0"
using SHApadded_len_def SHApadding_len_mod2 by presburger
lemma SHApadded_OR:
assumes "l < 2^Y" "k = SHApadding_k l"
shows "SHApadded M l = ((2*M + 1)*2^(k+Y)) OR l"
proof -
let ?x = "(2*M + 1)*2^k"
have "SHApadded M l = (?x*2^Y) + l"
by (metis assms(2) SHApadded_def mult.assoc power_add)
then show ?thesis
by (smt (z3) assms(1) OR_sum_nat_hilo_2 mult.assoc mult.commute power_add)
qed
lemma SHApadded_bitlen:
assumes "bit_length M ≤ l" "l < 2^Y"
shows "bit_length (SHApadded M l) ≤ SHApadded_len l"
proof -
have 1: "bit_length (2*M+1) = (bit_length M) + 1"
by (metis add.commute add_cancel_left_left add_diff_cancel_left' bit_len_exact3 bit_len_zero_eq
le_add2 less_exp mult.commute nat_0_less_mult_iff nat_less_le power_0 power_one_right
bit_len_shift_add)
let ?k = "SHApadding_k l"
have 2: "0 < 2*M + 1" by simp
have 3: "bit_length ((2*M + 1)*2^?k) = (bit_length M) + 1 + ?k"
using 1 2 bit_len_shift by presburger
have 4: "bit_length (((2*M + 1)*2^(?k+Y)) + l) = (bit_length M) + 1 + ?k + Y"
by (smt (z3) 2 3 assms(2) bit_len_shift_add mult.assoc nat_0_less_mult_iff power_add
zero_less_numeral zero_less_power)
have 5: "bit_length (SHApadded M l) = (bit_length M) + 1 + ?k + Y"
using 4 SHApadded_def by presburger
show ?thesis using assms(1) SHApadded_len_def 5 add_le_mono1 by presburger
qed
lemma SHApadded_bitlen2:
assumes "SHA_inputValid M l"
shows "bit_length (SHApadded M l) ≤ SHApadded_len l"
using SHApadded_bitlen SHA_inputValid_def assms less_bit_len2 by presburger
lemma SHApadded_l:
assumes "P = SHApadded M l" "l < 2^Y"
shows "l = P mod 2^Y"
proof -
let ?k = "SHApadding_k l"
let ?x = "(2*M + 1)*2^?k"
have "P = ?x*2^Y + l" by (metis SHApadded_def assms(1) mult.assoc power_add)
then show ?thesis by (metis assms(2) mod_less mod_mult_self3)
qed
lemma SHApadded_M:
assumes "P = SHApadded M l" "l < 2^Y" "k = SHApadding_k l"
shows "M = P div 2^(k+Y+1)"
proof -
have 1: "P = ((2*M + 1)*2^(k+Y)) + l" using assms(1,3) SHApadded_def by meson
have 2: "l < 2^(k+Y)"
by (metis assms(2) Suc_eq_plus1 le_add2 lessI less_le_trans one_add_one power_increasing_iff)
have 3: "P div 2^(k+Y) = 2*M+1"
by (simp add: 1 2 ab_semigroup_add_class.add_ac(1))
show ?thesis
by (metis 3 div_exp_eq div_mult_self1_is_m dvd_triv_left even_succ_div_two pos2 power_one_right)
qed
lemma SHApadded_asBits_valid: "bits_valid (SHApadded_asBits M l)"
by (simp add: SHApadded_asBits_def nat_to_words_len_valid words_valid_concat words_valid_cons
words_valid_zeros)
lemma SHApadded_asBits_len:
assumes "l < 2^Y" "M < 2^l"
shows "length (SHApadded_asBits M l) = SHApadded_len l"
by (simp add: SHApadded_asBits_def SHApadded_len_def assms nat_to_words_len_upbnd)
lemma SHApadded_asBits_len2:
assumes "SHA_inputValid M l"
shows "length (SHApadded_asBits M l) = SHApadded_len l"
by (meson SHA_inputValid_def SHApadded_asBits_len assms)
lemma SHApadded_asBits_to_nat:
assumes "l < 2^Y"
shows "bits_to_nat (SHApadded_asBits M l) = SHApadded M l"
proof -
let ?k = "SHApadding_k l"
have 1: "SHApadded_asBits M l = (nat_to_bits_len M l)@[1]@(replicate ?k 0)@(nat_to_bits_len l Y)"
using SHApadded_asBits_def by presburger
have l1: "bits_to_nat (nat_to_bits_len l Y) = l"
by (simp add: nat_to_words_len_to_nat)
have l2: "length (nat_to_bits_len l Y) = Y"
by (simp add: assms(1) nat_to_words_len_upbnd)
have k1: "bits_to_nat (replicate ?k 0) = 0"
by (simp add: words_to_zero_intro)
have M1: "bits_to_nat (nat_to_bits_len M l) = M"
by (simp add: nat_to_words_len_to_nat)
have 2: "bits_to_nat ((nat_to_bits_len M l)@[1]) = 2*M+1"
using M1 words_to_nat_append by force
have 3: "bits_to_nat ((nat_to_bits_len M l)@[1]@(replicate ?k 0)) = (2*M+1)*2^?k"
using 2 k1 words_to_nat_concat by force
let ?X = "(nat_to_bits_len M l)@[1]@(replicate ?k 0)"
have 4: "bits_to_nat (?X@(nat_to_bits_len l Y)) = ((2*M+1)*2^?k)*2^Y + l"
by (metis 3 l1 l2 power_one_right words_to_nat_concat)
show ?thesis
by (metis 1 4 SHApadded_def append.assoc mult.assoc power_add)
qed
lemma SHApadded_toBits:
assumes "l < 2^Y" "M < 2^l"
shows "nat_to_bits_len (SHApadded M l) (SHApadded_len l) = SHApadded_asBits M l"
by (metis SHApadded_asBits_len SHApadded_asBits_to_nat SHApadded_asBits_valid assms
words_to_nat_to_words_len2)
lemma SHApadded_toBits2:
assumes "SHA_inputValid M l"
shows "nat_to_bits_len (SHApadded M l) (SHApadded_len l) = SHApadded_asBits M l"
using SHA_inputValid_def SHApadded_toBits assms by presburger
lemma SHApadded_WdvdLen: "W dvd (SHApadded_len l)"
by (meson SHApadded_len_mod Wdvd dvd_eq_mod_eq_0 gcd_nat.trans)
lemma SHApadded_wordLen: "SHApadded_numWords l = (SHApadded_len l) div W"
by (simp add: SHApadded_numWords_def SHApadded_len_mod SHApadded_numBlocks_def Wdvd div_mult_swap
mod_0_imp_dvd)
lemma SHA_parsed_valid: "words_valid W (SHA_PaddedParsed M l)"
by (simp add: SHA_PaddedParsed_def nat_to_words_len_valid)
end
subsubsection ‹5.1/2.1 SHA-1, SHA-224 and SHA-256›
text ‹"Suppose that the length of the message, M, is l bits. Append the bit ``1'' to the end of the
message, followed by k zero bits, where k is the smallest, non-negative solution to the equation
l + 1 + k = 448 mod 512. Then append the 64-bit block that is equal to the number l expressed
using a binary representation."
This matches our generic version above with X = 448 and Y = 64. Then the block size is X+Y = 512.
Then the word size is W = 32, noting that 32 * 16 = 512, so that each block splits into 16 words.›
lemma SHA1parsing_h: "(32::nat) dvd (448 + 64)"
by force
global_interpretation SHA1_PadParse: SHA_PadParse 448 64 32
defines SHA1padding_k = "SHA1_PadParse.SHApadding_k"
and SHA1padded = "SHA1_PadParse.SHApadded"
and SHA1padded_len = "SHA1_PadParse.SHApadded_len"
and SHA1padded_numBlocks = "SHA1_PadParse.SHApadded_numBlocks"
and SHA1padded_asBits = "SHA1_PadParse.SHApadded_asBits"
and SHA1padded_numWords = "SHA1_PadParse.SHApadded_numWords"
and SHA1_PaddedParsed = "SHA1_PadParse.SHA_PaddedParsed"
and SHA1_inputValid = "SHA1_PadParse.SHA_inputValid"
by (simp add: SHA_PadParse_def SHA1parsing_h)
subsubsection ‹5.1/2.2 SHA-384, SHA-512, SHA-512/224 and SHA-512/256›
text ‹"Suppose the length of the message M, in bits, is l bits. Append the bit ``1'' to the end of
the message, followed by k zero bits, where k is the smallest non-negative solution to the equation
l + 1 + k = 896 mod 1024. Then append the 128-bit block that is equal to the number expressed
using a binary representation."
This matches our generic definition with X = 896 and Y = 128. Then the block size is X+Y = 1024.
Here the word size is W = 64, so each block is parsed into 16 64-bit numbers.›
lemma SHA512parsing_h: "(64::nat) dvd (896 + 128)"
by force
global_interpretation SHA512_PadParse: SHA_PadParse 896 128 64
defines SHA512padding_k = "SHA512_PadParse.SHApadding_k"
and SHA512padded = "SHA512_PadParse.SHApadded"
and SHA512padded_len = "SHA512_PadParse.SHApadded_len"
and SHA512padded_numBlocks = "SHA512_PadParse.SHApadded_numBlocks"
and SHA512padded_asBits = "SHA512_PadParse.SHApadded_asBits"
and SHA512padded_numWords = "SHA512_PadParse.SHApadded_numWords"
and SHA512_PaddedParsed = "SHA512_PadParse.SHA_PaddedParsed"
and SHA512_inputValid = "SHA512_PadParse.SHA_inputValid"
by (simp add: SHA_PadParse_def SHA512parsing_h)
subsection ‹5.3 Setting the Initial Hash Value H^(0)›
text ‹Before hash computation begins for each of the secure hash algorithms, the initial hash
value, H(0), must be set. The size and number of words in H(0) depends on the message digest size.›
subsubsection ‹5.3.1 SHA-1›
definition SHA1_H0 :: "nat list" where
"SHA1_H0 = [0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0]"
lemma SHA1_H0_bnd1:
assumes "h ∈ set SHA1_H0"
shows "h < 2^32"
using assms unfolding SHA1_H0_def apply (cases h) by auto
lemma SHA1_H0_bnd2:
assumes "i < length SHA1_H0"
shows "SHA1_H0 ! i < 2^32"
using SHA1_H0_bnd1 assms nth_mem by blast
lemma SHA1_H0_valid: "word32s_valid SHA1_H0"
using SHA1_H0_bnd1 words_valid_def by blast
lemma SHA1_H0_len [simp]: "length SHA1_H0 = 5"
unfolding SHA1_H0_def by simp
subsubsection ‹5.3.2 SHA-224›
definition SHA224_H0 :: "nat list" where
"SHA224_H0 = [0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939,
0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4]"
lemma SHA224_H0_bnd1:
assumes "h ∈ set SHA224_H0"
shows "h < 2^32"
using assms unfolding SHA224_H0_def apply (cases h) by auto
lemma SHA224_H0_bnd2:
assumes "i < length SHA224_H0"
shows "SHA224_H0 ! i < 2^32"
using SHA224_H0_bnd1 assms nth_mem by blast
lemma SHA224_H0_valid: "word32s_valid SHA224_H0"
using SHA224_H0_bnd1 words_valid_def by blast
lemma SHA224_H0_len [simp]: "length SHA224_H0 = 8"
unfolding SHA224_H0_def by simp
subsubsection ‹5.3.3 SHA-256›
definition SHA256_H0 :: "nat list" where
"SHA256_H0 = [0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19]"
lemma SHA256_H0_bnd1:
assumes "h ∈ set SHA256_H0"
shows "h < 2^32"
using assms unfolding SHA256_H0_def apply (cases h) by auto
lemma SHA256_H0_bnd2:
assumes "i < length SHA256_H0"
shows "SHA256_H0 ! i < 2^32"
using SHA256_H0_bnd1 assms nth_mem by blast
lemma SHA256_H0_valid: "word32s_valid SHA256_H0"
using SHA256_H0_bnd1 words_valid_def by blast
lemma SHA256_H0_len [simp]: "length SHA256_H0 = 8"
unfolding SHA256_H0_def by simp
subsubsection ‹5.3.4 SHA-384›
definition SHA384_H0 :: "nat list" where
"SHA384_H0 = [0xcbbb9d5dc1059ed8, 0x629a292a367cd507, 0x9159015a3070dd17, 0x152fecd8f70e5939,
0x67332667ffc00b31, 0x8eb44a8768581511, 0xdb0c2e0d64f98fa7, 0x47b5481dbefa4fa4]"
lemma SHA384_H0_bnd1:
assumes "h ∈ set SHA384_H0"
shows "h < 2^64"
using assms unfolding SHA384_H0_def apply (cases h) by auto
lemma SHA384_H0_bnd2:
assumes "i < length SHA384_H0"
shows "SHA384_H0 ! i < 2^64"
using SHA384_H0_bnd1 assms nth_mem by blast
lemma SHA384_H0_valid: "word64s_valid SHA384_H0"
using SHA384_H0_bnd1 words_valid_def by blast
lemma SHA384_H0_len [simp]: "length SHA384_H0 = 8"
unfolding SHA384_H0_def by simp
subsubsection ‹5.3.5 SHA-512›
definition SHA512_H0 :: "nat list" where
"SHA512_H0 = [0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1,
0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179]"
lemma SHA512_H0_bnd1:
assumes "h ∈ set SHA512_H0"
shows "h < 2^64"
using assms unfolding SHA512_H0_def apply (cases h) by auto
lemma SHA512_H0_bnd2:
assumes "i < length SHA512_H0"
shows "SHA512_H0 ! i < 2^64"
using SHA512_H0_bnd1 assms nth_mem by blast
lemma SHA512_H0_valid: "word64s_valid SHA512_H0"
using SHA512_H0_bnd1 words_valid_def by blast
lemma SHA512_H0_len [simp]: "length SHA512_H0 = 8"
unfolding SHA512_H0_def by simp
subsubsection ‹5.3.6 SHA-512/t›
text ‹"``SHA-512/t'' is the general name for a t-bit hash function based on SHA-512 whose output is
truncated to t bits. Each hash function requires a distinct initial hash value. This section
provides a procedure for determining the initial value for SHA-512/t for a given value of t.
... SHA-512/224 (t = 224) and SHA-512/256 (t = 256) are approved hash algorithms. Other SHA-
512/t hash algorithms with different t values may be specified in [SP 800-107] in the future as
the need arises. Below are the IVs for SHA-512/224 and SHA-512/256."›
text ‹5.3.6.1 SHA-512/224›
definition SHA512_224_H0 :: "nat list" where
"SHA512_224_H0 =
[0x8C3D37C819544DA2, 0x73E1996689DCD4D6, 0x1DFAB7AE32FF9C82, 0x679DD514582F9FCF,
0x0F6D2B697BD44DA8, 0x77E36F7304C48942, 0x3F9D85A86A1D36C8, 0x1112E6AD91D692A1]"
lemma SHA512_224_H0_bnd1:
assumes "h ∈ set SHA512_224_H0"
shows "h < 2^64"
using assms unfolding SHA512_224_H0_def apply (cases h) by auto
lemma SHA512_224_H0_bnd2:
assumes "i < length SHA512_224_H0"
shows "SHA512_224_H0 ! i < 2^64"
using SHA512_224_H0_bnd1 assms nth_mem by blast
lemma SHA512_224_H0_valid: "word64s_valid SHA512_224_H0"
using SHA512_224_H0_bnd1 words_valid_def by blast
lemma SHA512_224_H0_len [simp]: "length SHA512_224_H0 = 8"
unfolding SHA512_224_H0_def by simp
text ‹5.3.6.2 SHA-512/256›
definition SHA512_256_H0 :: "nat list" where
"SHA512_256_H0 =
[0x22312194FC2BF72C, 0x9F555FA3C84C64C2, 0x2393B86B6F53B151, 0x963877195940EABD,
0x96283EE2A88EFFE3, 0xBE5E1E2553863992, 0x2B0199FC2C85B8AA, 0x0EB72DDC81C52CA2]"
lemma SHA512_256_H0_bnd1:
assumes "h ∈ set SHA512_256_H0"
shows "h < 2^64"
using assms unfolding SHA512_256_H0_def apply (cases h) by auto
lemma SHA512_256_H0_bnd2:
assumes "i < length SHA512_256_H0"
shows "SHA512_256_H0 ! i < 2^64"
using SHA512_256_H0_bnd1 assms nth_mem by blast
lemma SHA512_256_H0_valid: "word64s_valid SHA512_256_H0"
using SHA512_256_H0_bnd1 words_valid_def by blast
lemma SHA512_256_H0_len [simp]: "length SHA512_256_H0 = 8"
unfolding SHA512_256_H0_def by simp
section ‹6. Secure Hash Algorithms›
text ‹"In the following sections, the hash algorithms are not described in ascending order of size.
SHA-256 is described before SHA-224 because the specification for SHA-224 is identical to SHA-256,
except that different initial hash values are used, and the final hash value is truncated to 224
bits for SHA-224. The same is true for SHA-512, SHA-384, SHA-512/224 and SHA-512/256, except that
the final hash value is truncated to 224 bits for SHA-512/224, 256 bits for SHA-512/256 or
384 bits for SHA-384."
It is important to remember that in the standard, addition is always done modulo the pertinent
word size. So for SHA-1, they may write a + b and suppress the (mod 2^32).›
subsection ‹6.1 SHA-1›
subsubsection ‹Message Schedule›
definition SHA1_MessageSchedule_1 :: "words ⇒ words" where
"SHA1_MessageSchedule_1 W =
( let t = length W in
W @ [ROTL32 1 ((W ! (t-3)) XOR (W ! (t-8)) XOR (W ! (t-14)) XOR (W ! (t-16)))] )"
fun SHA1_MessageSchedule_rec :: "nat ⇒ words ⇒ words" where
"SHA1_MessageSchedule_rec n W =
( let t = length W in
if t < 16 then W else (
if n = 0 then W else
SHA1_MessageSchedule_rec (n-1) (SHA1_MessageSchedule_1 W) )
)"
lemma SHA1_MessageSchedule_1_len: "length (SHA1_MessageSchedule_1 W) = (length W) + 1"
by (metis SHA1_MessageSchedule_1_def Suc_eq_plus1 length_append_singleton)
lemma SHA1_MessageSchedule_1_valid:
assumes "word32s_valid W" "t = length W" "16 ≤ t"
shows "word32s_valid (SHA1_MessageSchedule_1 W)"
proof -
have 10: "W ! (t-3) ∈ set W"
by (metis assms(2,3) diff_less length_greater_0_conv list.size(3) not_le nth_mem
zero_less_numeral)
have 11: "W ! (t-3) < 2^32" using 10 assms(1) words_valid_def by blast
have 20: "W ! (t-8) ∈ set W"
by (metis assms(2,3) diff_less length_greater_0_conv list.size(3) not_le nth_mem
zero_less_numeral)
have 21: "W ! (t-8) < 2^32" using 20 assms(1) words_valid_def by blast
have 30: "W ! (t-14) ∈ set W"
by (metis assms(2,3) diff_less length_greater_0_conv list.size(3) not_le nth_mem
zero_less_numeral)
have 31: "W ! (t-14) < 2^32" using 30 assms(1) words_valid_def by blast
have 40: "W ! (t-16) ∈ set W"
by (metis assms(2,3) diff_less length_greater_0_conv list.size(3) not_le nth_mem
zero_less_numeral)
have 41: "W ! (t-16) < 2^32" using 40 assms(1) words_valid_def by blast
have 50: "(W ! (t-3)) XOR (W ! (t-8)) XOR (W ! (t-14)) XOR (W ! (t-16)) < 2^32"
using 11 21 31 41 nat_XOR_upper by presburger
have 51: "ROTL32 1 ((W ! (t-3)) XOR (W ! (t-8)) XOR (W ! (t-14)) XOR (W ! (t-16))) < 2^32"
by (meson 50 ROTL_bnd one_less_numeral_iff semiring_norm(76))
have 52: "word32s_valid
(W @ [ROTL32 1 ((W ! (t-3)) XOR (W ! (t-8)) XOR (W ! (t-14)) XOR (W ! (t-16)))])"
using assms(1) 51 words_valid_def words_valid_concat words_valid_cons words_valid_nil by blast
show ?thesis by (metis assms(2) 52 SHA1_MessageSchedule_1_def)
qed
lemma SHA1_MessageSchedule_rec_valid:
assumes "word32s_valid W"
shows "word32s_valid (SHA1_MessageSchedule_rec n W)"
proof (cases "length W < 16")
case True
then have "SHA1_MessageSchedule_rec n W = W" by simp
then show ?thesis using assms by simp
next
case F: False
then show ?thesis using assms proof (induction n arbitrary: W)
case 0
then have "SHA1_MessageSchedule_rec 0 W = W" by simp
then show ?case using 0(2) by simp
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA1_MessageSchedule_1 W"
have 1: "word32s_valid ?W1" by (metis C.prems(1,2) SHA1_MessageSchedule_1_valid leI)
have 2: "length ?W1 = ?t + 1" by (simp add: SHA1_MessageSchedule_1_len)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 4: "word32s_valid (SHA1_MessageSchedule_rec n ?W1)"
using 1 3 C.IH by blast
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA1_MessageSchedule_rec (Suc n) W = (SHA1_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA1_MessageSchedule_rec.simps)
show ?case using 4 6 by presburger
qed
qed
lemma SHA1_MessageSchedule_rec_len:
assumes "¬ length W < 16"
shows "length (SHA1_MessageSchedule_rec n W) = (length W) + n"
using assms proof (induction n arbitrary: W)
case 0
then have "SHA1_MessageSchedule_rec 0 W = W" by simp
then show ?case by presburger
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA1_MessageSchedule_1 W"
have 2: "length ?W1 = ?t + 1" by (simp add: SHA1_MessageSchedule_1_len)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA1_MessageSchedule_rec (Suc n) W = (SHA1_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA1_MessageSchedule_rec.simps)
show ?case using 2 3 6 C.IH by presburger
qed
definition SHA1_MessageSchedule :: "words ⇒ words" where
"SHA1_MessageSchedule MessageBlock = SHA1_MessageSchedule_rec (80-16) MessageBlock"
lemma SHA1_MessageSchedule_len:
assumes "length MessageBlock = 16"
shows "length (SHA1_MessageSchedule MessageBlock) = 80"
using SHA1_MessageSchedule_def SHA1_MessageSchedule_rec_len assms less_not_refl by presburger
lemma SHA1_MessageSchedule_valid:
assumes "word32s_valid MessageBlock"
shows "word32s_valid (SHA1_MessageSchedule MessageBlock)"
using SHA1_MessageSchedule_rec_valid SHA1_MessageSchedule_def assms by presburger
subsubsection ‹Round Function›
definition SHA1_RoundFunction :: "nat ⇒ words ⇒ nat ⇒ words" where
"SHA1_RoundFunction t ABCDE Wt =
(let a = ABCDE ! 0;
b = ABCDE ! 1;
c = ABCDE ! 2;
d = ABCDE ! 3;
e = ABCDE ! 4;
T = ((ROTL32 5 a) + (SHA1_ft t b c d) + e + (SHA1_Kt t) + Wt) mod (2^32)
in
[ T, a, ROTL32 30 b, c, d ] )"
text ‹We need to iterate over the round function for t=0 to 79. For the definition of this
recursive function, we start s at 80 and decrement in each loop, so t = 80 - s. The message
schedule W starts at length 80. We use the head of W in each round and drop it before starting
the next round. So when s=0, W = []. Could replace s with (length W).›
fun SHA1_RoundFunction_rec :: "nat ⇒ words ⇒ words ⇒ words" where
"SHA1_RoundFunction_rec 0 ABCDE W = ABCDE"
| "SHA1_RoundFunction_rec s ABCDE W =
SHA1_RoundFunction_rec (s-1) (SHA1_RoundFunction (80-s) ABCDE (hd W)) (drop 1 W)"
lemma SHA1_RoundFunction_Valid:
assumes "5 ≤ length ABCDE" "word32s_valid ABCDE"
shows "word32s_valid (SHA1_RoundFunction t ABCDE Wt)"
proof -
let ?a = "ABCDE ! 0"
let ?b = "ABCDE ! 1"
let ?c = "ABCDE ! 2"
let ?d = "ABCDE ! 3"
let ?e = "ABCDE ! 4"
have 0: "0 < length ABCDE ∧ 1 < length ABCDE ∧ 2 < length ABCDE ∧ 3 < length ABCDE ∧
4 < length ABCDE"
using assms(1) by linarith
have 1: "?a < 2^32 ∧ ?b < 2^32 ∧ ?c < 2^32 ∧ ?d < 2^32 ∧ ?e < 2^32"
using 0 assms(2) words_valid_ith by presburger
let ?T = "((ROTL32 5 ?a) + (SHA1_ft t ?b ?c ?d) + ?e + (SHA1_Kt t) + Wt) mod (2^32)"
have 2: "?T < 2^32" by force
have 3: "ROTL32 30 ?b < 2^32" by (meson 1 ROTL_bnd numeral_less_iff semiring_norm(76,78,81))
have 4: "word32s_valid [ ?T, ?a, ROTL32 30 ?b, ?c, ?d ]"
using 1 2 3 words_valid_def by auto
show ?thesis using 4 SHA1_RoundFunction_def by metis
qed
lemma SHA1_RoundFunction_len: "length (SHA1_RoundFunction t ABCDE Wt) = 5"
proof -
let ?a = "ABCDE ! 0"
let ?b = "ABCDE ! 1"
let ?c = "ABCDE ! 2"
let ?d = "ABCDE ! 3"
let ?e = "ABCDE ! 4"
let ?T = "((ROTL32 5 ?a) + (SHA1_ft t ?b ?c ?d) + ?e + (SHA1_Kt t) + Wt) mod (2^32)"
have 4: "length [ ?T, ?a, ROTL32 30 ?b, ?c, ?d ] = 5" by auto
show ?thesis using 4 SHA1_RoundFunction_def by metis
qed
lemma SHA1_RoundFunction_rec_Valid:
assumes "5 ≤ length ABCDE" "word32s_valid ABCDE"
shows "word32s_valid (SHA1_RoundFunction_rec s ABCDE W)"
using assms proof (induction s arbitrary: ABCDE W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA1_RoundFunction (80-(Suc s)) ABCDE (hd W))"
have X1: "length ?X = 5" using SHA1_RoundFunction_len by blast
have X2: "word32s_valid ?X" by (simp add: C.prems(1,2) SHA1_RoundFunction_Valid)
have X3: "5 ≤ length ?X" using X1 by simp
have "SHA1_RoundFunction_rec (Suc s) ABCDE W = SHA1_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X2 X3 by presburger
qed
lemma SHA1_RoundFunction_rec_len:
assumes "length ABCDE = 5"
shows "length (SHA1_RoundFunction_rec s ABCDE W) = 5"
using assms proof (induction s arbitrary: ABCDE W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA1_RoundFunction (80-(Suc s)) ABCDE (hd W))"
have X1: "length ?X = 5" using SHA1_RoundFunction_len by blast
have "SHA1_RoundFunction_rec (Suc s) ABCDE W = SHA1_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X1 by presburger
qed
subsubsection ‹SHA-1›
fun SHA1_rec :: "words ⇒ nat ⇒ words ⇒ words" where
"SHA1_rec LastHashValue 0 PaddedParsedM = LastHashValue"
| "SHA1_rec LastHashValue numBlocks PaddedParsedM =
( let MessageBlock = take 16 PaddedParsedM;
MessageSchedule = SHA1_MessageSchedule MessageBlock;
ABCDE = SHA1_RoundFunction_rec 80 LastHashValue MessageSchedule;
NewHashValue = map2 (λx y. (x+y) mod (2^32)) ABCDE LastHashValue
in
SHA1_rec NewHashValue (numBlocks-1) (drop 16 PaddedParsedM)
)"
definition SHA1 :: "nat ⇒ nat ⇒ nat" where
"SHA1 M l = (
let PaddedParsedM = SHA1_PaddedParsed M l;
numBlocks = SHA1padded_numBlocks l
in
word32s_to_nat (SHA1_rec SHA1_H0 numBlocks PaddedParsedM)
)"
lemma SHA1_rec_len:
assumes "length H = 5"
shows "length (SHA1_rec H n PPM) = 5"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA1_MessageSchedule ?MessageBlock"
let ?ABCDE = "SHA1_RoundFunction_rec 80 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^32)) ?ABCDE H"
have 1: "length ?ABCDE = 5" by (simp add: C.prems SHA1_RoundFunction_rec_len)
have 2: "length ?NewHashValue = 5" using C(2) 1 by simp
have 3: "SHA1_rec H (Suc n) PPM = SHA1_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 2 3 by presburger
qed
lemma SHA1_H0_rec_len: "length (SHA1_rec SHA1_H0 n PPM) = 5"
using SHA1_rec_len by simp
lemma SHA1_rec_valid:
assumes "word32s_valid H" "word32s_valid PPM" "length H = 5"
shows "word32s_valid (SHA1_rec H n PPM)"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA1_MessageSchedule ?MessageBlock"
let ?ABCDE = "SHA1_RoundFunction_rec 80 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^32)) ?ABCDE H"
have 1: "word32s_valid ?MessageBlock" using C(3) words_valid_take by blast
have 2: "word32s_valid ?MessageSchedule" using 1 SHA1_MessageSchedule_valid by fast
have 3: "length ?ABCDE = 5" using C(4) SHA1_RoundFunction_rec_len by fast
have 4: "length ?NewHashValue = 5" using C(4) 3 by simp
have 5: "word32s_valid ?NewHashValue" using words_valid_sum_mod by fast
have 6: "word32s_valid (drop 16 PPM)" using words_valid_drop C(3) by presburger
have 7: "SHA1_rec H (Suc n) PPM = SHA1_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 4 5 6 7 by presburger
qed
lemma SHA1_H0_rec_valid:
assumes "PPM = SHA1_PaddedParsed M l"
shows "word32s_valid (SHA1_rec SHA1_H0 n PPM)"
by (simp add: SHA1_H0_valid SHA1_rec_valid SHA1_PadParse.SHA_parsed_valid assms)
lemma SHA1_bnd: "SHA1 M l < 2^160"
proof -
let ?PPM = "SHA1_PaddedParsed M l"
let ?n = "SHA1padded_numBlocks l"
have 1: "word32s_valid (SHA1_rec SHA1_H0 ?n ?PPM)"
by (meson SHA1_H0_rec_valid)
have 2: "length (SHA1_rec SHA1_H0 ?n ?PPM) = 5"
using SHA1_H0_rec_len by presburger
have 3: "SHA1 M l = word32s_to_nat (SHA1_rec SHA1_H0 ?n ?PPM)"
by (meson SHA1_def)
have 4: "SHA1 M l < (2^32)^5"
by (metis 1 2 3 words_valid_def zero_less_numeral words_to_nat_len_bnd words_valid_def)
show ?thesis using 4 by simp
qed
subsection ‹6.2 SHA-256›
subsubsection ‹Message Schedule›
definition SHA256_MessageSchedule_1 :: "words ⇒ words" where
"SHA256_MessageSchedule_1 W =
( let t = length W in
W @
[(sigma256_1 (W ! (t-2)) + (W ! (t-7)) + sigma256_0 (W ! (t-15)) + (W ! (t-16))) mod 2^32])"
fun SHA256_MessageSchedule_rec :: "nat ⇒ words ⇒ words" where
"SHA256_MessageSchedule_rec n W =
( let t = length W in
if t < 16 then W else (
if n = 0 then W else
SHA256_MessageSchedule_rec (n-1) (SHA256_MessageSchedule_1 W) )
)"
lemma SHA256_MessageSchedule_1_valid:
assumes "word32s_valid W"
shows "word32s_valid (SHA256_MessageSchedule_1 W)"
by (metis SHA256_MessageSchedule_1_def assms mod_less_divisor words_valid_concat
words_valid_cons words_valid_nil zero_less_numeral zero_less_power)
lemma SHA256_MessageSchedule_rec_valid:
assumes "word32s_valid W"
shows "word32s_valid (SHA256_MessageSchedule_rec n W)"
proof (cases "length W < 16")
case True
then have "SHA256_MessageSchedule_rec n W = W" by simp
then show ?thesis using assms by simp
next
case F: False
then show ?thesis using assms proof (induction n arbitrary: W)
case 0
then have "SHA256_MessageSchedule_rec 0 W = W" by simp
then show ?case using 0(2) by simp
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA256_MessageSchedule_1 W"
have 1: "word32s_valid ?W1"
by (metis C(3) SHA256_MessageSchedule_1_valid)
have 2: "length ?W1 = ?t + 1"
by (metis SHA256_MessageSchedule_1_def Suc_eq_plus1 length_append_singleton)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 4: "word32s_valid (SHA256_MessageSchedule_rec n ?W1)"
using 1 3 C.IH by blast
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA256_MessageSchedule_rec (Suc n) W = (SHA256_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA256_MessageSchedule_rec.simps)
show ?case using 4 6 by presburger
qed
qed
lemma SHA256_MessageSchedule_rec_len:
assumes "¬ length W < 16"
shows "length (SHA256_MessageSchedule_rec n W) = (length W) + n"
using assms proof (induction n arbitrary: W)
case 0
then have "SHA256_MessageSchedule_rec 0 W = W" by simp
then show ?case by presburger
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA256_MessageSchedule_1 W"
have 2: "length ?W1 = ?t + 1"
by (metis SHA256_MessageSchedule_1_def Suc_eq_plus1 length_append_singleton)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA256_MessageSchedule_rec (Suc n) W = (SHA256_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA256_MessageSchedule_rec.simps[of "Suc n" W])
show ?case using 2 3 6 C.IH by presburger
qed
definition SHA256_MessageSchedule :: "words ⇒ words" where
"SHA256_MessageSchedule MessageBlock = SHA256_MessageSchedule_rec (64-16) MessageBlock"
lemma SHA256_MessageSchedule_len:
assumes "length MessageBlock = 16"
shows "length (SHA256_MessageSchedule MessageBlock) = 64"
using SHA256_MessageSchedule_def SHA256_MessageSchedule_rec_len assms less_not_refl by presburger
lemma SHA256_MessageSchedule_valid:
assumes "word32s_valid MessageBlock"
shows "word32s_valid (SHA256_MessageSchedule MessageBlock)"
using SHA256_MessageSchedule_rec_valid SHA256_MessageSchedule_def assms by presburger
subsubsection ‹Round Function›
definition SHA256_RoundFunction :: "nat ⇒ words ⇒ nat ⇒ words" where
"SHA256_RoundFunction t ABCDEFGH Wt =
(let a = ABCDEFGH ! 0;
b = ABCDEFGH ! 1;
c = ABCDEFGH ! 2;
d = ABCDEFGH ! 3;
e = ABCDEFGH ! 4;
f = ABCDEFGH ! 5;
g = ABCDEFGH ! 6;
h = ABCDEFGH ! 7;
T1 = (h + (Sigma256_1 e) + (Ch32 e f g) + (K256list ! t) + Wt) mod (2^32);
T2 = ((Sigma256_0 a) + (Maj a b c)) mod (2^32);
a' = (T1 + T2) mod (2^32);
e' = ( d + T1) mod (2^32)
in
[a', a, b, c, e', e, f, g] )"
fun SHA256_RoundFunction_rec :: "nat ⇒ words ⇒ words ⇒ words" where
"SHA256_RoundFunction_rec 0 ABCDEFGH W = ABCDEFGH"
| "SHA256_RoundFunction_rec s ABCDEFGH W =
SHA256_RoundFunction_rec (s-1) (SHA256_RoundFunction (64-s) ABCDEFGH (hd W)) (drop 1 W)"
lemma SHA256_RoundFunction_Valid:
assumes "8 ≤ length ABCDEFGH" "word32s_valid ABCDEFGH"
shows "word32s_valid (SHA256_RoundFunction t ABCDEFGH Wt)"
proof -
let ?a = "ABCDEFGH ! 0"
let ?b = "ABCDEFGH ! 1"
let ?c = "ABCDEFGH ! 2"
let ?d = "ABCDEFGH ! 3"
let ?e = "ABCDEFGH ! 4"
let ?f = "ABCDEFGH ! 5"
let ?g = "ABCDEFGH ! 6"
let ?h = "ABCDEFGH ! 7"
have 0: "0 < length ABCDEFGH ∧ 1 < length ABCDEFGH ∧ 2 < length ABCDEFGH ∧ 3 < length ABCDEFGH ∧
4 < length ABCDEFGH ∧ 5 < length ABCDEFGH ∧ 6 < length ABCDEFGH ∧ 7 < length ABCDEFGH"
using assms(1) by linarith
have 1: "?a < 2^32 ∧ ?b < 2^32 ∧ ?c < 2^32 ∧ ?d < 2^32 ∧
?e < 2^32 ∧ ?f < 2^32 ∧ ?g < 2^32 ∧ ?h < 2^32"
using 0 assms(2) words_valid_ith by presburger
let ?T1 = "(?h + (Sigma256_1 ?e) + (Ch32 ?e ?f ?g) + (K256list ! t) + Wt) mod (2^32)"
have 2: "?T1 < 2^32" by force
let ?T2 = "((Sigma256_0 ?a) + (Maj ?a ?b ?c)) mod (2^32)"
have 3: "?T2 < 2^32" by force
let ?a' = "(?T1 + ?T2) mod (2^32)"
have 4: "?a' < 2^32" by force
let ?e' = "(?d + ?T1) mod (2^32)"
have 5: "?e' < 2^32" by force
have 6: "word32s_valid [?a', ?a, ?b, ?c, ?e', ?e, ?f, ?g]"
using 1 2 3 4 5 words_valid_cons words_valid_nil by presburger
show ?thesis using 6 SHA256_RoundFunction_def by metis
qed
lemma SHA256_RoundFunction_len: "length (SHA256_RoundFunction t ABCDEFGH Wt) = 8"
proof -
let ?a = "ABCDEFGH ! 0"
let ?b = "ABCDEFGH ! 1"
let ?c = "ABCDEFGH ! 2"
let ?d = "ABCDEFGH ! 3"
let ?e = "ABCDEFGH ! 4"
let ?f = "ABCDEFGH ! 5"
let ?g = "ABCDEFGH ! 6"
let ?h = "ABCDEFGH ! 7"
let ?T1 = "(?h + (Sigma256_1 ?e) + (Ch32 ?e ?f ?g) + (K256list ! t) + Wt) mod (2^32)"
let ?T2 = "((Sigma256_0 ?a) + (Maj ?a ?b ?c)) mod (2^32)"
let ?a' = "(?T1 + ?T2) mod (2^32)"
let ?e' = " (?d + ?T1) mod (2^32)"
have "length [?a', ?a, ?b, ?c, ?e', ?e, ?f, ?g] = 8" by force
then show ?thesis using SHA256_RoundFunction_def by metis
qed
lemma SHA256_RoundFunction_rec_Valid:
assumes "8 ≤ length ABCDEFGH" "word32s_valid ABCDEFGH"
shows "word32s_valid (SHA256_RoundFunction_rec s ABCDEFGH W)"
using assms proof (induction s arbitrary: ABCDEFGH W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA256_RoundFunction (64-(Suc s)) ABCDEFGH (hd W))"
have X1: "length ?X = 8" using SHA256_RoundFunction_len by blast
have X2: "word32s_valid ?X" by (simp add: C.prems(1,2) SHA256_RoundFunction_Valid)
have X3: "8 ≤ length ?X" using X1 by simp
have "SHA256_RoundFunction_rec (Suc s) ABCDEFGH W = SHA256_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X2 X3 by presburger
qed
lemma SHA256_RoundFunction_rec_len:
assumes "length ABCDEFGH = 8"
shows "length (SHA256_RoundFunction_rec s ABCDEFGH W) = 8"
using assms proof (induction s arbitrary: ABCDEFGH W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA256_RoundFunction (64-(Suc s)) ABCDEFGH (hd W))"
have X1: "length ?X = 8" using SHA256_RoundFunction_len by blast
have "SHA256_RoundFunction_rec (Suc s) ABCDEFGH W = SHA256_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X1 by presburger
qed
subsubsection ‹SHA-256›
fun SHA256_rec :: "words ⇒ nat ⇒ words ⇒ words" where
"SHA256_rec LastHashValue 0 PaddedParsedM = LastHashValue"
| "SHA256_rec LastHashValue numBlocks PaddedParsedM =
( let MessageBlock = take 16 PaddedParsedM;
MessageSchedule = SHA256_MessageSchedule MessageBlock;
ABCDEFGH = SHA256_RoundFunction_rec 64 LastHashValue MessageSchedule;
NewHashValue = map2 (λx y. (x+y) mod (2^32)) ABCDEFGH LastHashValue
in
SHA256_rec NewHashValue (numBlocks-1) (drop 16 PaddedParsedM)
)"
definition SHA256 :: "nat ⇒ nat ⇒ nat" where
"SHA256 M l = (
let PaddedParsedM = SHA1_PaddedParsed M l;
numBlocks = SHA1padded_numBlocks l
in
word32s_to_nat (SHA256_rec SHA256_H0 numBlocks PaddedParsedM)
)"
text ‹SHA-1, -256, and -224 all allow messages up to length 2^64.›
abbreviation SHA256_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA256_inputValid M l ≡ SHA1_inputValid M l"
lemma SHA256_rec_len:
assumes "length H = 8"
shows "length (SHA256_rec H n PPM) = 8"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA256_MessageSchedule ?MessageBlock"
let ?ABCDEFGH = "SHA256_RoundFunction_rec 64 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^32)) ?ABCDEFGH H"
have 1: "length ?ABCDEFGH = 8" by (simp add: C.prems SHA256_RoundFunction_rec_len)
have 2: "length ?NewHashValue = 8" using C(2) 1 by simp
have 3: "SHA256_rec H (Suc n) PPM = SHA256_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 2 3 by presburger
qed
lemma SHA256_H0_rec_len: "length (SHA256_rec SHA256_H0 n PPM) = 8"
using SHA256_rec_len by simp
lemma SHA256_rec_valid:
assumes "word32s_valid H" "word32s_valid PPM" "length H = 8"
shows "word32s_valid (SHA256_rec H n PPM)"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA256_MessageSchedule ?MessageBlock"
let ?ABCDEFGH = "SHA256_RoundFunction_rec 64 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^32)) ?ABCDEFGH H"
have 1: "word32s_valid ?MessageBlock" using C(3) words_valid_take by blast
have 2: "word32s_valid ?MessageSchedule" using 1 SHA256_MessageSchedule_valid by fast
have 3: "length ?ABCDEFGH = 8" using C(4) SHA256_RoundFunction_rec_len by fast
have 4: "length ?NewHashValue = 8" using C(4) 3 by simp
have 5: "word32s_valid ?NewHashValue" using words_valid_sum_mod by fast
have 6: "word32s_valid (drop 16 PPM)" using words_valid_drop C(3) by presburger
have 7: "SHA256_rec H (Suc n) PPM = SHA256_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 4 5 6 7 by presburger
qed
lemma SHA256_H0_rec_valid:
assumes "PPM = SHA1_PaddedParsed M l"
shows "word32s_valid (SHA256_rec SHA256_H0 n PPM)"
by (simp add: SHA1_PadParse.SHA_parsed_valid SHA256_H0_valid SHA256_rec_valid assms)
lemma SHA256_bnd: "SHA256 M l < 2^256"
proof -
let ?PPM = "SHA1_PaddedParsed M l"
let ?n = "SHA1padded_numBlocks l"
have 1: "word32s_valid (SHA256_rec SHA256_H0 ?n ?PPM)"
by (meson SHA256_H0_rec_valid)
have 2: "length (SHA256_rec SHA256_H0 ?n ?PPM) = 8"
using SHA256_H0_rec_len by presburger
have 3: "SHA256 M l = word32s_to_nat (SHA256_rec SHA256_H0 ?n ?PPM)"
by (meson SHA256_def)
have 4: "SHA256 M l < (2^32)^8"
by (metis 1 2 3 words_valid_def zero_less_numeral words_to_nat_len_bnd words_valid_def)
show ?thesis using 4 by simp
qed
subsection ‹6.3 SHA-224›
definition SHA224 :: "nat ⇒ nat ⇒ nat" where
"SHA224 M l = (
let PaddedParsedM = SHA1_PaddedParsed M l;
numBlocks = SHA1padded_numBlocks l;
H256 = SHA256_rec SHA224_H0 numBlocks PaddedParsedM
in
word32s_to_nat (butlast H256)
)"
text ‹SHA-1, -256, and -224 all allow messages up to length 2^64.›
abbreviation SHA224_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA224_inputValid M l ≡ SHA1_inputValid M l"
lemma SHA224_H0_rec_len: "length (SHA256_rec SHA224_H0 n PPM) = 8"
using SHA256_rec_len by simp
lemma SHA224_H0_rec_valid:
assumes "PPM = SHA1_PaddedParsed M l"
shows "word32s_valid (SHA256_rec SHA224_H0 n PPM)"
by (simp add: SHA1_PadParse.SHA_parsed_valid SHA224_H0_valid SHA256_rec_valid assms)
lemma SHA224_bnd: "SHA224 M l < 2^224"
proof -
let ?PPM = "SHA1_PaddedParsed M l"
let ?n = "SHA1padded_numBlocks l"
let ?H256 = "SHA256_rec SHA224_H0 ?n ?PPM"
have 1: "word32s_valid ?H256"
by (meson SHA224_H0_rec_valid)
have 2: "length ?H256 = 8"
using SHA224_H0_rec_len by presburger
have 3: "SHA224 M l = word32s_to_nat (butlast ?H256)"
by (meson SHA224_def)
have 4: "length (butlast ?H256) = 7" using 2 by simp
have 5: "word32s_valid (butlast ?H256)" using 1 words_valid_butlast by fast
have 6: "SHA224 M l < (2^32)^7"
by (metis 3 4 5 words_to_nat_len_bnd words_valid_def zero_less_numeral)
show ?thesis using 6 by simp
qed
subsection ‹6.4 SHA-512›
subsubsection ‹Message Schedule›
definition SHA512_MessageSchedule_1 :: "words ⇒ words" where
"SHA512_MessageSchedule_1 W =
( let t = length W in
W @
[(sigma512_1 (W ! (t-2)) + (W ! (t-7)) + sigma512_0 (W ! (t-15)) + (W ! (t-16))) mod 2^64] )"
fun SHA512_MessageSchedule_rec :: "nat ⇒ words ⇒ words" where
"SHA512_MessageSchedule_rec n W =
( let t = length W in
if t < 16 then W else (
if n = 0 then W else
SHA512_MessageSchedule_rec (n-1) (SHA512_MessageSchedule_1 W) )
)"
lemma SHA512_MessageSchedule_1_valid:
assumes "word64s_valid W"
shows "word64s_valid (SHA512_MessageSchedule_1 W)"
by (metis SHA512_MessageSchedule_1_def assms mod_less_divisor words_valid_concat
words_valid_cons words_valid_nil zero_less_numeral zero_less_power)
lemma SHA512_MessageSchedule_rec_valid:
assumes "word64s_valid W"
shows "word64s_valid (SHA512_MessageSchedule_rec n W)"
proof (cases "length W < 16")
case True
then have "SHA512_MessageSchedule_rec n W = W" by simp
then show ?thesis using assms by simp
next
case F: False
then show ?thesis using assms proof (induction n arbitrary: W)
case 0
then have "SHA512_MessageSchedule_rec 0 W = W" by simp
then show ?case using 0(2) by simp
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA512_MessageSchedule_1 W"
have 1: "word64s_valid ?W1"
by (metis C(3) SHA512_MessageSchedule_1_valid)
have 2: "length ?W1 = ?t + 1"
by (metis SHA512_MessageSchedule_1_def Suc_eq_plus1 length_append_singleton)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 4: "word64s_valid (SHA512_MessageSchedule_rec n ?W1)"
using 1 3 C.IH by blast
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA512_MessageSchedule_rec (Suc n) W = (SHA512_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA512_MessageSchedule_rec.simps)
show ?case using 4 6 by presburger
qed
qed
lemma SHA512_MessageSchedule_rec_len:
assumes "¬ length W < 16"
shows "length (SHA512_MessageSchedule_rec n W) = (length W) + n"
using assms proof (induction n arbitrary: W)
case 0
then have "SHA512_MessageSchedule_rec 0 W = W" by simp
then show ?case by presburger
next
case C: (Suc n)
have 0: "¬ 0 = Suc n" by simp
let ?t = "length W"
let ?W1 = "SHA512_MessageSchedule_1 W"
have 2: "length ?W1 = ?t + 1"
by (metis SHA512_MessageSchedule_1_def Suc_eq_plus1 length_append_singleton)
have 3: "¬ length ?W1 < 16" by (metis 2 C.prems(1) add_lessD1)
have 5: "(Suc n) - 1 = n" by simp
have 6: "SHA512_MessageSchedule_rec (Suc n) W = (SHA512_MessageSchedule_rec n ?W1)"
by (metis C(2) 0 5 SHA512_MessageSchedule_rec.simps[of "Suc n" W])
show ?case using 2 3 6 C.IH by presburger
qed
definition SHA512_MessageSchedule :: "words ⇒ words" where
"SHA512_MessageSchedule MessageBlock = SHA512_MessageSchedule_rec (80-16) MessageBlock"
lemma SHA512_MessageSchedule_len:
assumes "length MessageBlock = 16"
shows "length (SHA512_MessageSchedule MessageBlock) = 80"
using SHA512_MessageSchedule_def SHA512_MessageSchedule_rec_len assms less_not_refl by presburger
lemma SHA512_MessageSchedule_valid:
assumes "word64s_valid MessageBlock"
shows "word64s_valid (SHA512_MessageSchedule MessageBlock)"
using SHA512_MessageSchedule_rec_valid SHA512_MessageSchedule_def assms by presburger
subsubsection ‹Round Function›
definition SHA512_RoundFunction :: "nat ⇒ words ⇒ nat ⇒ words" where
"SHA512_RoundFunction t ABCDEFGH Wt =
(let a = ABCDEFGH ! 0;
b = ABCDEFGH ! 1;
c = ABCDEFGH ! 2;
d = ABCDEFGH ! 3;
e = ABCDEFGH ! 4;
f = ABCDEFGH ! 5;
g = ABCDEFGH ! 6;
h = ABCDEFGH ! 7;
T1 = (h + (Sigma512_1 e) + (Ch64 e f g) + (K512list ! t) + Wt) mod (2^64);
T2 = ((Sigma512_0 a) + (Maj a b c)) mod (2^64);
a' = (T1 + T2) mod (2^64);
e' = ( d + T1) mod (2^64)
in
[a', a, b, c, e', e, f, g] )"
fun SHA512_RoundFunction_rec :: "nat ⇒ words ⇒ words ⇒ words" where
"SHA512_RoundFunction_rec 0 ABCDEFGH W = ABCDEFGH"
| "SHA512_RoundFunction_rec s ABCDEFGH W =
SHA512_RoundFunction_rec (s-1) (SHA512_RoundFunction (80-s) ABCDEFGH (hd W)) (drop 1 W)"
lemma SHA512_RoundFunction_Valid:
assumes "8 ≤ length ABCDEFGH" "word64s_valid ABCDEFGH"
shows "word64s_valid (SHA512_RoundFunction t ABCDEFGH Wt)"
proof -
let ?a = "ABCDEFGH ! 0"
let ?b = "ABCDEFGH ! 1"
let ?c = "ABCDEFGH ! 2"
let ?d = "ABCDEFGH ! 3"
let ?e = "ABCDEFGH ! 4"
let ?f = "ABCDEFGH ! 5"
let ?g = "ABCDEFGH ! 6"
let ?h = "ABCDEFGH ! 7"
have 0: "0 < length ABCDEFGH ∧ 1 < length ABCDEFGH ∧ 2 < length ABCDEFGH ∧ 3 < length ABCDEFGH ∧
4 < length ABCDEFGH ∧ 5 < length ABCDEFGH ∧ 6 < length ABCDEFGH ∧ 7 < length ABCDEFGH"
using assms(1) by linarith
have 1: "?a < 2^64 ∧ ?b < 2^64 ∧ ?c < 2^64 ∧ ?d < 2^64 ∧
?e < 2^64 ∧ ?f < 2^64 ∧ ?g < 2^64 ∧ ?h < 2^64"
using 0 assms(2) words_valid_ith by presburger
let ?T1 = "(?h + (Sigma512_1 ?e) + (Ch64 ?e ?f ?g) + (K512list ! t) + Wt) mod (2^64)"
have 2: "?T1 < 2^64" by force
let ?T2 = "((Sigma512_0 ?a) + (Maj ?a ?b ?c)) mod (2^64)"
have 3: "?T2 < 2^64" by force
let ?a' = "(?T1 + ?T2) mod (2^64)"
have 4: "?a' < 2^64" by force
let ?e' = "(?d + ?T1) mod (2^64)"
have 5: "?e' < 2^64" by force
have 6: "word64s_valid [?a', ?a, ?b, ?c, ?e', ?e, ?f, ?g]"
using 1 2 3 4 5 words_valid_cons words_valid_nil by presburger
show ?thesis using 6 SHA512_RoundFunction_def by metis
qed
lemma SHA512_RoundFunction_len: "length (SHA512_RoundFunction t ABCDEFGH Wt) = 8"
proof -
let ?a = "ABCDEFGH ! 0"
let ?b = "ABCDEFGH ! 1"
let ?c = "ABCDEFGH ! 2"
let ?d = "ABCDEFGH ! 3"
let ?e = "ABCDEFGH ! 4"
let ?f = "ABCDEFGH ! 5"
let ?g = "ABCDEFGH ! 6"
let ?h = "ABCDEFGH ! 7"
let ?T1 = "(?h + (Sigma512_1 ?e) + (Ch64 ?e ?f ?g) + (K512list ! t) + Wt) mod (2^64)"
let ?T2 = "((Sigma512_0 ?a) + (Maj ?a ?b ?c)) mod (2^64)"
let ?a' = "(?T1 + ?T2) mod (2^64)"
let ?e' = "(?d + ?T1) mod (2^64)"
have "length [?a', ?a, ?b, ?c, ?e', ?e, ?f, ?g] = 8" by force
then show ?thesis using SHA512_RoundFunction_def by metis
qed
lemma SHA512_RoundFunction_rec_Valid:
assumes "8 ≤ length ABCDEFGH" "word64s_valid ABCDEFGH"
shows "word64s_valid (SHA512_RoundFunction_rec s ABCDEFGH W)"
using assms proof (induction s arbitrary: ABCDEFGH W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA512_RoundFunction (80-(Suc s)) ABCDEFGH (hd W))"
have X1: "length ?X = 8" using SHA512_RoundFunction_len by blast
have X2: "word64s_valid ?X" by (simp add: C.prems(1,2) SHA512_RoundFunction_Valid)
have X3: "8 ≤ length ?X" using X1 by simp
have "SHA512_RoundFunction_rec (Suc s) ABCDEFGH W = SHA512_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X2 X3 by presburger
qed
lemma SHA512_RoundFunction_rec_len:
assumes "length ABCDEFGH = 8"
shows "length (SHA512_RoundFunction_rec s ABCDEFGH W) = 8"
using assms proof (induction s arbitrary: ABCDEFGH W)
case 0
then show ?case by simp
next
case C: (Suc s)
let ?d1W = "drop 1 W"
let ?X = "(SHA512_RoundFunction (80-(Suc s)) ABCDEFGH (hd W))"
have X1: "length ?X = 8" using SHA512_RoundFunction_len by blast
have "SHA512_RoundFunction_rec (Suc s) ABCDEFGH W = SHA512_RoundFunction_rec s ?X ?d1W" by simp
then show ?case using C.IH X1 by presburger
qed
subsubsection ‹SHA-512›
fun SHA512_rec :: "words ⇒ nat ⇒ words ⇒ words" where
"SHA512_rec LastHashValue 0 PaddedParsedM = LastHashValue"
| "SHA512_rec LastHashValue numBlocks PaddedParsedM =
( let MessageBlock = take 16 PaddedParsedM;
MessageSchedule = SHA512_MessageSchedule MessageBlock;
ABCDEFGH = SHA512_RoundFunction_rec 80 LastHashValue MessageSchedule;
NewHashValue = map2 (λx y. (x+y) mod (2^64)) ABCDEFGH LastHashValue
in
SHA512_rec NewHashValue (numBlocks-1) (drop 16 PaddedParsedM)
)"
definition SHA512 :: "nat ⇒ nat ⇒ nat" where
"SHA512 M l = (
let PaddedParsedM = SHA512_PaddedParsed M l;
numBlocks = SHA512padded_numBlocks l
in
word64s_to_nat (SHA512_rec SHA512_H0 numBlocks PaddedParsedM)
)"
lemma SHA512_rec_len:
assumes "length H = 8"
shows "length (SHA512_rec H n PPM) = 8"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA512_MessageSchedule ?MessageBlock"
let ?ABCDEFGH = "SHA512_RoundFunction_rec 80 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^64)) ?ABCDEFGH H"
have 1: "length ?ABCDEFGH = 8" by (simp add: C.prems SHA512_RoundFunction_rec_len)
have 2: "length ?NewHashValue = 8" using C(2) 1 by simp
have 3: "SHA512_rec H (Suc n) PPM = SHA512_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 2 3 by presburger
qed
lemma SHA512_H0_rec_len: "length (SHA512_rec SHA512_H0 n PPM) = 8"
using SHA512_rec_len by simp
lemma SHA512_rec_valid:
assumes "word64s_valid H" "word64s_valid PPM" "length H = 8"
shows "word64s_valid (SHA512_rec H n PPM)"
using assms proof (induction n arbitrary: H PPM)
case 0
then show ?case by simp
next
case C: (Suc n)
let ?MessageBlock = "take 16 PPM"
let ?MessageSchedule = "SHA512_MessageSchedule ?MessageBlock"
let ?ABCDEFGH = "SHA512_RoundFunction_rec 80 H ?MessageSchedule"
let ?NewHashValue = "map2 (λx y. (x+y) mod (2^64)) ?ABCDEFGH H"
have 1: "word64s_valid ?MessageBlock" using C(3) words_valid_take by blast
have 2: "word64s_valid ?MessageSchedule" using 1 SHA512_MessageSchedule_valid by fast
have 3: "length ?ABCDEFGH = 8" using C(4) SHA512_RoundFunction_rec_len by fast
have 4: "length ?NewHashValue = 8" using C(4) 3 by simp
have 5: "word64s_valid ?NewHashValue" using words_valid_sum_mod by fast
have 6: "word64s_valid (drop 16 PPM)" using words_valid_drop C(3) by presburger
have 7: "SHA512_rec H (Suc n) PPM = SHA512_rec ?NewHashValue n (drop 16 PPM)" by force
show ?case using C(1) 4 5 6 7 by presburger
qed
lemma SHA512_H0_rec_valid:
assumes "PPM = SHA512_PaddedParsed M l"
shows "word64s_valid (SHA512_rec SHA512_H0 n PPM)"
by (simp add: SHA512_PadParse.SHA_parsed_valid SHA512_H0_valid SHA512_rec_valid assms)
lemma SHA512_bnd: "SHA512 M l < 2^512"
proof -
let ?PPM = "SHA512_PaddedParsed M l"
let ?n = "SHA512padded_numBlocks l"
have 1: "word64s_valid (SHA512_rec SHA512_H0 ?n ?PPM)"
by (meson SHA512_H0_rec_valid)
have 2: "length (SHA512_rec SHA512_H0 ?n ?PPM) = 8"
using SHA512_H0_rec_len by presburger
have 3: "SHA512 M l = word64s_to_nat (SHA512_rec SHA512_H0 ?n ?PPM)"
by (meson SHA512_def)
have 4: "SHA512 M l < (2^64)^8"
by (metis 1 2 3 words_valid_def words_to_nat_len_bnd zero_less_numeral)
show ?thesis using 4 by simp
qed
subsection ‹6.5 SHA-384›
definition SHA384 :: "nat ⇒ nat ⇒ nat" where
"SHA384 M l = (
let PaddedParsedM = SHA512_PaddedParsed M l;
numBlocks = SHA512padded_numBlocks l;
H512 = SHA512_rec SHA384_H0 numBlocks PaddedParsedM
in
word64s_to_nat (take 6 H512)
)"
text ‹SHA-512, -384, and -512/t all allow messages up to length 2^128.›
abbreviation SHA384_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA384_inputValid M l ≡ SHA512_inputValid M l"
lemma SHA384_H0_rec_len: "length (SHA512_rec SHA384_H0 n PPM) = 8"
using SHA512_rec_len by simp
lemma SHA384_H0_rec_valid:
assumes "PPM = SHA512_PaddedParsed M l"
shows "word64s_valid (SHA512_rec SHA384_H0 n PPM)"
by (simp add: SHA512_PadParse.SHA_parsed_valid SHA384_H0_valid SHA512_rec_valid assms)
lemma SHA384_bnd: "SHA384 M l < 2^384"
proof -
let ?PPM = "SHA512_PaddedParsed M l"
let ?n = "SHA512padded_numBlocks l"
let ?H512 = "SHA512_rec SHA384_H0 ?n ?PPM"
have 1: "word64s_valid ?H512" by (meson SHA384_H0_rec_valid)
have 10: "word64s_valid (take 6 ?H512)" using 1 words_valid_take by blast
have 2: "length (?H512) = 8" using SHA384_H0_rec_len by presburger
have 20: "length (take 6 ?H512) = 6" using 2 by simp
have 3: "SHA384 M l = word64s_to_nat (take 6 ?H512)" by (meson SHA384_def)
have 4: "SHA384 M l < (2^64)^6"
by (metis 10 20 3 SHA512_PadParse.XYWpos(3) words_to_nat_len_bnd words_valid_def)
show ?thesis using 4 by simp
qed
subsection ‹6.6 SHA-512/224›
definition SHA512_224 :: "nat ⇒ nat ⇒ nat" where
"SHA512_224 M l = (
let PaddedParsedM = SHA512_PaddedParsed M l;
numBlocks = SHA512padded_numBlocks l;
H512 = word64s_to_nat (SHA512_rec SHA512_224_H0 numBlocks PaddedParsedM)
in
H512 div 2^288
)"
text ‹SHA-512, -384, and -512/t all allow messages up to length 2^128.›
abbreviation SHA512_224_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA512_224_inputValid M l ≡ SHA512_inputValid M l"
lemma SHA512_224_H0_rec_len: "length (SHA512_rec SHA512_224_H0 n PPM) = 8"
using SHA512_rec_len by simp
lemma SHA512_224_H0_rec_valid:
assumes "PPM = SHA512_PaddedParsed M l"
shows "word64s_valid (SHA512_rec SHA512_224_H0 n PPM)"
by (simp add: SHA512_PadParse.SHA_parsed_valid SHA512_224_H0_valid SHA512_rec_valid assms)
lemma SHA512_224_bnd: "SHA512_224 M l < 2^224"
proof -
let ?PPM = "SHA512_PaddedParsed M l"
let ?n = "SHA512padded_numBlocks l"
let ?H512 = "SHA512_rec SHA512_224_H0 ?n ?PPM"
let ?H512_nat = "word64s_to_nat ?H512"
have 1: "word64s_valid ?H512" by (meson SHA512_224_H0_rec_valid)
have 2: "length (?H512) = 8" using SHA512_224_H0_rec_len by presburger
have 3: "?H512_nat < (2^64)^8"
by (metis 1 2 SHA512_PadParse.XYWpos(3) words_to_nat_len_bnd words_valid_def)
have 4: "?H512_nat < 2^512" using 3 by simp
show ?thesis using 4 SHA512_224_def by simp
qed
subsection ‹6.6 SHA-512/256›
definition SHA512_256 :: "nat ⇒ nat ⇒ nat" where
"SHA512_256 M l = (
let PaddedParsedM = SHA512_PaddedParsed M l;
numBlocks = SHA512padded_numBlocks l;
H512 = word64s_to_nat (SHA512_rec SHA512_256_H0 numBlocks PaddedParsedM)
in
H512 div 2^256
)"
text ‹SHA-512, -384, and -512/t all allow messages up to length 2^128.›
abbreviation SHA512_256_inputValid :: "nat ⇒ nat ⇒ bool" where
"SHA512_256_inputValid M l ≡ SHA512_inputValid M l"
lemma SHA512_256_H0_rec_len: "length (SHA512_rec SHA512_256_H0 n PPM) = 8"
using SHA512_rec_len by simp
lemma SHA512_256_H0_rec_valid:
assumes "PPM = SHA512_PaddedParsed M l"
shows "word64s_valid (SHA512_rec SHA512_256_H0 n PPM)"
by (simp add: SHA512_PadParse.SHA_parsed_valid SHA512_256_H0_valid SHA512_rec_valid assms)
lemma SHA512_256_bnd: "SHA512_256 M l < 2^256"
proof -
let ?PPM = "SHA512_PaddedParsed M l"
let ?n = "SHA512padded_numBlocks l"
let ?H512 = "SHA512_rec SHA512_256_H0 ?n ?PPM"
let ?H512_nat = "word64s_to_nat ?H512"
have 1: "word64s_valid ?H512" by (meson SHA512_256_H0_rec_valid)
have 2: "length (?H512) = 8" using SHA512_256_H0_rec_len by presburger
have 3: "?H512_nat < (2^64)^8"
by (metis 1 2 SHA512_PadParse.XYWpos(3) words_to_nat_len_bnd words_valid_def)
have 4: "?H512_nat < 2^512" using 3 by simp
show ?thesis using 4 SHA512_256_def by simp
qed
section ‹Octets›
text ‹We have translated the Secure Hash Standard so that each of the Secure Hash Algorithms is
a function from natural numbers to natural numbers. This allows us the flexibility to apply
the SHA definition to any implementation, whether that implementation acts on natural numbers, bit
strings, octet (i.e., byte) strings, or (generically) n-bit word strings. (Words.thy contains all
the conversion functions needed between natural numbers and n-bit words with abbreviations for
conversions to and from bit strings, octet strings, 32-bit word strings, and 64-bit word strings.)
Some NIST standards rely on an underlying hash function and they assume that that hash function
takes as input a string of 8-bit values, that is octets, and produces a string of octets. So here
we provide the "octet version" of each of the secure hash algorithms above. For each of these,
we prove the basic things that one would like to know: that the output octet string is valid
(meaning each octet is < 256) and that we know how many octets is output by each of the
hash algorithms.
Note that these functions assume that the message length (in bits) is exactly 8 times the number
of input octets. For a particular implementation, you will need to decide if a message bit-length
must be 0 mod 8. If not, you may need to provide a message length as an additional input and
deal with right- or left-alignment of the message within the words. The following as a guide,
along with the conversions available in Words.thy, you can easily form any wrapper you may need
to apply to the above nat-to-nat SHA functions defined above.›
subsection ‹SHA-1›
definition SHA1octets :: "octets ⇒ octets" where
"SHA1octets os = nat_to_octets_len (SHA1 (octets_to_nat os) (8*(length os))) 20"
definition SHA1_hLen :: nat where
"SHA1_hLen = 20"
lemma SHA1octets_len: "length (SHA1octets os) = 20"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA1 ?M ?l < 2^160" using SHA1_bnd by blast
have 2: "(160::nat) = 8*20" by force
have 3: "SHA1 ?M ?l < (2^8)^20" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA1 ?M ?l) 20 ) = 20"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA1octets_def by presburger
qed
lemma SHA1octets_len2: "∀x. length (SHA1octets x) = 20"
using SHA1octets_len by blast
lemma SHA1octets_valid: "octets_valid (SHA1octets os)"
using nat_to_words_len_valid SHA1octets_def by presburger
lemma SHA1octets_valid2: "∀x. octets_valid (SHA1octets x)"
using SHA1octets_valid by satx
subsection ‹SHA-224›
definition SHA224octets :: "octets ⇒ octets" where
"SHA224octets os = nat_to_octets_len (SHA224 (octets_to_nat os) (8*(length os))) 28"
definition SHA224_hLen :: nat where
"SHA224_hLen = 28"
lemma SHA224octets_len: "length (SHA224octets os) = 28"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA224 ?M ?l < 2^224" using SHA224_bnd by blast
have 2: "(224::nat) = 8*28" by force
have 3: "SHA224 ?M ?l < (2^8)^28" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA224 ?M ?l) 28 ) = 28"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA224octets_def by presburger
qed
lemma SHA224octets_len2: "∀x. length (SHA224octets x) = 28"
using SHA224octets_len by blast
lemma SHA224octets_valid: "octets_valid (SHA224octets os)"
using nat_to_words_len_valid SHA224octets_def by presburger
lemma SHA224octets_valid2: "∀x. octets_valid (SHA224octets x)"
using SHA224octets_valid by satx
subsection ‹SHA-256›
definition SHA256octets :: "octets ⇒ octets" where
"SHA256octets os = nat_to_octets_len (SHA256 (octets_to_nat os) (8*(length os))) 32"
definition SHA256_hLen :: nat where
"SHA256_hLen = 32"
lemma SHA256octets_len: "length (SHA256octets os) = 32"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA256 ?M ?l < 2^256" using SHA256_bnd by blast
have 2: "(256::nat) = 8*32" by force
have 3: "SHA256 ?M ?l < (2^8)^32" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA256 ?M ?l) 32 ) = 32"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA256octets_def by presburger
qed
lemma SHA256octets_len2: "∀x. length (SHA256octets x) = 32"
using SHA256octets_len by blast
lemma SHA256octets_valid: "octets_valid (SHA256octets os)"
using nat_to_words_len_valid SHA256octets_def by presburger
lemma SHA256octets_valid2: "∀x. octets_valid (SHA256octets x)"
using SHA256octets_valid by satx
subsection ‹SHA-384›
definition SHA384octets :: "octets ⇒ octets" where
"SHA384octets os = nat_to_octets_len (SHA384 (octets_to_nat os) (8*(length os))) 48"
definition SHA384_hLen :: nat where
"SHA384_hLen = 48"
lemma SHA384octets_len: "length (SHA384octets os) = 48"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA384 ?M ?l < 2^384" using SHA384_bnd by blast
have 2: "(384::nat) = 8*48" by force
have 3: "SHA384 ?M ?l < (2^8)^48" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA384 ?M ?l) 48 ) = 48"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA384octets_def by presburger
qed
lemma SHA384octets_len2: "∀x. length (SHA384octets x) = 48"
using SHA384octets_len by blast
lemma SHA384octets_valid: "octets_valid (SHA384octets os)"
using nat_to_words_len_valid SHA384octets_def by presburger
lemma SHA384octets_valid2: "∀x. octets_valid (SHA384octets x)"
using SHA384octets_valid by satx
subsection ‹SHA-512›
definition SHA512octets :: "octets ⇒ octets" where
"SHA512octets os = nat_to_octets_len (SHA512 (octets_to_nat os) (8*(length os))) 64"
definition SHA512_hLen :: nat where
"SHA512_hLen = 64"
lemma SHA512octets_len: "length (SHA512octets os) = 64"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA512 ?M ?l < 2^512" using SHA512_bnd by blast
have 2: "(512::nat) = 8*64" by force
have 3: "SHA512 ?M ?l < (2^8)^64" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA512 ?M ?l) 64 ) = 64"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA512octets_def by presburger
qed
lemma SHA512octets_len2: "∀x. length (SHA512octets x) = 64"
using SHA512octets_len by blast
lemma SHA512octets_valid: "octets_valid (SHA512octets os)"
using nat_to_words_len_valid SHA512octets_def by presburger
lemma SHA512octets_valid2: "∀x. octets_valid (SHA512octets x)"
using SHA512octets_valid by satx
subsection ‹SHA-512/224›
definition SHA512_224octets :: "octets ⇒ octets" where
"SHA512_224octets os = nat_to_octets_len (SHA512_224 (octets_to_nat os) (8*(length os))) 28"
definition SHA512_224_hLen :: nat where
"SHA512_224_hLen = 28"
lemma SHA512_224octets_len: "length (SHA512_224octets os) = 28"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA512_224 ?M ?l < 2^224" using SHA512_224_bnd by blast
have 2: "(224::nat) = 8*28" by force
have 3: "SHA512_224 ?M ?l < (2^8)^28" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA512_224 ?M ?l) 28 ) = 28"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA512_224octets_def by presburger
qed
lemma SHA512_224octets_len2: "∀x. length (SHA512_224octets x) = 28"
using SHA512_224octets_len by blast
lemma SHA512_224octets_valid: "octets_valid (SHA512_224octets os)"
using nat_to_words_len_valid SHA512_224octets_def by presburger
lemma SHA512_224octets_valid2: "∀x. octets_valid (SHA512_224octets x)"
using SHA512_224octets_valid by satx
subsection ‹SHA-512/256›
definition SHA512_256octets :: "octets ⇒ octets" where
"SHA512_256octets os = nat_to_octets_len (SHA512_256 (octets_to_nat os) (8*(length os))) 32"
definition SHA512_256_hLen :: nat where
"SHA512_256_hLen = 32"
lemma SHA512_256octets_len: "length (SHA512_256octets os) = 32"
proof -
let ?M = "(octets_to_nat os)"
let ?l = "8*(length os)"
have 1: "SHA512_256 ?M ?l < 2^256" using SHA512_256_bnd by blast
have 2: "(256::nat) = 8*32" by force
have 3: "SHA512_256 ?M ?l < (2^8)^32" by (metis 1 2 power_mult)
have 4: "length ( nat_to_octets_len (SHA512_256 ?M ?l) 32 ) = 32"
using 3 nat_to_words_len_upbnd by force
show ?thesis using 4 SHA512_256octets_def by presburger
qed
lemma SHA512_256octets_len2: "∀x. length (SHA512_256octets x) = 32"
using SHA512_256octets_len by blast
lemma SHA512_256octets_valid: "octets_valid (SHA512_256octets os)"
using nat_to_words_len_valid SHA512_256octets_def by presburger
lemma SHA512_256octets_valid2: "∀x. octets_valid (SHA512_256octets x)"
using SHA512_256octets_valid by satx
end