author | huffman |
Sat, 14 Feb 2009 01:24:01 -0800 | |
changeset 29908 | b82ab2aebbbf |
parent 26019 | ecbfe2645694 |
child 30509 | e19d5b459a61 |
permissions | -rw-r--r-- |
11250 | 1 |
(* Title: HOL/Auth/Public |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Theory of Public Keys (common to all public-key protocols) |
|
7 |
||
8 |
Private and public keys; initial states of agents |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
9 |
*)(*<*) |
16417 | 10 |
theory Public imports Event |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
11 |
begin |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
12 |
(*>*) |
11250 | 13 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
14 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
15 |
The function |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
16 |
@{text pubK} maps agents to their public keys. The function |
25341 | 17 |
@{text priK} maps agents to their private keys. It is merely |
18 |
an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of |
|
19 |
@{text invKey} and @{text pubK}. |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
20 |
*} |
11250 | 21 |
|
25341 | 22 |
consts pubK :: "agent \<Rightarrow> key" |
23 |
abbreviation priK :: "agent \<Rightarrow> key" |
|
24 |
where "priK x \<equiv> invKey(pubK x)" |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
25 |
(*<*) |
11250 | 26 |
primrec |
27 |
(*Agents know their private key and all public keys*) |
|
28 |
initState_Server: "initState Server = |
|
29 |
insert (Key (priK Server)) (Key ` range pubK)" |
|
30 |
initState_Friend: "initState (Friend i) = |
|
31 |
insert (Key (priK (Friend i))) (Key ` range pubK)" |
|
32 |
initState_Spy: "initState Spy = |
|
33 |
(Key`invKey`pubK`bad) Un (Key ` range pubK)" |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
34 |
(*>*) |
11250 | 35 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
36 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
37 |
\noindent |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
38 |
The set @{text bad} consists of those agents whose private keys are known to |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
39 |
the spy. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
40 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
41 |
Two axioms are asserted about the public-key cryptosystem. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
42 |
No two agents have the same public key, and no private key equals |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
43 |
any public key. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
44 |
*} |
11250 | 45 |
|
46 |
axioms |
|
47 |
inj_pubK: "inj pubK" |
|
25341 | 48 |
priK_neq_pubK: "priK A \<noteq> pubK B" |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
49 |
(*<*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
50 |
lemmas [iff] = inj_pubK [THEN inj_eq] |
11250 | 51 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
52 |
lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
53 |
apply safe |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
54 |
apply (drule_tac f=invKey in arg_cong) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
55 |
apply simp |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
56 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
57 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
58 |
lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
59 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
60 |
lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
61 |
by (simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
62 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
63 |
lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
64 |
by (simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
65 |
|
25341 | 66 |
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'" |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
67 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
68 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
69 |
lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
70 |
==> X \<in> analz H" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
71 |
by (auto simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
72 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
73 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
74 |
(** "Image" equations that hold for injective functions **) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
75 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
76 |
lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
77 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
78 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
79 |
(*holds because invKey is injective*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
80 |
lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
81 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
82 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
83 |
lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
84 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
85 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
86 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
87 |
(** Rewrites should not refer to initState(Friend i) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
88 |
-- not in normal form! **) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
89 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
90 |
lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
91 |
apply (unfold keysFor_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
92 |
apply (induct C) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
93 |
apply (auto intro: range_eqI) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
94 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
95 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
96 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
97 |
(*** Function "spies" ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
98 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
99 |
(*Agents see their own private keys!*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
100 |
lemma priK_in_initState[iff]: "Key (priK A) : initState A" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
101 |
by (induct A) auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
102 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
103 |
(*All public keys are visible*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
104 |
lemma spies_pubK[iff]: "Key (pubK A) : spies evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
105 |
by (induct evs) (simp_all add: imageI knows_Cons split: event.split) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
106 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
107 |
(*Spy sees private keys of bad agents!*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
108 |
lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
109 |
by (induct evs) (simp_all add: imageI knows_Cons split: event.split) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
110 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
111 |
lemmas [iff] = spies_pubK [THEN analz.Inj] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
112 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
113 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
114 |
(*** Fresh nonces ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
115 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
116 |
lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
117 |
by (induct B) auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
118 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
119 |
lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
120 |
by (simp add: used_Nil) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
121 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
122 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
123 |
(*** Supply fresh nonces for possibility theorems. ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
124 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
125 |
(*In any trace, there is an upper bound N on the greatest nonce in use.*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
126 |
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
127 |
apply (induct_tac "evs") |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
128 |
apply (rule_tac x = 0 in exI) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
129 |
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
130 |
apply safe |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
131 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
132 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
133 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
134 |
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
135 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
136 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
137 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
138 |
apply (rule Nonce_supply_lemma [THEN exE]) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
139 |
apply (rule someI, fast) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
140 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
141 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
142 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
143 |
(*** Specialized rewriting for the analz_image_... theorems ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
144 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
145 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
146 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
147 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
148 |
lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
149 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
150 |
|
11250 | 151 |
|
152 |
(*Specialized methods*) |
|
153 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
154 |
(*Tactic for possibility theorems*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
155 |
ML {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
156 |
fun possibility_tac st = st |> |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
157 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
26019 | 158 |
(ALLGOALS (simp_tac (@{simpset} delsimps [used_Says])) |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
159 |
THEN |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
160 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
161 |
resolve_tac [refl, conjI, @{thm Nonce_supply}])); |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
162 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
163 |
|
11250 | 164 |
method_setup possibility = {* |
165 |
Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} |
|
166 |
"for proving possibility theorems" |
|
167 |
||
168 |
end |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
169 |
(*>*) |