1.1 --- a/doc-src/TutorialI/Protocol/Public.thy Mon Jul 23 14:30:53 2007 +0200
1.2 +++ b/doc-src/TutorialI/Protocol/Public.thy Mon Jul 23 14:31:34 2007 +0200
1.3 @@ -6,20 +6,24 @@
1.4 Theory of Public Keys (common to all public-key protocols)
1.5
1.6 Private and public keys; initial states of agents
1.7 -*)
1.8 +*)(*<*)
1.9 +theory Public imports Event
1.10 +begin
1.11 +(*>*)
1.12
1.13 -theory Public imports Event
1.14 -uses ("Public_lemmas.ML") begin
1.15 +text {*
1.16 +The function
1.17 +@{text pubK} maps agents to their public keys. The function
1.18 +@{text priK} maps agents to their private keys. It is defined in terms of
1.19 +@{text invKey} and @{text pubK} by a translation; therefore @{text priK} is
1.20 +not a proper constant, so we declare it using \isacommand{syntax}
1.21 +(cf.\ \S\ref{sec:syntax-translations}).
1.22 +*}
1.23
1.24 -consts
1.25 - pubK :: "agent => key"
1.26 -
1.27 -syntax
1.28 - priK :: "agent => key"
1.29 -
1.30 -translations (*BEWARE! expressions like (inj priK) will NOT work!*)
1.31 - "priK x" == "invKey(pubK x)"
1.32 -
1.33 +consts pubK :: "agent => key"
1.34 +syntax priK :: "agent => key"
1.35 +translations "priK x" \<rightleftharpoons> "invKey(pubK x)"
1.36 +(*<*)
1.37 primrec
1.38 (*Agents know their private key and all public keys*)
1.39 initState_Server: "initState Server =
1.40 @@ -28,19 +32,139 @@
1.41 insert (Key (priK (Friend i))) (Key ` range pubK)"
1.42 initState_Spy: "initState Spy =
1.43 (Key`invKey`pubK`bad) Un (Key ` range pubK)"
1.44 +(*>*)
1.45
1.46 +text {*
1.47 +\noindent
1.48 +The set @{text bad} consists of those agents whose private keys are known to
1.49 +the spy.
1.50 +
1.51 +Two axioms are asserted about the public-key cryptosystem.
1.52 +No two agents have the same public key, and no private key equals
1.53 +any public key.
1.54 +*}
1.55
1.56 axioms
1.57 - (*Public keys are disjoint, and never clash with private keys*)
1.58 inj_pubK: "inj pubK"
1.59 priK_neq_pubK: "priK A ~= pubK B"
1.60 +(*<*)
1.61 +lemmas [iff] = inj_pubK [THEN inj_eq]
1.62
1.63 -use "Public_lemmas.ML"
1.64 +lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
1.65 + apply safe
1.66 + apply (drule_tac f=invKey in arg_cong)
1.67 + apply simp
1.68 + done
1.69 +
1.70 +lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]
1.71 +
1.72 +lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys"
1.73 + by (simp add: symKeys_def)
1.74 +
1.75 +lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
1.76 + by (simp add: symKeys_def)
1.77 +
1.78 +lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
1.79 + by blast
1.80 +
1.81 +lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
1.82 + ==> X \<in> analz H"
1.83 + by (auto simp add: symKeys_def)
1.84 +
1.85 +
1.86 +(** "Image" equations that hold for injective functions **)
1.87 +
1.88 +lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)"
1.89 + by auto
1.90 +
1.91 +(*holds because invKey is injective*)
1.92 +lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)"
1.93 + by auto
1.94 +
1.95 +lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)"
1.96 + by auto
1.97 +
1.98 +
1.99 +(** Rewrites should not refer to initState(Friend i)
1.100 + -- not in normal form! **)
1.101 +
1.102 +lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
1.103 + apply (unfold keysFor_def)
1.104 + apply (induct C)
1.105 + apply (auto intro: range_eqI)
1.106 + done
1.107 +
1.108 +
1.109 +(*** Function "spies" ***)
1.110 +
1.111 +(*Agents see their own private keys!*)
1.112 +lemma priK_in_initState[iff]: "Key (priK A) : initState A"
1.113 + by (induct A) auto
1.114 +
1.115 +(*All public keys are visible*)
1.116 +lemma spies_pubK[iff]: "Key (pubK A) : spies evs"
1.117 + by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
1.118 +
1.119 +(*Spy sees private keys of bad agents!*)
1.120 +lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs"
1.121 + by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
1.122 +
1.123 +lemmas [iff] = spies_pubK [THEN analz.Inj]
1.124 +
1.125 +
1.126 +(*** Fresh nonces ***)
1.127 +
1.128 +lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)"
1.129 + by (induct B) auto
1.130 +
1.131 +lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []"
1.132 + by (simp add: used_Nil)
1.133 +
1.134 +
1.135 +(*** Supply fresh nonces for possibility theorems. ***)
1.136 +
1.137 +(*In any trace, there is an upper bound N on the greatest nonce in use.*)
1.138 +lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
1.139 +apply (induct_tac "evs")
1.140 +apply (rule_tac x = 0 in exI)
1.141 +apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
1.142 +apply safe
1.143 +apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
1.144 +done
1.145 +
1.146 +lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
1.147 +by (rule Nonce_supply_lemma [THEN exE], blast)
1.148 +
1.149 +lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
1.150 +apply (rule Nonce_supply_lemma [THEN exE])
1.151 +apply (rule someI, fast)
1.152 +done
1.153 +
1.154 +
1.155 +(*** Specialized rewriting for the analz_image_... theorems ***)
1.156 +
1.157 +lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
1.158 + by blast
1.159 +
1.160 +lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
1.161 + by blast
1.162 +
1.163
1.164 (*Specialized methods*)
1.165
1.166 +(*Tactic for possibility theorems*)
1.167 +ML {*
1.168 +fun possibility_tac st = st |>
1.169 + REPEAT (*omit used_Says so that Nonces start from different traces!*)
1.170 + (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
1.171 + THEN
1.172 + REPEAT_FIRST (eq_assume_tac ORELSE'
1.173 + resolve_tac [refl, conjI, @{thm Nonce_supply}]));
1.174 +*}
1.175 +
1.176 method_setup possibility = {*
1.177 Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
1.178 "for proving possibility theorems"
1.179
1.180 end
1.181 +(*>*)
1.182 \ No newline at end of file