src/HOL/Auth/Event.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 32404 da3ca3c6ec81
child 37936 1e4c5015a72e
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  Title:      HOL/Auth/Event
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Datatype of events; function "spies"; freshness
     7 
     8 "bad" agents have been broken by the Spy; their private keys and internal
     9     stores are visible to him
    10 *)
    11 
    12 header{*Theory of Events for Security Protocols*}
    13 
    14 theory Event imports Message begin
    15 
    16 consts  (*Initial states of agents -- parameter of the construction*)
    17   initState :: "agent => msg set"
    18 
    19 datatype
    20   event = Says  agent agent msg
    21         | Gets  agent       msg
    22         | Notes agent       msg
    23        
    24 consts 
    25   bad    :: "agent set"                         -- {* compromised agents *}
    26   knows  :: "agent => event list => msg set"
    27 
    28 
    29 text{*The constant "spies" is retained for compatibility's sake*}
    30 
    31 abbreviation (input)
    32   spies  :: "event list => msg set" where
    33   "spies == knows Spy"
    34 
    35 text{*Spy has access to his own key for spoof messages, but Server is secure*}
    36 specification (bad)
    37   Spy_in_bad     [iff]: "Spy \<in> bad"
    38   Server_not_bad [iff]: "Server \<notin> bad"
    39     by (rule exI [of _ "{Spy}"], simp)
    40 
    41 primrec
    42   knows_Nil:   "knows A [] = initState A"
    43   knows_Cons:
    44     "knows A (ev # evs) =
    45        (if A = Spy then 
    46         (case ev of
    47            Says A' B X => insert X (knows Spy evs)
    48          | Gets A' X => knows Spy evs
    49          | Notes A' X  => 
    50              if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
    51         else
    52         (case ev of
    53            Says A' B X => 
    54              if A'=A then insert X (knows A evs) else knows A evs
    55          | Gets A' X    => 
    56              if A'=A then insert X (knows A evs) else knows A evs
    57          | Notes A' X    => 
    58              if A'=A then insert X (knows A evs) else knows A evs))"
    59 
    60 (*
    61   Case A=Spy on the Gets event
    62   enforces the fact that if a message is received then it must have been sent,
    63   therefore the oops case must use Notes
    64 *)
    65 
    66 consts
    67   (*Set of items that might be visible to somebody:
    68     complement of the set of fresh items*)
    69   used :: "event list => msg set"
    70 
    71 primrec
    72   used_Nil:   "used []         = (UN B. parts (initState B))"
    73   used_Cons:  "used (ev # evs) =
    74                      (case ev of
    75                         Says A B X => parts {X} \<union> used evs
    76                       | Gets A X   => used evs
    77                       | Notes A X  => parts {X} \<union> used evs)"
    78     --{*The case for @{term Gets} seems anomalous, but @{term Gets} always
    79         follows @{term Says} in real protocols.  Seems difficult to change.
    80         See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}
    81 
    82 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs --> X \<in> used evs"
    83 apply (induct_tac evs)
    84 apply (auto split: event.split) 
    85 done
    86 
    87 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs --> X \<in> used evs"
    88 apply (induct_tac evs)
    89 apply (auto split: event.split) 
    90 done
    91 
    92 
    93 subsection{*Function @{term knows}*}
    94 
    95 (*Simplifying   
    96  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
    97   This version won't loop with the simplifier.*)
    98 lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
    99 
   100 lemma knows_Spy_Says [simp]:
   101      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
   102 by simp
   103 
   104 text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
   105       on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
   106 lemma knows_Spy_Notes [simp]:
   107      "knows Spy (Notes A X # evs) =  
   108           (if A:bad then insert X (knows Spy evs) else knows Spy evs)"
   109 by simp
   110 
   111 lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
   112 by simp
   113 
   114 lemma knows_Spy_subset_knows_Spy_Says:
   115      "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
   116 by (simp add: subset_insertI)
   117 
   118 lemma knows_Spy_subset_knows_Spy_Notes:
   119      "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
   120 by force
   121 
   122 lemma knows_Spy_subset_knows_Spy_Gets:
   123      "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
   124 by (simp add: subset_insertI)
   125 
   126 text{*Spy sees what is sent on the traffic*}
   127 lemma Says_imp_knows_Spy [rule_format]:
   128      "Says A B X \<in> set evs --> X \<in> knows Spy evs"
   129 apply (induct_tac "evs")
   130 apply (simp_all (no_asm_simp) split add: event.split)
   131 done
   132 
   133 lemma Notes_imp_knows_Spy [rule_format]:
   134      "Notes A X \<in> set evs --> A: bad --> X \<in> knows Spy evs"
   135 apply (induct_tac "evs")
   136 apply (simp_all (no_asm_simp) split add: event.split)
   137 done
   138 
   139 
   140 text{*Elimination rules: derive contradictions from old Says events containing
   141   items known to be fresh*}
   142 lemmas Says_imp_parts_knows_Spy = 
   143        Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   144 
   145 lemmas knows_Spy_partsEs =
   146      Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
   147 
   148 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
   149 
   150 text{*Compatibility for the old "spies" function*}
   151 lemmas spies_partsEs = knows_Spy_partsEs
   152 lemmas Says_imp_spies = Says_imp_knows_Spy
   153 lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy]
   154 
   155 
   156 subsection{*Knowledge of Agents*}
   157 
   158 lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
   159 by simp
   160 
   161 lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
   162 by simp
   163 
   164 lemma knows_Gets:
   165      "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
   166 by simp
   167 
   168 
   169 lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
   170 by (simp add: subset_insertI)
   171 
   172 lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
   173 by (simp add: subset_insertI)
   174 
   175 lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
   176 by (simp add: subset_insertI)
   177 
   178 text{*Agents know what they say*}
   179 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs --> X \<in> knows A evs"
   180 apply (induct_tac "evs")
   181 apply (simp_all (no_asm_simp) split add: event.split)
   182 apply blast
   183 done
   184 
   185 text{*Agents know what they note*}
   186 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs --> X \<in> knows A evs"
   187 apply (induct_tac "evs")
   188 apply (simp_all (no_asm_simp) split add: event.split)
   189 apply blast
   190 done
   191 
   192 text{*Agents know what they receive*}
   193 lemma Gets_imp_knows_agents [rule_format]:
   194      "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
   195 apply (induct_tac "evs")
   196 apply (simp_all (no_asm_simp) split add: event.split)
   197 done
   198 
   199 
   200 text{*What agents DIFFERENT FROM Spy know 
   201   was either said, or noted, or got, or known initially*}
   202 lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
   203      "[| X \<in> knows A evs; A \<noteq> Spy |] ==> EX B.  
   204   Says A B X \<in> set evs | Gets A X \<in> set evs | Notes A X \<in> set evs | X \<in> initState A"
   205 apply (erule rev_mp)
   206 apply (induct_tac "evs")
   207 apply (simp_all (no_asm_simp) split add: event.split)
   208 apply blast
   209 done
   210 
   211 text{*What the Spy knows -- for the time being --
   212   was either said or noted, or known initially*}
   213 lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
   214      "[| X \<in> knows Spy evs |] ==> EX A B.  
   215   Says A B X \<in> set evs | Notes A X \<in> set evs | X \<in> initState Spy"
   216 apply (erule rev_mp)
   217 apply (induct_tac "evs")
   218 apply (simp_all (no_asm_simp) split add: event.split)
   219 apply blast
   220 done
   221 
   222 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
   223 apply (induct_tac "evs", force)  
   224 apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
   225 done
   226 
   227 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   228 
   229 lemma initState_into_used: "X \<in> parts (initState B) ==> X \<in> used evs"
   230 apply (induct_tac "evs")
   231 apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
   232 done
   233 
   234 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
   235 by simp
   236 
   237 lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
   238 by simp
   239 
   240 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   241 by simp
   242 
   243 lemma used_nil_subset: "used [] \<subseteq> used evs"
   244 apply simp
   245 apply (blast intro: initState_into_used)
   246 done
   247 
   248 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   249 declare knows_Cons [simp del]
   250         used_Nil [simp del] used_Cons [simp del]
   251 
   252 
   253 text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) --> P"}
   254   New events added by induction to "evs" are discarded.  Provided 
   255   this information isn't needed, the proof will be much shorter, since
   256   it will omit complicated reasoning about @{term analz}.*}
   257 
   258 lemmas analz_mono_contra =
   259        knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
   260        knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
   261        knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
   262 
   263 
   264 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   265 by (induct e, auto simp: knows_Cons)
   266 
   267 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
   268 apply (induct_tac evs, simp) 
   269 apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   270 done
   271 
   272 
   273 text{*For proving @{text new_keys_not_used}*}
   274 lemma keysFor_parts_insert:
   275      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
   276       ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
   277 by (force 
   278     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   279            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
   280     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
   281 
   282 
   283 lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
   284 
   285 ML
   286 {*
   287 val analz_mono_contra_tac = 
   288   rtac @{thm analz_impI} THEN' 
   289   REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
   290   THEN' mp_tac
   291 *}
   292 
   293 method_setup analz_mono_contra = {*
   294     Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
   295     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   296 
   297 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
   298 
   299 lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
   300 
   301 ML
   302 {*
   303 val synth_analz_mono_contra_tac = 
   304   rtac @{thm syan_impI} THEN'
   305   REPEAT1 o 
   306     (dresolve_tac 
   307      [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
   308       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
   309       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   310   THEN'
   311   mp_tac
   312 *}
   313 
   314 method_setup synth_analz_mono_contra = {*
   315     Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
   316     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
   317 
   318 end