src/HOL/Auth/Smartcard/EventSC.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 26302 68b073052e8c
child 32960 69916a850301
permissions -rw-r--r--
generalize tendsto to class topological_space
     1 header{*Theory of Events for Security Protocols that use smartcards*}
     2 
     3 theory EventSC imports "../Message" begin
     4 
     5 consts  (*Initial states of agents -- parameter of the construction*)
     6   initState :: "agent => msg set"
     7 
     8 datatype card = Card agent
     9 
    10 text{*Four new events express the traffic between an agent and his card*}
    11 datatype  
    12   event = Says  agent agent msg
    13         | Notes agent       msg
    14         | Gets  agent       msg
    15         | Inputs agent card msg (*Agent sends to card and\<dots>*)
    16         | C_Gets card       msg (*\<dots> card receives it*) 
    17         | Outpts card agent msg (*Card sends to agent and\<dots>*)
    18         | A_Gets agent      msg (*agent receives it*)
    19     
    20 consts 
    21  bad     :: "agent set"  (*compromised agents*)
    22  knows   :: "agent => event list => msg set" (*agents' knowledge*)
    23  stolen    :: "card set" (* stolen smart cards *)
    24  cloned  :: "card set"   (* cloned smart cards*)
    25  secureM :: "bool"(*assumption of secure means between agents and their cards*)
    26 
    27 abbreviation
    28   insecureM :: bool where (*certain protocols make no assumption of secure means*)
    29   "insecureM == \<not>secureM"
    30 
    31 
    32 text{*Spy has access to his own key for spoof messages, but Server is secure*}
    33 specification (bad)
    34   Spy_in_bad     [iff]: "Spy \<in> bad"
    35   Server_not_bad [iff]: "Server \<notin> bad"
    36   apply (rule exI [of _ "{Spy}"], simp) done
    37 
    38 specification (stolen)
    39   (*The server's card is secure by assumption\<dots>*)
    40   Card_Server_not_stolen [iff]: "Card Server \<notin> stolen"
    41   Card_Spy_not_stolen  	 [iff]: "Card Spy \<notin> stolen"
    42   apply blast done
    43 
    44 specification (cloned)
    45   (*\<dots> the spy's card is secure because she already can use it freely*)
    46   Card_Server_not_cloned [iff]: "Card Server \<notin> cloned"
    47   Card_Spy_not_cloned  	 [iff]: "Card Spy \<notin> cloned"
    48   apply blast done
    49 
    50 
    51 primrec (*This definition is extended over the new events, subject to the 
    52           assumption of secure means*)
    53   knows_Nil:   "knows A [] = initState A"
    54   knows_Cons:  "knows A (ev # evs) =
    55 	 (case ev of
    56 	    Says A' B X => 
    57                 if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs
    58 	  | Notes A' X  => 
    59 	        if (A=A' | (A=Spy & A'\<in>bad)) then insert X (knows A evs) 
    60                                              else knows A evs 
    61           | Gets A' X   =>
    62 		if (A=A' & A \<noteq> Spy) then insert X (knows A evs) 
    63                                      else knows A evs
    64           | Inputs A' C X =>
    65 	      if secureM then
    66                 if A=A' then insert X (knows A evs) else knows A evs
    67 	      else
    68 	        if (A=A' | A=Spy) then insert X (knows A evs) else knows A evs
    69           | C_Gets C X   => knows A evs
    70           | Outpts C A' X =>
    71 	      if secureM then
    72                 if A=A' then insert X (knows A evs) else knows A evs
    73               else
    74 	        if A=Spy then insert X (knows A evs) else knows A evs
    75           | A_Gets A' X   =>
    76 		if (A=A' & A \<noteq> Spy) then insert X (knows A evs) 
    77                                      else knows A evs)"
    78 
    79 
    80 
    81 consts
    82   (*The set of items that might be visible to someone is easily extended 
    83     over the new events*)
    84   used :: "event list => msg set"
    85 
    86 primrec
    87   used_Nil:   "used []         = (UN B. parts (initState B))"
    88   used_Cons:  "used (ev # evs) =
    89 	         (case ev of
    90 		    Says A B X => parts {X} \<union> (used evs)
    91 		  | Notes A X  => parts {X} \<union> (used evs)
    92 		  | Gets A X   => used evs
    93                   | Inputs A C X  => parts{X} \<union> (used evs) 
    94 		  | C_Gets C X   => used evs
    95                   | Outpts C A X  => parts{X} \<union> (used evs)
    96 		  | A_Gets A X   => used evs)"
    97     --{*@{term Gets} always follows @{term Says} in real protocols. 
    98        Likewise, @{term C_Gets} will always have to follow @{term Inputs}
    99        and @{term A_Gets} will always have to follow @{term Outpts}*}
   100 
   101 
   102 lemma Notes_imp_used [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> used evs"
   103 apply (induct_tac evs)
   104 apply (auto split: event.split) 
   105 done
   106 
   107 lemma Says_imp_used [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> used evs"
   108 apply (induct_tac evs)
   109 apply (auto split: event.split) 
   110 done
   111 
   112 lemma MPair_used [rule_format]:
   113      "MPair X Y \<in> used evs \<longrightarrow> X \<in> used evs & Y \<in> used evs"
   114 apply (induct_tac evs)
   115 apply (auto split: event.split) 
   116 done
   117 
   118 
   119 subsection{*Function @{term knows}*}
   120 
   121 (*Simplifying   
   122  parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
   123   This version won't loop with the simplifier.*)
   124 lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
   125 
   126 lemma knows_Spy_Says [simp]:
   127      "knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
   128 by simp
   129 
   130 text{*Letting the Spy see "bad" agents' notes avoids redundant case-splits
   131       on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*}
   132 lemma knows_Spy_Notes [simp]:
   133      "knows Spy (Notes A X # evs) =  
   134           (if A\<in>bad then insert X (knows Spy evs) else knows Spy evs)"
   135 by simp
   136 
   137 lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs"
   138 by simp
   139 
   140 lemma knows_Spy_Inputs_secureM [simp]: 
   141      "secureM \<Longrightarrow> knows Spy (Inputs A C X # evs) =  
   142         (if A=Spy then insert X (knows Spy evs) else knows Spy evs)"
   143 by simp
   144 
   145 lemma knows_Spy_Inputs_insecureM [simp]: 
   146      "insecureM \<Longrightarrow> knows Spy (Inputs A C X # evs) = insert X (knows Spy evs)"
   147 by simp
   148 
   149 lemma knows_Spy_C_Gets [simp]: "knows Spy (C_Gets C X # evs) = knows Spy evs"
   150 by simp
   151 
   152 lemma knows_Spy_Outpts_secureM [simp]: 
   153       "secureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = 
   154          (if A=Spy then insert X (knows Spy evs) else knows Spy evs)"
   155 by simp
   156 
   157 lemma knows_Spy_Outpts_insecureM [simp]: 
   158       "insecureM \<Longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)"
   159 by simp
   160 
   161 lemma knows_Spy_A_Gets [simp]: "knows Spy (A_Gets A X # evs) = knows Spy evs"
   162 by simp
   163 
   164 
   165 
   166 
   167 lemma knows_Spy_subset_knows_Spy_Says:
   168      "knows Spy evs \<subseteq> knows Spy (Says A B X # evs)"
   169 by (simp add: subset_insertI)
   170 
   171 lemma knows_Spy_subset_knows_Spy_Notes:
   172      "knows Spy evs \<subseteq> knows Spy (Notes A X # evs)"
   173 by force
   174 
   175 lemma knows_Spy_subset_knows_Spy_Gets:
   176      "knows Spy evs \<subseteq> knows Spy (Gets A X # evs)"
   177 by (simp add: subset_insertI)
   178 
   179 lemma knows_Spy_subset_knows_Spy_Inputs: 
   180      "knows Spy evs \<subseteq> knows Spy (Inputs A C X # evs)"
   181 by auto
   182 
   183 lemma knows_Spy_equals_knows_Spy_Gets: 
   184      "knows Spy evs = knows Spy (C_Gets C X # evs)"
   185 by (simp add: subset_insertI)
   186 
   187 lemma knows_Spy_subset_knows_Spy_Outpts: "knows Spy evs \<subseteq> knows Spy (Outpts C A X # evs)"
   188 by auto
   189 
   190 lemma knows_Spy_subset_knows_Spy_A_Gets: "knows Spy evs \<subseteq> knows Spy (A_Gets A X # evs)"
   191 by (simp add: subset_insertI)
   192 
   193 
   194 
   195 text{*Spy sees what is sent on the traffic*}
   196 lemma Says_imp_knows_Spy [rule_format]:
   197      "Says A B X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
   198 apply (induct_tac "evs")
   199 apply (simp_all (no_asm_simp) split add: event.split)
   200 done
   201 
   202 lemma Notes_imp_knows_Spy [rule_format]:
   203      "Notes A X \<in> set evs \<longrightarrow> A\<in> bad \<longrightarrow> X \<in> knows Spy evs"
   204 apply (induct_tac "evs")
   205 apply (simp_all (no_asm_simp) split add: event.split)
   206 done
   207 
   208 (*Nothing can be stated on a Gets event*)
   209 
   210 lemma Inputs_imp_knows_Spy_secureM [rule_format (no_asm)]: 
   211      "Inputs Spy C X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
   212 apply (induct_tac "evs")
   213 apply (simp_all (no_asm_simp) split add: event.split)
   214 done
   215 
   216 lemma Inputs_imp_knows_Spy_insecureM [rule_format (no_asm)]:
   217      "Inputs A C X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
   218 apply (induct_tac "evs")
   219 apply (simp_all (no_asm_simp) split add: event.split)
   220 done
   221 
   222 (*Nothing can be stated on a C_Gets event*)
   223 
   224 lemma Outpts_imp_knows_Spy_secureM [rule_format (no_asm)]: 
   225      "Outpts C Spy X \<in> set evs \<longrightarrow> secureM \<longrightarrow> X \<in> knows Spy evs"
   226 apply (induct_tac "evs")
   227 apply (simp_all (no_asm_simp) split add: event.split)
   228 done
   229 
   230 lemma Outpts_imp_knows_Spy_insecureM [rule_format (no_asm)]:
   231      "Outpts C A X \<in> set evs \<longrightarrow> insecureM \<longrightarrow> X \<in> knows Spy evs"
   232 apply (induct_tac "evs")
   233 apply (simp_all (no_asm_simp) split add: event.split)
   234 done
   235 
   236 (*Nothing can be stated on an A_Gets event*)
   237 
   238 
   239 
   240 text{*Elimination rules: derive contradictions from old Says events containing
   241   items known to be fresh*}
   242 lemmas knows_Spy_partsEs =
   243      Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] 
   244      parts.Body [THEN revcut_rl, standard]
   245 
   246 
   247 
   248 subsection{*Knowledge of Agents*}
   249 
   250 lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
   251 by simp
   252 
   253 lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
   254 by simp
   255 
   256 lemma knows_Gets:
   257       "A \<noteq> Spy \<longrightarrow> knows A (Gets A X # evs) = insert X (knows A evs)"
   258 by simp
   259 
   260 lemma knows_Inputs: "knows A (Inputs A C X # evs) = insert X (knows A evs)"
   261 by simp
   262 
   263 lemma knows_C_Gets: "knows A (C_Gets C X # evs) = knows A evs"
   264 by simp
   265 
   266 lemma knows_Outpts_secureM: 
   267       "secureM \<longrightarrow> knows A (Outpts C A X # evs) = insert X (knows A evs)"
   268 by simp
   269 
   270 lemma knows_Outpts_insecureM: 
   271       "insecureM \<longrightarrow> knows Spy (Outpts C A X # evs) = insert X (knows Spy evs)"
   272 by simp
   273 (*somewhat equivalent to knows_Spy_Outpts_insecureM*)
   274 
   275 
   276 
   277 
   278 lemma knows_subset_knows_Says: "knows A evs \<subseteq> knows A (Says A' B X # evs)"
   279 by (simp add: subset_insertI)
   280 
   281 lemma knows_subset_knows_Notes: "knows A evs \<subseteq> knows A (Notes A' X # evs)"
   282 by (simp add: subset_insertI)
   283 
   284 lemma knows_subset_knows_Gets: "knows A evs \<subseteq> knows A (Gets A' X # evs)"
   285 by (simp add: subset_insertI)
   286 
   287 lemma knows_subset_knows_Inputs: "knows A evs \<subseteq> knows A (Inputs A' C X # evs)"
   288 by (simp add: subset_insertI)
   289 
   290 lemma knows_subset_knows_C_Gets: "knows A evs \<subseteq> knows A (C_Gets C X # evs)"
   291 by (simp add: subset_insertI)
   292 
   293 lemma knows_subset_knows_Outpts: "knows A evs \<subseteq> knows A (Outpts C A' X # evs)"
   294 by (simp add: subset_insertI)
   295 
   296 lemma knows_subset_knows_A_Gets: "knows A evs \<subseteq> knows A (A_Gets A' X # evs)"
   297 by (simp add: subset_insertI)
   298 
   299 
   300 text{*Agents know what they say*}
   301 lemma Says_imp_knows [rule_format]: "Says A B X \<in> set evs \<longrightarrow> X \<in> knows A evs"
   302 apply (induct_tac "evs")
   303 apply (simp_all (no_asm_simp) split add: event.split)
   304 apply blast
   305 done
   306 
   307 text{*Agents know what they note*}
   308 lemma Notes_imp_knows [rule_format]: "Notes A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
   309 apply (induct_tac "evs")
   310 apply (simp_all (no_asm_simp) split add: event.split)
   311 apply blast
   312 done
   313 
   314 text{*Agents know what they receive*}
   315 lemma Gets_imp_knows_agents [rule_format]:
   316      "A \<noteq> Spy \<longrightarrow> Gets A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
   317 apply (induct_tac "evs")
   318 apply (simp_all (no_asm_simp) split add: event.split)
   319 done
   320 
   321 (*Agents know what they input to their smart card*)
   322 lemma Inputs_imp_knows_agents [rule_format (no_asm)]: 
   323      "Inputs A (Card A) X \<in> set evs \<longrightarrow> X \<in> knows A evs"
   324 apply (induct_tac "evs")
   325 apply (simp_all (no_asm_simp) split add: event.split)
   326 apply blast
   327 done
   328 
   329 (*Nothing to prove about C_Gets*)
   330 
   331 (*Agents know what they obtain as output of their smart card,
   332   if the means is secure...*)
   333 lemma Outpts_imp_knows_agents_secureM [rule_format (no_asm)]: 
   334      "secureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows A evs"
   335 apply (induct_tac "evs")
   336 apply (simp_all (no_asm_simp) split add: event.split)
   337 done
   338 
   339 (*otherwise only the spy knows the outputs*)
   340 lemma Outpts_imp_knows_agents_insecureM [rule_format (no_asm)]: 
   341       "insecureM \<longrightarrow> Outpts (Card A) A X \<in> set evs \<longrightarrow> X \<in> knows Spy evs"
   342 apply (induct_tac "evs")
   343 apply (simp_all (no_asm_simp) split add: event.split)
   344 done
   345 
   346 (*end lemmas about agents' knowledge*)
   347 
   348 
   349 
   350 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \<subseteq> used evs"
   351 apply (induct_tac "evs", force)  
   352 apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) 
   353 done
   354 
   355 lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro]
   356 
   357 lemma initState_into_used: "X \<in> parts (initState B) \<Longrightarrow> X \<in> used evs"
   358 apply (induct_tac "evs")
   359 apply (simp_all add: parts_insert_knows_A split add: event.split, blast)
   360 done
   361 
   362 lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \<union> used evs"
   363 by simp
   364 
   365 lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} \<union> used evs"
   366 by simp
   367 
   368 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
   369 by simp
   370 
   371 lemma used_Inputs [simp]: "used (Inputs A C X # evs) = parts{X} \<union> used evs"
   372 by simp
   373 
   374 lemma used_C_Gets [simp]: "used (C_Gets C X # evs) = used evs"
   375 by simp
   376 
   377 lemma used_Outpts [simp]: "used (Outpts C A X # evs) = parts{X} \<union> used evs"
   378 by simp
   379 
   380 lemma used_A_Gets [simp]: "used (A_Gets A X # evs) = used evs"
   381 by simp
   382 
   383 lemma used_nil_subset: "used [] \<subseteq> used evs"
   384 apply simp
   385 apply (blast intro: initState_into_used)
   386 done
   387 
   388 
   389 
   390 (*Novel lemmas*)
   391 lemma Says_parts_used [rule_format (no_asm)]: 
   392      "Says A B X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   393 apply (induct_tac "evs")
   394 apply (simp_all (no_asm_simp) split add: event.split)
   395 apply blast
   396 done
   397 
   398 lemma Notes_parts_used [rule_format (no_asm)]: 
   399      "Notes A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   400 apply (induct_tac "evs")
   401 apply (simp_all (no_asm_simp) split add: event.split)
   402 apply blast
   403 done
   404 
   405 lemma Outpts_parts_used [rule_format (no_asm)]: 
   406      "Outpts C A X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   407 apply (induct_tac "evs")
   408 apply (simp_all (no_asm_simp) split add: event.split)
   409 apply blast
   410 done
   411 
   412 lemma Inputs_parts_used [rule_format (no_asm)]: 
   413      "Inputs A C X \<in> set evs \<longrightarrow> (parts  {X}) \<subseteq> used evs"
   414 apply (induct_tac "evs")
   415 apply (simp_all (no_asm_simp) split add: event.split)
   416 apply blast
   417 done
   418 
   419 
   420 
   421 
   422 text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*}
   423 declare knows_Cons [simp del]
   424         used_Nil [simp del] used_Cons [simp del]
   425 
   426 
   427 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   428 by (induct e, auto simp: knows_Cons)
   429 
   430 lemma initState_subset_knows: "initState A \<subseteq> knows A evs"
   431 apply (induct_tac evs, simp) 
   432 apply (blast intro: knows_subset_knows_Cons [THEN subsetD])
   433 done
   434 
   435 
   436 text{*For proving @{text new_keys_not_used}*}
   437 lemma keysFor_parts_insert:
   438      "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk>   
   439       \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H"; 
   440 by (force 
   441     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   442            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
   443     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
   444 
   445 end