41561
|
1 |
(* Title: HOL/SPARK/Examples/RIPEMD-160/Hash.thy
|
|
2 |
Author: Fabian Immler, TU Muenchen
|
|
3 |
|
|
4 |
Verification of the RIPEMD-160 hash function
|
|
5 |
*)
|
|
6 |
|
|
7 |
theory Hash
|
|
8 |
imports RMD_Specification
|
|
9 |
begin
|
|
10 |
|
69605
|
11 |
spark_open \<open>rmd/hash\<close>
|
41561
|
12 |
|
|
13 |
abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
|
|
14 |
"from_chain c \<equiv> (
|
|
15 |
word_of_int (h0 c),
|
|
16 |
word_of_int (h1 c),
|
|
17 |
word_of_int (h2 c),
|
|
18 |
word_of_int (h3 c),
|
|
19 |
word_of_int (h4 c))"
|
|
20 |
|
|
21 |
abbreviation to_chain :: "RMD.chain \<Rightarrow> chain" where
|
|
22 |
"to_chain c \<equiv>
|
|
23 |
(let (h0, h1, h2, h3, h4) = c in
|
|
24 |
(|h0 = uint h0,
|
|
25 |
h1 = uint h1,
|
|
26 |
h2 = uint h2,
|
|
27 |
h3 = uint h3,
|
|
28 |
h4 = uint h4|))"
|
|
29 |
|
|
30 |
abbreviation round' :: "chain \<Rightarrow> block \<Rightarrow> chain" where
|
|
31 |
"round' c b == to_chain (round (\<lambda>n. word_of_int (b (int n))) (from_chain c))"
|
|
32 |
|
|
33 |
abbreviation rounds' :: "chain \<Rightarrow> int \<Rightarrow> message \<Rightarrow> chain" where
|
|
34 |
"rounds' h i X ==
|
|
35 |
to_chain (rounds
|
|
36 |
(\<lambda>n. \<lambda>m. word_of_int (X (int n) (int m)))
|
|
37 |
(from_chain h)
|
|
38 |
(nat i))"
|
|
39 |
|
|
40 |
abbreviation rmd_hash :: "message \<Rightarrow> int \<Rightarrow> chain" where
|
|
41 |
"rmd_hash X i == to_chain (rmd
|
|
42 |
(\<lambda>n. \<lambda>m. word_of_int (X (int n) (int m)))
|
|
43 |
(nat i))"
|
|
44 |
|
|
45 |
spark_proof_functions
|
|
46 |
round_spec = round'
|
|
47 |
rounds = rounds'
|
|
48 |
rmd_hash = rmd_hash
|
|
49 |
|
|
50 |
spark_vc function_hash_12
|
|
51 |
using H1 H6
|
|
52 |
by (simp add:
|
|
53 |
rounds_def rmd_body_def round_def
|
|
54 |
h_0_def h0_0_def h1_0_def h2_0_def h3_0_def h4_0_def)
|
|
55 |
|
|
56 |
|
|
57 |
lemma rounds_step:
|
|
58 |
assumes "0 <= i"
|
|
59 |
shows "rounds X b (Suc i) = round (X i) (rounds X b i)"
|
|
60 |
by (simp add: rounds_def rmd_body_def)
|
|
61 |
|
|
62 |
lemma from_to_id: "from_chain (to_chain C) = C"
|
|
63 |
proof (cases C)
|
|
64 |
fix a b c d e f::word32
|
|
65 |
assume "C = (a, b, c, d, e)"
|
72262
|
66 |
thus ?thesis by (cases a) (simp add: take_bit_nat_eq_self)
|
41561
|
67 |
qed
|
|
68 |
|
|
69 |
lemma steps_to_steps':
|
|
70 |
"round X (foldl a b c) = round X (from_chain (to_chain (foldl a b c)))"
|
|
71 |
unfolding from_to_id ..
|
|
72 |
|
|
73 |
lemma rounds'_step:
|
|
74 |
assumes "0 <= i"
|
|
75 |
shows "rounds' c (i + 1) x = round' (rounds' c i x) (x i)"
|
|
76 |
proof -
|
|
77 |
have makesuc: "nat (i + 1) = Suc (nat i)" using assms by simp
|
|
78 |
show ?thesis using assms
|
|
79 |
by (simp add: makesuc rounds_def rmd_body_def steps_to_steps')
|
|
80 |
qed
|
|
81 |
|
|
82 |
|
|
83 |
spark_vc function_hash_13
|
|
84 |
proof -
|
|
85 |
have loop_suc: "loop__1__i + 2 = (loop__1__i + 1) + 1" by simp
|
63167
|
86 |
have "0 <= loop__1__i + 1" using \<open>0 <= loop__1__i\<close> by simp
|
41561
|
87 |
show ?thesis
|
|
88 |
unfolding loop_suc
|
63167
|
89 |
unfolding rounds'_step[OF \<open>0 <= loop__1__i + 1\<close>]
|
41561
|
90 |
unfolding H1[symmetric]
|
|
91 |
unfolding H18 ..
|
|
92 |
qed
|
|
93 |
|
|
94 |
|
|
95 |
spark_vc function_hash_17
|
|
96 |
unfolding rmd_def H1 rounds_def ..
|
|
97 |
|
|
98 |
spark_end
|
|
99 |
|
|
100 |
end
|