author | steckerm |
Sat, 20 Sep 2014 10:44:24 +0200 | |
changeset 58407 | 111d801b5d5d |
parent 48260 | 65ed3b2b3157 |
child 61830 | 4f5ab843cf5b |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Guard_Public.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2002 University of Cambridge |
|
13508 | 4 |
|
41775 | 5 |
Lemmas on guarded messages for public protocols. |
6 |
*) |
|
13508 | 7 |
|
48260 | 8 |
theory Guard_Public imports Guard "../Public" Extensions begin |
13508 | 9 |
|
10 |
subsection{*Extensions to Theory @{text Public}*} |
|
11 |
||
12 |
declare initState.simps [simp del] |
|
13 |
||
14 |
subsubsection{*signature*} |
|
15 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
16 |
definition sign :: "agent => msg => msg" where |
13508 | 17 |
"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}" |
18 |
||
19 |
lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')" |
|
20 |
by (auto simp: sign_def) |
|
21 |
||
22 |
subsubsection{*agent associated to a key*} |
|
23 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
24 |
definition agt :: "key => agent" where |
13508 | 25 |
"agt K == @A. K = priK A | K = pubK A" |
26 |
||
27 |
lemma agt_priK [simp]: "agt (priK A) = A" |
|
28 |
by (simp add: agt_def) |
|
29 |
||
30 |
lemma agt_pubK [simp]: "agt (pubK A) = A" |
|
31 |
by (simp add: agt_def) |
|
32 |
||
33 |
subsubsection{*basic facts about @{term initState}*} |
|
34 |
||
35 |
lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)" |
|
36 |
by (cases A, auto simp: initState.simps) |
|
37 |
||
38 |
lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)" |
|
39 |
by auto |
|
40 |
||
41 |
lemma no_priK_in_analz_init [simp]: "A ~:bad |
|
42 |
==> Key (priK A) ~:analz (initState Spy)" |
|
43 |
by (auto simp: initState.simps) |
|
44 |
||
45 |
lemma priK_notin_initState_Friend [simp]: "A ~= Friend C |
|
46 |
==> Key (priK A) ~: parts (initState (Friend C))" |
|
47 |
by (auto simp: initState.simps) |
|
48 |
||
49 |
lemma keyset_init [iff]: "keyset (initState A)" |
|
50 |
by (cases A, auto simp: keyset_def initState.simps) |
|
51 |
||
52 |
subsubsection{*sets of private keys*} |
|
53 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
54 |
definition priK_set :: "key set => bool" where |
13508 | 55 |
"priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)" |
56 |
||
57 |
lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A" |
|
58 |
by (simp add: priK_set_def) |
|
59 |
||
60 |
lemma priK_set1 [iff]: "priK_set {priK A}" |
|
61 |
by (simp add: priK_set_def) |
|
62 |
||
63 |
lemma priK_set2 [iff]: "priK_set {priK A, priK B}" |
|
64 |
by (simp add: priK_set_def) |
|
65 |
||
66 |
subsubsection{*sets of good keys*} |
|
67 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
68 |
definition good :: "key set => bool" where |
13508 | 69 |
"good Ks == ALL K. K:Ks --> agt K ~:bad" |
70 |
||
71 |
lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad" |
|
72 |
by (simp add: good_def) |
|
73 |
||
74 |
lemma good1 [simp]: "A ~:bad ==> good {priK A}" |
|
75 |
by (simp add: good_def) |
|
76 |
||
77 |
lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}" |
|
78 |
by (simp add: good_def) |
|
79 |
||
80 |
subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*} |
|
81 |
||
35418 | 82 |
primrec greatest :: "event list => nat" |
83 |
where |
|
84 |
"greatest [] = 0" |
|
85 |
| "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)" |
|
13508 | 86 |
|
87 |
lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs" |
|
88 |
apply (induct evs, auto simp: initState.simps) |
|
89 |
apply (drule used_sub_parts_used, safe) |
|
90 |
apply (drule greatest_msg_is_greatest, arith) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
16417
diff
changeset
|
91 |
by simp |
13508 | 92 |
|
93 |
subsubsection{*function giving a new nonce*} |
|
94 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
95 |
definition new :: "event list => nat" where |
13508 | 96 |
"new evs == Suc (greatest evs)" |
97 |
||
98 |
lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs" |
|
99 |
by (clarify, drule greatest_is_greatest, auto simp: new_def) |
|
100 |
||
101 |
subsection{*Proofs About Guarded Messages*} |
|
102 |
||
103 |
subsubsection{*small hack necessary because priK is defined as the inverse of pubK*} |
|
104 |
||
105 |
lemma pubK_is_invKey_priK: "pubK A = invKey (priK A)" |
|
106 |
by simp |
|
107 |
||
108 |
lemmas pubK_is_invKey_priK_substI = pubK_is_invKey_priK [THEN ssubst] |
|
109 |
||
110 |
lemmas invKey_invKey_substI = invKey [THEN ssubst] |
|
111 |
||
112 |
lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}" |
|
113 |
apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI) |
|
114 |
by (rule Guard_Nonce, simp+) |
|
115 |
||
116 |
subsubsection{*guardedness results*} |
|
117 |
||
118 |
lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks" |
|
119 |
by (auto simp: sign_def) |
|
120 |
||
121 |
lemma Guard_init [iff]: "Guard n Ks (initState B)" |
|
122 |
by (induct B, auto simp: Guard_def initState.simps) |
|
123 |
||
124 |
lemma Guard_knows_max': "Guard n Ks (knows_max' C evs) |
|
125 |
==> Guard n Ks (knows_max C evs)" |
|
126 |
by (simp add: knows_max_def) |
|
127 |
||
128 |
lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs |
|
129 |
==> Guard n Ks (spies evs)" |
|
130 |
by (auto simp: Guard_def dest: not_used_not_known parts_sub) |
|
131 |
||
132 |
lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs; |
|
133 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)" |
|
134 |
by (auto simp: Guard_def dest: known_used parts_trans) |
|
135 |
||
136 |
lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs; |
|
137 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)" |
|
138 |
by (auto simp: Guard_def dest: known_max_used parts_trans) |
|
139 |
||
140 |
lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs; |
|
141 |
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)" |
|
142 |
apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono) |
|
143 |
by (auto simp: knows_max_def) |
|
144 |
||
145 |
subsubsection{*regular protocols*} |
|
146 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
20217
diff
changeset
|
147 |
definition regular :: "event list set => bool" where |
13508 | 148 |
"regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)" |
149 |
||
150 |
lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
151 |
(Key (priK A):parts (spies evs)) = (A:bad)" |
|
152 |
by (auto simp: regular_def) |
|
153 |
||
154 |
lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==> |
|
155 |
(Key (priK A):analz (spies evs)) = (A:bad)" |
|
156 |
by auto |
|
157 |
||
158 |
lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p; |
|
159 |
priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)" |
|
160 |
apply (clarify, simp only: knows_decomp) |
|
161 |
apply (drule Guard_invKey_keyset, simp+, safe) |
|
162 |
apply (drule in_good, simp) |
|
163 |
apply (drule in_priK_set, simp+, clarify) |
|
164 |
apply (frule_tac A=A in priK_analz_iff_bad) |
|
165 |
by (simp add: knows_decomp)+ |
|
166 |
||
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
16417
diff
changeset
|
167 |
end |