author | berghofe |
Wed, 30 Apr 2014 15:43:44 +0200 | |
changeset 56798 | 939e88e79724 |
parent 41561 | d1318f3c86ba |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
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 |
||
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
41561
diff
changeset
|
11 |
spark_open "rmd/hash" |
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)" |
|
66 |
thus ?thesis by (cases a) simp |
|
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 |
|
86 |
have "0 <= loop__1__i + 1" using `0 <= loop__1__i` by simp |
|
87 |
show ?thesis |
|
88 |
unfolding loop_suc |
|
89 |
unfolding rounds'_step[OF `0 <= loop__1__i + 1`] |
|
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 |