Quelle  Public.thy

(*  Title:      Doc/Tutorial/Protocol/Public.thy
  Author: Lawrence C Paulson, Cambridge University Computer Laboratory
  Copyright 1996 University of Cambridge
 
 Theory of Public Keys (common to all public-key protocols)
 
 Private and public keys; initial states of agents
*)
theory Public imports Event
begin
(*>*)

text ‹
 The function
 ‹pubK› m
‹priK› maps agents to their private keys.  It is merely
an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
‹invKey› and ‹pubK›.
›

consts pubK :: "agent ==> key"
abbreviation priK :: "agent ==> key"
where "priK x ≡ invKey(pubK x)"
(*<*)
overloading initState ≡ initState
begin

primrec initState where
        (*Agents know their private key and all public keys*)
  initState_Server:  "initState Server =
                         insert (Key (priK Server)) (Key ` range pubK)"
| initState_Friend:  "initState (Friend i) =
                         insert (Key (priK (Friend i))) (Key ` range pubK)"
| initState_Spy:     "initState Spy =
                         (Key`invKey`pubK`bad) ∪ (Key ` range pubK)"

end
(*>*)

text ‹
 \noindent
 The set ‹bad› c
the spy.

Two axioms are asserted about the public-key cryptosystem. 
No two agents have the same public key, and no private key equals
any public key.
›

axiomatization where
  inj_pubK:        "inj pubK" and
  priK_neq_pubK:   "priK A ≠ pubK B"
(*<*)
lemmas [iff] = inj_pubK [THEN inj_eq]

lemma priK_inj_eq[iff]: "(priK A = priK B) = (A=B)"
  apply safe
  apply (drule_tac f=invKey in arg_cong)
  apply simp
  done

lemmas [iff] = priK_neq_pubK priK_neq_pubK [THEN not_sym]

lemma not_symKeys_pubK[iff]: "pubK A ∉ symKeys"
  by (simp add: symKeys_def)

lemma not_symKeys_priK[iff]: "priK A ∉ symKeys"
  by (simp add: symKeys_def)

lemma symKeys_neq_imp_neq: "(K ∈ symKeys) ≠ (K' ∈ symKeys) ==> K ≠ K'"
  by blast

lemma analz_symKeys_Decrypt: "[| Crypt K X ∈ analz H; K ∈ symKeys; Key K ∈ analz H |]
     ==> X ∈ analz H"
  by (auto simp add: symKeys_def)


(** "Image" equations that hold for injective functions **)

lemma invKey_image_eq[simp]: "(invKey x ∈ invKey`A) = (x∈A)"
  by auto

(*holds because invKey is injective*)
lemma pubK_image_eq[simp]: "(pubK x ∈ pubK`A) = (x∈A)"
  by auto

lemma priK_pubK_image_eq[simp]: "(priK x ∉ pubK`A)"
  by auto


(** Rewrites should not refer to  initState(Friend i) 
    -- not in normal form! **)

lemma keysFor_parts_initState[simp]: "keysFor (parts (initState C)) = {}"
  apply (unfold keysFor_def)
  apply (induct C)
  apply (auto intro: range_eqI)
  done


(*** Function "spies" ***)

(*Agents see their own private keys!*)
lemma priK_in_initState[iff]: "Key (priK A) ∈ initState A"
  by (induct A) auto

(*All public keys are visible*)
lemma spies_pubK[iff]: "Key (pubK A) ∈ spies evs"
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)

(*Spy sees private keys of bad agents!*)
lemma Spy_spies_bad[intro!]: "A ∈ bad ==> Key (priK A) ∈ spies evs"
  by (induct evs) (simp_all add: imageI knows_Cons split: event.split)

lemmas [iff] = spies_pubK [THEN analz.Inj]


(*** Fresh nonces ***)

lemma Nonce_notin_initState[iff]: "Nonce N ∉ parts (initState B)"
  by (induct B) auto

lemma Nonce_notin_used_empty[simp]: "Nonce N ∉ used []"
  by (simp add: used_Nil)


(*** Supply fresh nonces for possibility theorems. ***)

(*In any trace, there is an upper bound N on the greatest nonce in use.*)
lemma Nonce_supply_lemma: "∃N. ∀n. N≤n ⟶ Nonce n ∉ used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done

lemma Nonce_supply1: "∃N. Nonce N ∉ used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)

lemma Nonce_supply: "Nonce (SOME N. Nonce N ∉ used evs) ∉ used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)
done


(*** Specialized rewriting for the analz_image_... theorems ***)

lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} ∪ H"
  by blast

lemma insert_Key_image: "insert (Key K) (Key`KK ∪ C) = Key ` (insert K KK) ∪ C"
  by blast


(*Specialized methods*)

(*Tactic for possibility theorems*)
ML ‹
 fun possibility_tac ctxt =
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
    (ALLGOALS (simp_tac (ctxt delsimps [used_Says]))
     THEN
     REPEAT_FIRST (eq_assume_tac ORELSE' 
                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]));
›

method_setup possibility = ‹Scan.succeed (SIMPLE_METHOD o possibility_tac)›
    "for proving possibility theorems"

end
(*>*)