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