author | bulwahn |
Mon, 22 Mar 2010 08:30:12 +0100 | |
changeset 35876 | ac44e2312f0a |
parent 32960 | 69916a850301 |
child 39795 | 9e59b4c11039 |
permissions | -rw-r--r-- |
11250 | 1 |
(* Title: HOL/Auth/Public |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1996 University of Cambridge |
|
4 |
||
5 |
Theory of Public Keys (common to all public-key protocols) |
|
6 |
||
7 |
Private and public keys; initial states of agents |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
8 |
*)(*<*) |
16417 | 9 |
theory Public imports Event |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
10 |
begin |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
11 |
(*>*) |
11250 | 12 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
13 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
14 |
The function |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
15 |
@{text pubK} maps agents to their public keys. The function |
25341 | 16 |
@{text priK} maps agents to their private keys. It is merely |
17 |
an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of |
|
18 |
@{text invKey} and @{text pubK}. |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
19 |
*} |
11250 | 20 |
|
25341 | 21 |
consts pubK :: "agent \<Rightarrow> key" |
22 |
abbreviation priK :: "agent \<Rightarrow> key" |
|
23 |
where "priK x \<equiv> invKey(pubK x)" |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
24 |
(*<*) |
11250 | 25 |
primrec |
26 |
(*Agents know their private key and all public keys*) |
|
27 |
initState_Server: "initState Server = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
28 |
insert (Key (priK Server)) (Key ` range pubK)" |
11250 | 29 |
initState_Friend: "initState (Friend i) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
30 |
insert (Key (priK (Friend i))) (Key ` range pubK)" |
11250 | 31 |
initState_Spy: "initState Spy = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
32 |
(Key`invKey`pubK`bad) Un (Key ` range pubK)" |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
33 |
(*>*) |
11250 | 34 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
35 |
text {* |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
36 |
\noindent |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
37 |
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
|
38 |
the spy. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
39 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
40 |
Two axioms are asserted about the public-key cryptosystem. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
41 |
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
|
42 |
any public key. |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
43 |
*} |
11250 | 44 |
|
45 |
axioms |
|
46 |
inj_pubK: "inj pubK" |
|
25341 | 47 |
priK_neq_pubK: "priK A \<noteq> pubK B" |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
48 |
(*<*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
49 |
lemmas [iff] = inj_pubK [THEN inj_eq] |
11250 | 50 |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
51 |
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
|
52 |
apply safe |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
53 |
apply (drule_tac f=invKey in arg_cong) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
54 |
apply simp |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
55 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
56 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
57 |
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
|
58 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
59 |
lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
60 |
by (simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
61 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
62 |
lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
63 |
by (simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
64 |
|
25341 | 65 |
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
|
66 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
67 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
68 |
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
|
69 |
==> X \<in> analz H" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
70 |
by (auto simp add: symKeys_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
71 |
|
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 |
(** "Image" equations that hold for injective functions **) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
74 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
75 |
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
|
76 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
77 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
78 |
(*holds because invKey is injective*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
79 |
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
|
80 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
81 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
82 |
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
|
83 |
by auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
84 |
|
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 |
(** Rewrites should not refer to initState(Friend i) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
87 |
-- not in normal form! **) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
88 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
89 |
lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
90 |
apply (unfold keysFor_def) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
91 |
apply (induct C) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
92 |
apply (auto intro: range_eqI) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
93 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
94 |
|
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 |
(*** Function "spies" ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
97 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
98 |
(*Agents see their own private keys!*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
99 |
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
|
100 |
by (induct A) auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
101 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
102 |
(*All public keys are visible*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
103 |
lemma spies_pubK[iff]: "Key (pubK A) : spies evs" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
104 |
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
|
105 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
106 |
(*Spy sees private keys of bad agents!*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
107 |
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
|
108 |
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
|
109 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
110 |
lemmas [iff] = spies_pubK [THEN analz.Inj] |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
111 |
|
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 |
(*** Fresh nonces ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
114 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
115 |
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
|
116 |
by (induct B) auto |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
117 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
118 |
lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []" |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
119 |
by (simp add: used_Nil) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
120 |
|
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 |
(*** Supply fresh nonces for possibility theorems. ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
123 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
124 |
(*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
|
125 |
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
|
126 |
apply (induct_tac "evs") |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
127 |
apply (rule_tac x = 0 in exI) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
128 |
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
|
129 |
apply safe |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
130 |
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
|
131 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
132 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
133 |
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
|
134 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
135 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
136 |
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
|
137 |
apply (rule Nonce_supply_lemma [THEN exE]) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
138 |
apply (rule someI, fast) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
139 |
done |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
140 |
|
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 |
(*** Specialized rewriting for the analz_image_... theorems ***) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
143 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
144 |
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
|
145 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
146 |
|
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
147 |
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
|
148 |
by blast |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
149 |
|
11250 | 150 |
|
151 |
(*Specialized methods*) |
|
152 |
||
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
153 |
(*Tactic for possibility theorems*) |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
154 |
ML {* |
30608 | 155 |
fun possibility_tac ctxt = |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
156 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
30608
diff
changeset
|
157 |
(ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says])) |
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
158 |
THEN |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
159 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
160 |
resolve_tac [refl, conjI, @{thm Nonce_supply}])); |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
161 |
*} |
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
162 |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30548
diff
changeset
|
163 |
method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *} |
11250 | 164 |
"for proving possibility theorems" |
165 |
||
166 |
end |
|
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
16417
diff
changeset
|
167 |
(*>*) |