1 (* Title: Doc/Tutorial/Protocol/Public.thy
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Copyright 1996 University of Cambridge
5 Theory of Public Keys (common to all public-key protocols)
7 Private and public keys; initial states of agents
9 theory Public imports Event
15 @{text pubK} maps agents to their public keys. The function
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}.
21 consts pubK :: "agent \<Rightarrow> key"
22 abbreviation priK :: "agent \<Rightarrow> key"
23 where "priK x \<equiv> invKey(pubK x)"
25 overloading initState \<equiv> initState
28 primrec initState where
29 (*Agents know their private key and all public keys*)
30 initState_Server: "initState Server =
31 insert (Key (priK Server)) (Key ` range pubK)"
32 | initState_Friend: "initState (Friend i) =
33 insert (Key (priK (Friend i))) (Key ` range pubK)"
34 | initState_Spy: "initState Spy =
35 (Key`invKey`pubK`bad) Un (Key ` range pubK)"
42 The set @{text bad} consists of those agents whose private keys are known to
45 Two axioms are asserted about the public-key cryptosystem.
46 No two agents have the same public key, and no private key equals
51 inj_pubK: "inj pubK" and
52 priK_neq_pubK: "priK A \<noteq> pubK B"
54 lemmas [iff] = inj_pubK [THEN inj_eq]
56 lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
58 apply (drule_tac f=invKey in arg_cong)
62 lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]
64 lemma not_symKeys_pubK[iff]: "pubK A \<notin> symKeys"
65 by (simp add: symKeys_def)
67 lemma not_symKeys_priK[iff]: "priK A \<notin> symKeys"
68 by (simp add: symKeys_def)
70 lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'"
73 lemma analz_symKeys_Decrypt: "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |]
75 by (auto simp add: symKeys_def)
78 (** "Image" equations that hold for injective functions **)
80 lemma invKey_image_eq[simp]: "(invKey x : invKey`A) = (x:A)"
83 (*holds because invKey is injective*)
84 lemma pubK_image_eq[simp]: "(pubK x : pubK`A) = (x:A)"
87 lemma priK_pubK_image_eq[simp]: "(priK x ~: pubK`A)"
91 (** Rewrites should not refer to initState(Friend i)
92 -- not in normal form! **)
94 lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
95 apply (unfold keysFor_def)
97 apply (auto intro: range_eqI)
101 (*** Function "spies" ***)
103 (*Agents see their own private keys!*)
104 lemma priK_in_initState[iff]: "Key (priK A) : initState A"
107 (*All public keys are visible*)
108 lemma spies_pubK[iff]: "Key (pubK A) : spies evs"
109 by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
111 (*Spy sees private keys of bad agents!*)
112 lemma Spy_spies_bad[intro!]: "A: bad ==> Key (priK A) : spies evs"
113 by (induct evs) (simp_all add: imageI knows_Cons split: event.split)
115 lemmas [iff] = spies_pubK [THEN analz.Inj]
118 (*** Fresh nonces ***)
120 lemma Nonce_notin_initState[iff]: "Nonce N ~: parts (initState B)"
123 lemma Nonce_notin_used_empty[simp]: "Nonce N ~: used []"
124 by (simp add: used_Nil)
127 (*** Supply fresh nonces for possibility theorems. ***)
129 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
130 lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs"
131 apply (induct_tac "evs")
132 apply (rule_tac x = 0 in exI)
133 apply (simp_all (no_asm_simp) add: used_Cons split add: event.split)
135 apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
138 lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs"
139 by (rule Nonce_supply_lemma [THEN exE], blast)
141 lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs"
142 apply (rule Nonce_supply_lemma [THEN exE])
143 apply (rule someI, fast)
147 (*** Specialized rewriting for the analz_image_... theorems ***)
149 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
152 lemma insert_Key_image: "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
156 (*Specialized methods*)
158 (*Tactic for possibility theorems*)
160 fun possibility_tac ctxt =
161 REPEAT (*omit used_Says so that Nonces start from different traces!*)
162 (ALLGOALS (simp_tac (ctxt delsimps [used_Says]))
164 REPEAT_FIRST (eq_assume_tac ORELSE'
165 resolve_tac [refl, conjI, @{thm Nonce_supply}]));
168 method_setup possibility = {* Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
169 "for proving possibility theorems"