Skip to content

Commit 8140422

Browse files
xrchzxrchz
authored
Merge pull request #1358 from HOL-Theorem-Prover/sha2
Define SHA-256 (part of the SHA-2 standard) and translate it for cv compute
2 parents 6c54683 + 2671daf commit 8140422

File tree

3 files changed

+256
-1
lines changed

3 files changed

+256
-1
lines changed

‎examples/Crypto/SHA-2/Holmakefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
INCLUDES = $(HOLDIR)/src/num/theories/cv_compute/automation

‎examples/Crypto/SHA-2/sha2Script.sml

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
1+
open HolKernel boolLib bossLib Parse
2+
listTheory rich_listTheory arithmeticTheory logrootTheory
3+
bitTheory wordsTheory numposrepTheory byteTheory wordsLib
4+
dividesTheory cv_transLib cv_stdTheory
5+
6+
(* The SHA-2 Standard: https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf *)
7+
(* SHA-256 in particular (i.e. Section 6.2) *)
8+
9+
val _ = new_theory"sha2";
10+
11+
(* TODO: move *)
12+
val () = cv_auto_trans numposrepTheory.n2l_n2lA;
13+
14+
Definition pad_message_def:
15+
pad_message bits =
16+
let l = LENGTH bits in
17+
let n = (l + 1) MOD 512 in
18+
let k = if n <= 448 then 448 - n else 512 + 448 - n in
19+
let lb = PAD_LEFT 0 64 $ (if l = 0 then [] else REVERSE $ n2l 2 l) in
20+
bits ++ 1 :: REPLICATE k 0 ++ lb
21+
End
22+
23+
val () = cv_auto_trans pad_message_def;
24+
25+
Theorem pad_message_length_multiple:
26+
LENGTH bs < 2 ** 64 ==>
27+
divides 512 $ LENGTH (pad_message bs)
28+
Proof
29+
rewrite_tac[pad_message_def, PAD_LEFT, ADD1]
30+
\\ strip_tac
31+
\\ BasicProvers.LET_ELIM_TAC
32+
\\ Cases_on`l = 0` \\ gs[Abbr`n`, Abbr`lb`, Abbr`k`]
33+
\\ simp[LENGTH_n2l, ADD1, LOG2_def]
34+
\\ `LOG2 l < 64`
35+
by ( qspecl_then[`l`,`64`]mp_tac LT_TWOEXP \\ simp[] )
36+
\\ gs[LOG2_def]
37+
\\ qspec_then `512` mp_tac DIVISION
38+
\\ impl_tac >- rw[]
39+
\\ disch_then(qspec_then`l + 1`mp_tac)
40+
\\ strip_tac
41+
\\ qpat_x_assum`l + 1 = _`(assume_tac o SYM)
42+
\\ `(l + 1) MOD 512 = l + 1 - (l + 1) DIV 512 * 512` by simp[]
43+
\\ pop_assum SUBST1_TAC
44+
\\ IF_CASES_TAC
45+
\\ simp[]
46+
\\ irule DIVIDES_ADD_1
47+
\\ simp[]
48+
\\ simp[divides_def]
49+
QED
50+
51+
Definition parse_block_def:
52+
parse_block acc bits =
53+
if NULL bits then REVERSE acc : word32 list
54+
else parse_block
55+
((word_from_bin_list $ REVERSE $ TAKE 32 bits)::acc)
56+
(DROP 32 bits)
57+
Termination
58+
WF_REL_TAC`measure (LENGTH o SND)` \\ Cases \\ rw[]
59+
End
60+
61+
val () = cv_auto_trans parse_block_def;
62+
63+
Definition parse_message_def:
64+
parse_message acc bits =
65+
if NULL bits then REVERSE acc else
66+
parse_message (parse_block [] (TAKE 512 bits) :: acc) (DROP 512 bits)
67+
Termination
68+
WF_REL_TAC`measure (LENGTH o SND)` \\ Cases \\ rw[]
69+
End
70+
71+
val () = cv_auto_trans parse_message_def;
72+
73+
Definition initial_hash_value_def:
74+
initial_hash_value = (
75+
0x6a09e667w : word32,
76+
0xbb67ae85w : word32,
77+
0x3c6ef372w : word32,
78+
0xa54ff53aw : word32,
79+
0x510e527fw : word32,
80+
0x9b05688cw : word32,
81+
0x1f83d9abw : word32,
82+
0x5be0cd19w : word32
83+
)
84+
End
85+
86+
val () = cv_trans_deep_embedding EVAL initial_hash_value_def;
87+
88+
Definition rotr_def:
89+
rotr n (x: 'a word) = x >>> n || x << (dimindex(:'a) - n)
90+
End
91+
92+
val () = cv_auto_trans (INST_TYPE[alpha |-> ``:32``] rotr_def);
93+
94+
Definition sigma0_def:
95+
sigma0 (x: word32) = rotr 7 x ?? rotr 18 x ?? x >>> 3
96+
End
97+
98+
Definition sigma1_def:
99+
sigma1 (x: word32) = rotr 17 x ?? rotr 19 x ?? x >>> 10
100+
End
101+
102+
val () = cv_auto_trans sigma0_def;
103+
val () = cv_auto_trans sigma1_def;
104+
105+
Definition Sigma0_def:
106+
Sigma0 (x: word32) = rotr 2 x ?? rotr 13 x ?? rotr 22 x
107+
End
108+
109+
Definition Sigma1_def:
110+
Sigma1 (x: word32) = rotr 6 x ?? rotr 11 x ?? rotr 25 x
111+
End
112+
113+
val () = cv_auto_trans Sigma0_def;
114+
val () = cv_auto_trans Sigma1_def;
115+
116+
Definition initial_schedule_loop_def:
117+
initial_schedule_loop Ws t =
118+
if t ≥ 64 ∨ t < 16 ∨ LENGTH Ws < t then
119+
REVERSE Ws
120+
else let
121+
Wt2 = EL 1 Ws;
122+
Wt7 = EL 6 Ws;
123+
Wt15 = EL 14 Ws;
124+
Wt16 = EL 15 Ws;
125+
Wt = sigma1 Wt2 + Wt7 + sigma0 Wt15 + Wt16
126+
in
127+
initial_schedule_loop (Wt::Ws) (SUC t)
128+
Termination
129+
WF_REL_TAC`measure (λx. 64 - SND x)`
130+
End
131+
132+
val initial_schedule_loop_pre_def = cv_auto_trans_pre initial_schedule_loop_def;
133+
134+
Theorem initial_schedule_loop_pre[cv_pre]:
135+
∀Ws t. initial_schedule_loop_pre Ws t
136+
Proof
137+
ho_match_mp_tac initial_schedule_loop_ind
138+
\\ rw[initial_schedule_loop_def]
139+
\\ rw[Once initial_schedule_loop_pre_def]
140+
QED
141+
142+
Definition initial_schedule_def:
143+
initial_schedule block =
144+
initial_schedule_loop (REVERSE block) 16
145+
End
146+
147+
val () = cv_auto_trans initial_schedule_def;
148+
149+
Definition K_def:
150+
K: word32 list = [
151+
0x428a2f98w; 0x71374491w; 0xb5c0fbcfw; 0xe9b5dba5w; 0x3956c25bw; 0x59f111f1w; 0x923f82a4w; 0xab1c5ed5w;
152+
0xd807aa98w; 0x12835b01w; 0x243185bew; 0x550c7dc3w; 0x72be5d74w; 0x80deb1few; 0x9bdc06a7w; 0xc19bf174w;
153+
0xe49b69c1w; 0xefbe4786w; 0x0fc19dc6w; 0x240ca1ccw; 0x2de92c6fw; 0x4a7484aaw; 0x5cb0a9dcw; 0x76f988daw;
154+
0x983e5152w; 0xa831c66dw; 0xb00327c8w; 0xbf597fc7w; 0xc6e00bf3w; 0xd5a79147w; 0x06ca6351w; 0x14292967w;
155+
0x27b70a85w; 0x2e1b2138w; 0x4d2c6dfcw; 0x53380d13w; 0x650a7354w; 0x766a0abbw; 0x81c2c92ew; 0x92722c85w;
156+
0xa2bfe8a1w; 0xa81a664bw; 0xc24b8b70w; 0xc76c51a3w; 0xd192e819w; 0xd6990624w; 0xf40e3585w; 0x106aa070w;
157+
0x19a4c116w; 0x1e376c08w; 0x2748774cw; 0x34b0bcb5w; 0x391c0cb3w; 0x4ed8aa4aw; 0x5b9cca4fw; 0x682e6ff3w;
158+
0x748f82eew; 0x78a5636fw; 0x84c87814w; 0x8cc70208w; 0x90befffaw; 0xa4506cebw; 0xbef9a3f7w; 0xc67178f2w;
159+
]
160+
End
161+
162+
val () = cv_trans_deep_embedding EVAL K_def;
163+
164+
Definition Ch_def:
165+
Ch (x:word32) y z = (x && y) ?? (¬x && z)
166+
End
167+
168+
val () = cv_auto_trans Ch_def;
169+
170+
Definition Maj_def:
171+
Maj (x:word32) y z = (x && y) ?? (x && z) ?? (y && z)
172+
End
173+
174+
val () = cv_auto_trans Maj_def;
175+
176+
Definition step3_def:
177+
step3 Ws (t, (a, b, c, d, e, f, g, h)) = let
178+
t1 = h + Sigma1 e + Ch e f g +
179+
(if t < 64 then EL t K else 0w) +
180+
(if t < LENGTH Ws then EL t Ws else 0w);
181+
t2 = Sigma0 a + Maj a b c;
182+
h = g;
183+
g = f;
184+
f = e;
185+
e = d + t1;
186+
d = c;
187+
c = b;
188+
b = a;
189+
a = t1 + t2 in
190+
(SUC t, (a, b, c, d, e, f, g, h))
191+
End
192+
193+
val step3_pre_def = cv_auto_trans_pre step3_def;
194+
195+
Theorem step3_pre[cv_pre]:
196+
step3_pre Ws v
197+
Proof
198+
rw[step3_pre_def, K_def]
199+
QED
200+
201+
Definition process_block_def:
202+
process_block hash block = let
203+
Ws = initial_schedule block;
204+
hs = FUNPOW (step3 Ws) 64 (0, hash);
205+
in case (hash, hs) of ((a0,b0,c0,d0,e0,f0,g0,h0),(_,(a,b,c,d,e,f,g,h)))
206+
=> (a0+a, b0+b, c0+c, d0+d, e0+e, f0+f, g0+g, h0+h)
207+
End
208+
209+
val () = cv_auto_trans process_block_def;
210+
211+
Definition process_blocks_def:
212+
process_blocks bs = FOLDL process_block initial_hash_value bs
213+
End
214+
215+
val () = cv_auto_trans process_blocks_def;
216+
217+
Definition SHA_256_def:
218+
SHA_256 m : 256 word = let
219+
p = pad_message m;
220+
blocks = parse_message [] p
221+
in
222+
case process_blocks blocks of
223+
(a, b, c, d, e, f, g, h)
224+
=> concat_word_list [h; g; f; e; d; c; b; a]
225+
End
226+
227+
val () = cv_auto_trans SHA_256_def;
228+
229+
Definition SHA_256_bytes_def:
230+
SHA_256_bytes (bs: word8 list) =
231+
SHA_256 $ FLAT $
232+
MAP (REVERSE o PAD_RIGHT 0 8 o word_to_bin_list) bs
233+
End
234+
235+
val () = cv_auto_trans SHA_256_bytes_def;
236+
237+
Theorem SHA_256_bytes_abc:
238+
SHA_256_bytes (MAP (n2w o ORD) "abc") =
239+
0xBA7816BF8F01CFEA414140DE5DAE2223B00361A396177A9CB410FF61F20015ADw
240+
Proof
241+
CONV_TAC(PATH_CONV"lrr"EVAL)
242+
\\ (fn g => (g |> #2 |> lhs |> cv_eval |> ACCEPT_TAC) g)
243+
QED
244+
245+
Theorem SHA_256_bytes_two_blocks:
246+
SHA_256_bytes (MAP (n2w o ORD)
247+
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq") =
248+
0x248D6A61D20638B8E5C026930C3E6039A33CE45964FF2167F6ECEDD419DB06C1w
249+
Proof
250+
CONV_TAC(PATH_CONV"lrr"EVAL)
251+
\\ (fn g => (g |> #2 |> lhs |> cv_eval |> ACCEPT_TAC) g)
252+
QED
253+
254+
val _ = export_theory();

‎src/parallel_builds/core/Holmakefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ ifdef HOLSELFTESTLEVEL
3232
# example directories to build at selftest level 1
3333
EXDIRS = algebra/aat \
3434
arm/arm6-verification arm/armv8-memory-model arm/experimental \
35-
CCS Crypto/RSA Hoare-for-divergence MLsyntax \
35+
CCS Crypto/RSA Crypto/SHA-2 Hoare-for-divergence MLsyntax \
3636
PSL/1.01/executable-semantics PSL/1.1/official-semantics \
3737
STE algorithms computability countchars dependability dev \
3838
developers/ThmSetData \

0 commit comments

Comments
 (0)