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