author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 56681 | e8d5d60d655e |
child 61830 | 4f5ab843cf5b |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Guard_Shared.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2002 University of Cambridge |
|
4 |
*) |
|
13508 | 5 |
|
58889 | 6 |
section{*lemmas on guarded messages for protocols with symmetric keys*} |
13508 | 7 |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35416
diff
changeset
|
8 |
theory Guard_Shared imports Guard GuardK "../Shared" begin |
13508 | 9 |
|
10 |
subsection{*Extensions to Theory @{text Shared}*} |
|
11 |
||
12 |
declare initState.simps [simp del] |
|
13 |
||
14 |
subsubsection{*a little abbreviation*} |
|
15 |
||
19363 | 16 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19363
diff
changeset
|
17 |
Ciph :: "agent => msg => msg" where |
19363 | 18 |
"Ciph A X == Crypt (shrK A) X" |
13508 | 19 |
|
20 |
subsubsection{*agent associated to a key*} |
|
21 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
21404
diff
changeset
|
22 |
definition agt :: "key => agent" where |
13508 | 23 |
"agt K == @A. K = shrK A" |
24 |
||
25 |
lemma agt_shrK [simp]: "agt (shrK A) = A" |
|
26 |
by (simp add: agt_def) |
|
27 |
||
28 |
subsubsection{*basic facts about @{term initState}*} |
|
29 |
||
30 |
lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)" |
|
31 |
by (cases A, auto simp: initState.simps) |
|
32 |
||
33 |
lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)" |
|
34 |
by auto |
|
35 |
||
36 |
lemma no_shrK_in_analz_init [simp]: "A ~:bad |
|
37 |
==> Key (shrK A) ~:analz (initState Spy)" |
|
38 |
by (auto simp: initState.simps) |
|
39 |
||
40 |
lemma shrK_notin_initState_Friend [simp]: "A ~= Friend C |
|
41 |
==> Key (shrK A) ~: parts (initState (Friend C))" |
|
42 |
by (auto simp: initState.simps) |
|
43 |
||
44 |
lemma keyset_init [iff]: "keyset (initState A)" |
|
45 |
by (cases A, auto simp: keyset_def initState.simps) |
|
46 |
||
47 |
subsubsection{*sets of symmetric keys*} |
|
48 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
21404
diff
changeset
|
49 |
definition shrK_set :: "key set => bool" where |
13508 | 50 |
"shrK_set Ks == ALL K. K:Ks --> (EX A. K = shrK A)" |
51 |
||
52 |
lemma in_shrK_set: "[| shrK_set Ks; K:Ks |] ==> EX A. K = shrK A" |
|
53 |
by (simp add: shrK_set_def) |
|
54 |
||
55 |
lemma shrK_set1 [iff]: "shrK_set {shrK A}" |
|
56 |
by (simp add: shrK_set_def) |
|
57 |
||
58 |
lemma shrK_set2 [iff]: "shrK_set {shrK A, shrK B}" |
|
59 |
by (simp add: shrK_set_def) |
|
60 |
||
61 |
subsubsection{*sets of good keys*} |
|
62 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
21404
diff
changeset
|
63 |
definition good :: "key set => bool" where |
13508 | 64 |
"good Ks == ALL K. K:Ks --> agt K ~:bad" |
65 |
||
66 |
lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad" |
|
67 |
by (simp add: good_def) |
|
68 |
||
69 |
lemma good1 [simp]: "A ~:bad ==> good {shrK A}" |
|
70 |
by (simp add: good_def) |
|
71 |
||
72 |
lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {shrK A, shrK B}" |
|
73 |
by (simp add: good_def) |
|
74 |
||
75 |
||
76 |
subsection{*Proofs About Guarded Messages*} |
|
77 |
||
78 |
subsubsection{*small hack*} |
|
79 |
||
80 |
lemma shrK_is_invKey_shrK: "shrK A = invKey (shrK A)" |
|
81 |
by simp |
|
82 |
||
83 |
lemmas shrK_is_invKey_shrK_substI = shrK_is_invKey_shrK [THEN ssubst] |
|
84 |
||
85 |
lemmas invKey_invKey_substI = invKey [THEN ssubst] |
|
86 |
||
87 |
lemma "Nonce n:parts {X} ==> Crypt (shrK A) X:guard n {shrK A}" |
|
88 |
apply (rule shrK_is_invKey_shrK_substI, rule invKey_invKey_substI) |
|
89 |
by (rule Guard_Nonce, simp+) |
|
90 |
||
91 |
subsubsection{*guardedness results on nonces*} |
|
92 |
||
93 |
lemma guard_ciph [simp]: "shrK A:Ks ==> Ciph A X:guard n Ks" |
|
94 |
by (rule Guard_Nonce, simp) |
|
95 |
||
13523 | 96 |
lemma guardK_ciph [simp]: "shrK A:Ks ==> Ciph A X:guardK n Ks" |
13508 | 97 |
by (rule Guard_Key, simp) |
98 |
||
99 |
lemma Guard_init [iff]: "Guard n Ks (initState B)" |
|
100 |
by (induct B, auto simp: Guard_def initState.simps) |
|
101 |
||
102 |
lemma Guard_knows_max': "Guard n Ks (knows_max' C evs) |
|
103 |
==> Guard n Ks (knows_max C evs)" |
|
104 |
by (simp add: knows_max_def) |
|
105 |
||
106 |
lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs |
|
107 |
==> Guard n Ks (spies evs)" |
|
108 |
by (auto simp: Guard_def dest: not_used_not_known parts_sub) |
|
109 |
||
110 |
lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs; |
|
111 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)" |
|
112 |
by (auto simp: Guard_def dest: known_used parts_trans) |
|
113 |
||
114 |
lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs; |
|
115 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)" |
|
116 |
by (auto simp: Guard_def dest: known_max_used parts_trans) |
|
117 |
||
118 |
lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs; |
|
119 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)" |
|
120 |
apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono) |
|
121 |
by (auto simp: knows_max_def) |
|
122 |
||
123 |
subsubsection{*guardedness results on keys*} |
|
124 |
||
125 |
lemma GuardK_init [simp]: "n ~:range shrK ==> GuardK n Ks (initState B)" |
|
126 |
by (induct B, auto simp: GuardK_def initState.simps) |
|
127 |
||
128 |
lemma GuardK_knows_max': "[| GuardK n A (knows_max' C evs); n ~:range shrK |] |
|
129 |
==> GuardK n A (knows_max C evs)" |
|
130 |
by (simp add: knows_max_def) |
|
131 |
||
132 |
lemma Key_not_used_GuardK_spies [dest]: "Key n ~:used evs |
|
133 |
==> GuardK n A (spies evs)" |
|
134 |
by (auto simp: GuardK_def dest: not_used_not_known parts_sub) |
|
135 |
||
136 |
lemma Key_not_used_GuardK [dest]: "[| evs:p; Key n ~:used evs; |
|
137 |
Gets_correct p; one_step p |] ==> GuardK n A (knows (Friend C) evs)" |
|
138 |
by (auto simp: GuardK_def dest: known_used parts_trans) |
|
139 |
||
140 |
lemma Key_not_used_GuardK_max [dest]: "[| evs:p; Key n ~:used evs; |
|
141 |
Gets_correct p; one_step p |] ==> GuardK n A (knows_max (Friend C) evs)" |
|
142 |
by (auto simp: GuardK_def dest: known_max_used parts_trans) |
|
143 |
||
144 |
lemma Key_not_used_GuardK_max' [dest]: "[| evs:p; Key n ~:used evs; |
|
145 |
Gets_correct p; one_step p |] ==> GuardK n A (knows_max' (Friend C) evs)" |
|
146 |
apply (rule_tac H="knows_max (Friend C) evs" in GuardK_mono) |
|
147 |
by (auto simp: knows_max_def) |
|
148 |
||
149 |
subsubsection{*regular protocols*} |
|
150 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
21404
diff
changeset
|
151 |
definition regular :: "event list set => bool" where |
13508 | 152 |
"regular p == ALL evs A. evs:p --> (Key (shrK A):parts (spies evs)) = (A:bad)" |
153 |
||
154 |
lemma shrK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
155 |
(Key (shrK A):parts (spies evs)) = (A:bad)" |
|
156 |
by (auto simp: regular_def) |
|
157 |
||
158 |
lemma shrK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
159 |
(Key (shrK A):analz (spies evs)) = (A:bad)" |
|
160 |
by auto |
|
161 |
||
162 |
lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p; |
|
163 |
shrK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)" |
|
164 |
apply (clarify, simp only: knows_decomp) |
|
165 |
apply (drule Guard_invKey_keyset, simp+, safe) |
|
166 |
apply (drule in_good, simp) |
|
167 |
apply (drule in_shrK_set, simp+, clarify) |
|
168 |
apply (frule_tac A=A in shrK_analz_iff_bad) |
|
169 |
by (simp add: knows_decomp)+ |
|
170 |
||
171 |
lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p; |
|
172 |
shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)" |
|
173 |
apply (clarify, simp only: knows_decomp) |
|
56681 | 174 |
apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN) |
13508 | 175 |
apply clarify |
176 |
apply (drule in_good, simp) |
|
177 |
apply (drule in_shrK_set, simp+, clarify) |
|
178 |
apply (frule_tac A=A in shrK_analz_iff_bad) |
|
179 |
by (simp add: knows_decomp)+ |
|
180 |
||
181 |
end |