src/HOL/Auth/Smartcard/ShoupRubinBella.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 30549 d2d7874648bd
child 32149 ef59550a55d3
permissions -rw-r--r--
generalize tendsto to class topological_space
     1 (*  ID:         $Id$
     2     Author:     Giampaolo Bella, Catania University
     3 *)
     4 
     5 header{*Bella's modification of the Shoup-Rubin protocol*}
     6 
     7 theory ShoupRubinBella imports Smartcard begin
     8 
     9 text{*The modifications are that message 7 now mentions A, while message 10
    10 now mentions Nb and B. The lack of explicitness of the original version was
    11 discovered by investigating adherence to the principle of Goal
    12 Availability. Only the updated version makes the goals of confidentiality,
    13 authentication and key distribution available to both peers.*}
    14 
    15 consts
    16 
    17     sesK :: "nat*key => key"
    18 
    19 axioms
    20      
    21    (*sesK is injective on each component*) 
    22    inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
    23 
    24    (*all long-term keys differ from sesK*)
    25    shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
    26    crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
    27    pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)"
    28    pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
    29 
    30    (*needed for base case in analz_image_freshK*)
    31    Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
    32                    Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" 
    33 
    34   (*this protocol makes the assumption of secure means
    35     between each agent and his smartcard*)
    36    shouprubin_assumes_securemeans [iff]: "evs \<in> srb \<Longrightarrow> secureM"
    37 
    38 constdefs
    39 
    40   Unique :: "[event, event list] => bool" ("Unique _ on _")
    41    "Unique ev on evs == 
    42       ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
    43 
    44 
    45 inductive_set srb :: "event list set"
    46   where
    47 
    48     Nil:  "[]\<in> srb"
    49 
    50 
    51 
    52   | Fake: "\<lbrakk> evsF \<in> srb;  X \<in> synth (analz (knows Spy evsF)); 
    53              illegalUse(Card B) \<rbrakk>
    54           \<Longrightarrow> Says Spy A X # 
    55               Inputs Spy (Card B) X # evsF \<in> srb"
    56 
    57 (*In general this rule causes the assumption Card B \<notin> cloned
    58   in most guarantees for B - starting with confidentiality -
    59   otherwise pairK_confidential could not apply*)
    60   | Forge:
    61          "\<lbrakk> evsFo \<in> srb; Nonce Nb \<in> analz (knows Spy evsFo);
    62              Key (pairK(A,B)) \<in> knows Spy evsFo \<rbrakk>
    63           \<Longrightarrow> Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \<in> srb"
    64 
    65 
    66 
    67   | Reception: "\<lbrakk> evsrb\<in> srb; Says A B X \<in> set evsrb \<rbrakk>
    68               \<Longrightarrow> Gets B X # evsrb \<in> srb"
    69 
    70 
    71 
    72 (*A AND THE SERVER*)
    73   | SR_U1:  "\<lbrakk> evs1 \<in> srb; A \<noteq> Server \<rbrakk>
    74           \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> 
    75                 # evs1 \<in> srb"
    76 
    77   | SR_U2:  "\<lbrakk> evs2 \<in> srb; 
    78              Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
    79           \<Longrightarrow> Says Server A \<lbrace>Nonce (Pairkey(A,B)), 
    80                            Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>
    81                   \<rbrace>
    82                 # evs2 \<in> srb"
    83 
    84 
    85 
    86 
    87 (*A AND HER CARD*)
    88 (*A cannot decrypt the verifier for she dosn't know shrK A,
    89   but the pairkey is recognisable*)
    90   | SR_U3:  "\<lbrakk> evs3 \<in> srb; legalUse(Card A);
    91              Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
    92              Gets A \<lbrace>Nonce Pk, Certificate\<rbrace> \<in> set evs3 \<rbrakk>
    93           \<Longrightarrow> Inputs A (Card A) (Agent A)
    94                 # evs3 \<in> srb"   (*however A only queries her card 
    95 if she has previously contacted the server to initiate with some B. 
    96 Otherwise she would do so even if the Server had not been active. 
    97 Still, this doesn't and can't mean that the pairkey originated with 
    98 the server*)
    99  
   100 (*The card outputs the nonce Na to A*)               
   101   | SR_U4:  "\<lbrakk> evs4 \<in> srb; 
   102              Nonce Na \<notin> used evs4; legalUse(Card A); A \<noteq> Server;
   103              Inputs A (Card A) (Agent A) \<in> set evs4 \<rbrakk> 
   104        \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
   105               # evs4 \<in> srb"
   106 
   107 (*The card can be exploited by the spy*)
   108 (*because of the assumptions on the card, A is certainly not server nor spy*)
   109   | SR_U4Fake: "\<lbrakk> evs4F \<in> srb; Nonce Na \<notin> used evs4F; 
   110              illegalUse(Card A);
   111              Inputs Spy (Card A) (Agent A) \<in> set evs4F \<rbrakk> 
   112       \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
   113             # evs4F \<in> srb"
   114 
   115 
   116 
   117 
   118 (*A TOWARDS B*)
   119   | SR_U5:  "\<lbrakk> evs5 \<in> srb; 
   120              Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs5;
   121              \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
   122           \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> # evs5 \<in> srb"
   123 (*A must check that the verifier is not a compound message, 
   124   otherwise this would also fire after SR_U7 *)
   125 
   126 
   127 
   128 
   129 (*B AND HIS CARD*)
   130   | SR_U6:  "\<lbrakk> evs6 \<in> srb; legalUse(Card B);
   131              Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs6 \<rbrakk>
   132           \<Longrightarrow> Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> 
   133                 # evs6 \<in> srb"
   134 (*B gets back from the card the session key and various verifiers*)
   135   | SR_U7:  "\<lbrakk> evs7 \<in> srb; 
   136              Nonce Nb \<notin> used evs7; legalUse(Card B); B \<noteq> Server;
   137              K = sesK(Nb,pairK(A,B));
   138              Key K \<notin> used evs7;
   139              Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7\<rbrakk>
   140     \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,
   141                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   142                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> 
   143                 # evs7 \<in> srb"
   144 (*The card can be exploited by the spy*)
   145 (*because of the assumptions on the card, A is certainly not server nor spy*)
   146   | SR_U7Fake:  "\<lbrakk> evs7F \<in> srb; Nonce Nb \<notin> used evs7F; 
   147              illegalUse(Card B);
   148              K = sesK(Nb,pairK(A,B));
   149              Key K \<notin> used evs7F;
   150              Inputs Spy (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7F \<rbrakk>
   151           \<Longrightarrow> Outpts (Card B) Spy \<lbrace>Nonce Nb, Agent A, Key K,
   152                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   153                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> 
   154                 # evs7F \<in> srb"
   155 
   156 
   157 
   158 
   159 (*B TOWARDS A*)
   160 (*having sent an input that mentions A is the only memory B relies on,
   161   since the output doesn't mention A - lack of explicitness*) 
   162   | SR_U8:  "\<lbrakk> evs8 \<in> srb;  
   163              Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs8;
   164              Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, 
   165                                  Cert1, Cert2\<rbrace> \<in> set evs8 \<rbrakk>
   166           \<Longrightarrow> Says B A \<lbrace>Nonce Nb, Cert1\<rbrace> # evs8 \<in> srb"
   167   
   168 
   169 
   170 
   171 (*A AND HER CARD*)
   172 (*A cannot check the form of the verifiers - although I can prove the form of
   173   Cert2 - and just feeds her card with what she's got*)
   174   | SR_U9:  "\<lbrakk> evs9 \<in> srb; legalUse(Card A);
   175              Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs9;
   176              Outpts (Card A) A \<lbrace>Nonce Na, Cert2\<rbrace> \<in> set evs9; 
   177              Gets A \<lbrace>Nonce Nb, Cert3\<rbrace> \<in> set evs9;
   178              \<forall> p q. Cert2 \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
   179           \<Longrightarrow> Inputs A (Card A) 
   180                  \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
   181                   Cert1, Cert3, Cert2\<rbrace> 
   182                 # evs9 \<in> srb"
   183 (*But the card will only give outputs to the inputs of the correct form*)
   184   | SR_U10: "\<lbrakk> evs10 \<in> srb; legalUse(Card A); A \<noteq> Server;
   185              K = sesK(Nb,pairK(A,B));
   186              Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, 
   187                                  Nonce (Pairkey(A,B)),
   188                                  Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), 
   189                                                    Agent B\<rbrace>,
   190                                  Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   191                                  Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
   192                \<in> set evs10 \<rbrakk>
   193           \<Longrightarrow> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
   194                                  Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
   195                  # evs10 \<in> srb"
   196 (*The card can be exploited by the spy*)
   197 (*because of the assumptions on the card, A is certainly not server nor spy*)
   198   | SR_U10Fake: "\<lbrakk> evs10F \<in> srb; 
   199              illegalUse(Card A);
   200              K = sesK(Nb,pairK(A,B));
   201              Inputs Spy (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, 
   202                                    Nonce (Pairkey(A,B)),
   203                                    Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), 
   204                                                     Agent B\<rbrace>,
   205                                    Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   206                                    Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
   207                \<in> set evs10F \<rbrakk>
   208           \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Agent B, Nonce Nb, 
   209                                    Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
   210                  # evs10F \<in> srb"
   211 
   212 
   213 
   214 
   215 (*A TOWARDS B*)
   216 (*having initiated with B is the only memory A relies on,
   217   since the output doesn't mention B - lack of explicitness*) 
   218   | SR_U11: "\<lbrakk> evs11 \<in> srb;
   219              Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs11;
   220              Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
   221                \<in> set evs11 \<rbrakk>
   222           \<Longrightarrow> Says A B (Certificate) 
   223                  # evs11 \<in> srb"
   224 
   225 
   226 
   227 (*Both peers may leak by accident the session keys obtained from their
   228   cards*)
   229   | Oops1:
   230      "\<lbrakk> evsO1 \<in> srb;
   231          Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
   232            \<in> set evsO1 \<rbrakk>
   233      \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO1 \<in> srb"
   234 
   235   | Oops2:
   236      "\<lbrakk> evsO2 \<in> srb;
   237          Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
   238            \<in> set evsO2 \<rbrakk>
   239     \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO2 \<in> srb"
   240 
   241 
   242 
   243 
   244 
   245 
   246 (*To solve Fake case when it doesn't involve analz - used to be condensed
   247   into Fake_parts_insert_tac*)
   248 declare Fake_parts_insert_in_Un  [dest]
   249 declare analz_into_parts [dest]
   250 (*declare parts_insertI [intro]*)
   251 
   252 
   253 
   254 (*General facts about message reception*)
   255 lemma Gets_imp_Says: 
   256        "\<lbrakk> Gets B X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> \<exists> A. Says A B X \<in> set evs"
   257 apply (erule rev_mp, erule srb.induct)
   258 apply auto
   259 done
   260 
   261 lemma Gets_imp_knows_Spy: 
   262      "\<lbrakk> Gets B X \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
   263 apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   264 done
   265 
   266 lemma Gets_imp_knows_Spy_parts_Snd: 
   267      "\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> Y \<in> parts (knows Spy evs)"
   268 apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy parts.Inj parts.Snd)
   269 done
   270 
   271 lemma Gets_imp_knows_Spy_analz_Snd: 
   272      "\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> Y \<in> analz (knows Spy evs)"
   273 apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy analz.Inj analz.Snd)
   274 done
   275 
   276 (*end general facts*)
   277 
   278 
   279 
   280 (*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help
   281   the simplifier, especially in analz_image_freshK*)
   282 
   283 
   284 lemma Inputs_imp_knows_Spy_secureM_srb: 
   285       "\<lbrakk> Inputs Spy C X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs"
   286 apply (simp (no_asm_simp) add: Inputs_imp_knows_Spy_secureM)
   287 done
   288 
   289 lemma knows_Spy_Inputs_secureM_srb_Spy: 
   290       "evs \<in>srb \<Longrightarrow> knows Spy (Inputs Spy C X # evs) = insert X (knows Spy evs)"
   291 apply (simp (no_asm_simp))
   292 done
   293 
   294 lemma knows_Spy_Inputs_secureM_srb: 
   295     "\<lbrakk> A \<noteq> Spy; evs \<in>srb \<rbrakk> \<Longrightarrow> knows Spy (Inputs A C X # evs) =  knows Spy evs"
   296 apply (simp (no_asm_simp))
   297 done
   298 
   299 lemma knows_Spy_Outpts_secureM_srb_Spy: 
   300       "evs \<in>srb \<Longrightarrow> knows Spy (Outpts C Spy X # evs) = insert X (knows Spy evs)"
   301 apply (simp (no_asm_simp))
   302 done
   303 
   304 lemma knows_Spy_Outpts_secureM_srb: 
   305      "\<lbrakk> A \<noteq> Spy; evs \<in>srb \<rbrakk> \<Longrightarrow> knows Spy (Outpts C A X # evs) =  knows Spy evs"
   306 apply (simp (no_asm_simp))
   307 done
   308 
   309 (*End lemmas on secure means for shouprubin*)
   310 
   311 
   312 
   313 
   314 (*BEGIN technical lemmas - evolution of forwarding lemmas*)
   315 
   316 (*If an honest agent uses a smart card, then the card is his/her own, is
   317   not stolen, and the agent has received suitable data to feed the card. 
   318   In other words, these are guarantees that an honest agent can only use 
   319   his/her own card, and must use it correctly.
   320   On the contrary, the spy can "Inputs" any cloned cards also by the Fake rule.
   321 
   322   Instead of Auto_tac, proofs here used to asm-simplify and then force-tac.
   323 *)
   324 lemma Inputs_A_Card_3: 
   325     "\<lbrakk> Inputs A C (Agent A) \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   326      \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   327       (\<exists> Pk Certificate. Gets A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs)"
   328 apply (erule rev_mp, erule srb.induct)
   329 apply auto
   330 done
   331 
   332 lemma Inputs_B_Card_6: 
   333      "\<lbrakk> Inputs B C \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; B \<noteq> Spy; evs \<in> srb \<rbrakk>  
   334       \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
   335 apply (erule rev_mp, erule srb.induct)
   336 apply auto
   337 done
   338 
   339 lemma Inputs_A_Card_9: 
   340      "\<lbrakk> Inputs A C \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
   341                                            Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
   342          A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   343   \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   344       Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs     \<and>  
   345       Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace> \<in> set evs        \<and>   
   346       Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
   347 apply (erule rev_mp, erule srb.induct)
   348 apply auto
   349 done
   350 
   351 
   352 (*The two occurrences of A in the Outpts event don't match SR_U4Fake, where
   353   A cannot be the Spy. Hence the card is legally usable by rule SR_U4*)
   354 lemma Outpts_A_Card_4: 
   355      "\<lbrakk> Outpts C A \<lbrace>Nonce Na, (Crypt (crdK (Card A)) (Nonce Na))\<rbrace> \<in> set evs;  
   356          evs \<in> srb \<rbrakk>  
   357      \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   358          Inputs A (Card A) (Agent A) \<in> set evs"
   359 apply (erule rev_mp, erule srb.induct)
   360 apply auto
   361 done
   362 
   363 
   364 (*First certificate is made explicit so that a comment similar to the previous
   365   applies. This also provides Na to the Inputs event in the conclusion*)
   366 lemma Outpts_B_Card_7: 
   367       "\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Agent A, Key K,  
   368                       Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
   369                       Cert2\<rbrace> \<in> set evs;  
   370          evs \<in> srb \<rbrakk>  
   371      \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>  
   372          Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
   373 apply (erule rev_mp, erule srb.induct)
   374 apply auto
   375 done
   376 
   377 lemma Outpts_A_Card_10: 
   378      "\<lbrakk> Outpts C A \<lbrace>Agent B, Nonce Nb, 
   379                     Key K, (Crypt (pairK(A,B)) (Nonce Nb))\<rbrace> \<in> set evs; 
   380          evs \<in> srb \<rbrakk>  
   381      \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   382          (\<exists> Na Ver1 Ver2 Ver3.  
   383        Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
   384                               Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
   385 apply (erule rev_mp, erule srb.induct)
   386 apply auto
   387 done
   388 
   389 
   390 
   391 (*
   392 Contrarily to original version, A doesn't need to check the form of the 
   393 certificate to learn that her peer is B. The goal is available to A.
   394 *)
   395 lemma Outpts_A_Card_10_imp_Inputs: 
   396      "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
   397           \<in> set evs; evs \<in> srb \<rbrakk>  
   398      \<Longrightarrow> (\<exists> Na Ver1 Ver2 Ver3.  
   399        Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
   400                               Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
   401 apply (erule rev_mp, erule srb.induct)
   402 apply simp_all
   403 apply blast+
   404 done
   405 
   406 
   407 
   408 
   409 (*Weaker version: if the agent can't check the forms of the verifiers, then
   410   the agent must not be the spy so as to solve SR_U4Fake. The verifier must be
   411   recognised as some cyphertex in order to distinguish from case SR_U7, 
   412   concerning B's output, which also begins with a nonce.
   413 *)
   414 lemma Outpts_honest_A_Card_4: 
   415      "\<lbrakk> Outpts C A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in>set evs; 
   416          A \<noteq> Spy;  evs \<in> srb \<rbrakk>  
   417      \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   418          Inputs A (Card A) (Agent A) \<in> set evs"
   419 apply (erule rev_mp, erule srb.induct)
   420 apply auto
   421 done
   422 
   423 (*alternative formulation of same theorem
   424 Goal "\<lbrakk> Outpts C A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;  
   425          \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;    
   426          A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   427      \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
   428          Inputs A (Card A) (Agent A) \<in> set evs"
   429 same proof
   430 *)
   431 
   432 
   433 lemma Outpts_honest_B_Card_7: 
   434     "\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;  
   435        B \<noteq> Spy; evs \<in> srb \<rbrakk>  
   436    \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>  
   437        (\<exists> Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs)"
   438 apply (erule rev_mp, erule srb.induct)
   439 apply auto
   440 done
   441 
   442 lemma Outpts_honest_A_Card_10: 
   443      "\<lbrakk> Outpts C A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;  
   444          A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   445      \<Longrightarrow> legalUse (C) \<and> C = (Card A) \<and>  
   446          (\<exists> Na Pk Ver1 Ver2 Ver3.  
   447           Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Pk,  
   448                               Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
   449 apply (erule rev_mp, erule srb.induct)
   450 apply simp_all
   451 apply blast+
   452 done
   453 (*-END-*)
   454 
   455 
   456 (*Even weaker versions: if the agent can't check the forms of the verifiers
   457   and the agent may be the spy, then we must know what card the agent
   458   is getting the output from. 
   459 *)
   460 lemma Outpts_which_Card_4: 
   461     "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
   462     \<Longrightarrow> Inputs A (Card A) (Agent A) \<in> set evs"
   463 apply (erule rev_mp, erule srb.induct)
   464 apply (simp_all (no_asm_simp))
   465 apply clarify
   466 done
   467 
   468 lemma Outpts_which_Card_7: 
   469   "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
   470        \<in> set evs;  evs \<in> srb \<rbrakk>  
   471      \<Longrightarrow> \<exists> Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
   472 apply (erule rev_mp, erule srb.induct)
   473 apply auto
   474 done
   475 
   476 (*This goal is now available - in the sense of Goal Availability*)
   477 lemma Outpts_which_Card_10: 
   478     "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate \<rbrace> \<in> set evs;
   479        evs \<in> srb \<rbrakk>  
   480     \<Longrightarrow> \<exists> Na. Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), 
   481                             Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>,  
   482                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
   483                             Crypt (crdK (Card A)) (Nonce Na) \<rbrace> \<in> set evs"
   484 apply (erule rev_mp, erule srb.induct)
   485 apply auto
   486 done
   487 
   488 
   489 (*Lemmas on the form of outputs*)
   490 
   491 
   492 (*A needs to check that the verifier is a cipher for it to come from SR_U4
   493   otherwise it could come from SR_U7 *)
   494 lemma Outpts_A_Card_form_4: 
   495   "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;  
   496          \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>; evs \<in> srb \<rbrakk>  
   497      \<Longrightarrow> Certificate = (Crypt (crdK (Card A)) (Nonce Na))"
   498 apply (erule rev_mp, erule srb.induct)
   499 apply (simp_all (no_asm_simp))
   500 done
   501 
   502 lemma Outpts_B_Card_form_7: 
   503    "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
   504         \<in> set evs; evs \<in> srb \<rbrakk>          
   505       \<Longrightarrow> \<exists> Na.    
   506           K = sesK(Nb,pairK(A,B)) \<and>                       
   507           Cert1 = (Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>) \<and>  
   508           Cert2 = (Crypt (pairK(A,B)) (Nonce Nb))"
   509 apply (erule rev_mp, erule srb.induct)
   510 apply auto
   511 done
   512 
   513 lemma Outpts_A_Card_form_10: 
   514    "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
   515         \<in> set evs; evs \<in> srb \<rbrakk>  
   516       \<Longrightarrow> K = sesK(Nb,pairK(A,B)) \<and>  
   517           Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
   518 apply (erule rev_mp, erule srb.induct)
   519 apply (simp_all (no_asm_simp))
   520 done
   521 
   522 lemma Outpts_A_Card_form_bis: 
   523   "\<lbrakk> Outpts (Card A') A' \<lbrace>Agent B', Nonce Nb', Key (sesK(Nb,pairK(A,B))), 
   524      Certificate\<rbrace> \<in> set evs; 
   525          evs \<in> srb \<rbrakk>  
   526       \<Longrightarrow> A' = A \<and> B' = B \<and> Nb = Nb' \<and>  
   527           Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
   528 apply (erule rev_mp, erule srb.induct)
   529 apply (simp_all (no_asm_simp))
   530 done
   531 
   532 (*\<dots> and Inputs *)
   533 
   534 lemma Inputs_A_Card_form_9: 
   535 
   536      "\<lbrakk> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
   537                              Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
   538          evs \<in> srb \<rbrakk>  
   539   \<Longrightarrow>    Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
   540 apply (erule rev_mp)
   541 apply (erule srb.induct)
   542 apply (simp_all (no_asm_simp))
   543 (*Fake*)
   544 apply force
   545 (*SR_U9*)
   546 apply (blast dest!: Outpts_A_Card_form_4)
   547 done
   548 (* Pk, Cert1, Cert2 cannot be made explicit because they traversed the network in the clear *)
   549 
   550 
   551 
   552 (*General guarantees on Inputs and Outpts*)
   553 
   554 (*for any agents*)
   555 
   556 
   557 lemma Inputs_Card_legalUse: 
   558   "\<lbrakk> Inputs A (Card A) X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> legalUse(Card A)"
   559 apply (erule rev_mp, erule srb.induct)
   560 apply auto
   561 done
   562 
   563 lemma Outpts_Card_legalUse: 
   564   "\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> legalUse(Card A)"
   565 apply (erule rev_mp, erule srb.induct)
   566 apply auto
   567 done
   568 
   569 (*for honest agents*)
   570 
   571 lemma Inputs_Card: "\<lbrakk> Inputs A C X \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   572       \<Longrightarrow> C = (Card A) \<and> legalUse(C)"
   573 apply (erule rev_mp, erule srb.induct)
   574 apply auto
   575 done
   576 
   577 lemma Outpts_Card: "\<lbrakk> Outpts C A X \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   578       \<Longrightarrow> C = (Card A) \<and> legalUse(C)"
   579 apply (erule rev_mp, erule srb.induct)
   580 apply auto
   581 done
   582 
   583 lemma Inputs_Outpts_Card: 
   584      "\<lbrakk> Inputs A C X \<in> set evs \<or> Outpts C A Y \<in> set evs;  
   585          A \<noteq> Spy; evs \<in> srb \<rbrakk>  
   586      \<Longrightarrow> C = (Card A) \<and> legalUse(Card A)"
   587 apply (blast dest: Inputs_Card Outpts_Card)
   588 done
   589 
   590 
   591 (*for the spy - they stress that the model behaves as it is meant to*) 
   592 
   593 (*The or version can be also proved directly.
   594   It stresses that the spy may use either her own legally usable card or
   595   all the illegally usable cards.
   596 *)
   597 lemma Inputs_Card_Spy: 
   598   "\<lbrakk> Inputs Spy C X \<in> set evs \<or> Outpts C Spy X \<in> set evs; evs \<in> srb \<rbrakk>  
   599       \<Longrightarrow> C = (Card Spy) \<and> legalUse(Card Spy) \<or>  
   600           (\<exists> A. C = (Card A) \<and> illegalUse(Card A))"
   601 apply (erule rev_mp, erule srb.induct)
   602 apply auto
   603 done
   604 
   605 
   606 (*END technical lemmas*)
   607 
   608 
   609 
   610 
   611 
   612 
   613 (*BEGIN unicity theorems: certain items uniquely identify a smart card's
   614                           output*)
   615 
   616 (*A's card's first output: the nonce uniquely identifies the rest*)
   617 lemma Outpts_A_Card_unique_nonce:
   618      "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>  
   619            \<in> set evs;   
   620          Outpts (Card A') A' \<lbrace>Nonce Na, Crypt (crdK (Card A')) (Nonce Na)\<rbrace> 
   621            \<in> set evs;   
   622          evs \<in> srb \<rbrakk> \<Longrightarrow> A=A'"
   623 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
   624 apply (fastsimp dest: Outpts_parts_used)
   625 apply blast
   626 done
   627 
   628 (*B's card's output: the NONCE uniquely identifies the rest*)
   629 lemma Outpts_B_Card_unique_nonce: 
   630      "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;   
   631       Outpts (Card B') B' \<lbrace>Nonce Nb, Agent A', Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;
   632        evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
   633 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
   634 apply (fastsimp dest: Outpts_parts_used)
   635 apply blast
   636 done
   637 
   638 
   639 (*B's card's output: the SESKEY uniquely identifies the rest*)
   640 lemma Outpts_B_Card_unique_key: 
   641      "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;   
   642       Outpts (Card B') B' \<lbrace>Nonce Nb', Agent A', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs; 
   643        evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
   644 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
   645 apply (fastsimp dest: Outpts_parts_used)
   646 apply blast
   647 done
   648 
   649 lemma Outpts_A_Card_unique_key: 
   650    "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, V\<rbrace> \<in> set evs;   
   651       Outpts (Card A') A' \<lbrace>Agent B', Nonce Nb', Key K, V'\<rbrace> \<in> set evs;   
   652          evs \<in> srb \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> Nb=Nb' \<and> V=V'"
   653 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
   654 apply (blast dest: Outpts_A_Card_form_bis)
   655 apply blast
   656 done
   657 
   658 
   659 (*Revised unicity theorem - applies to both steps 4 and 7*)
   660 lemma Outpts_A_Card_Unique: 
   661   "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
   662      \<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
   663 apply (erule rev_mp, erule srb.induct, simp_all add: Unique_def)
   664 apply (fastsimp dest: Outpts_parts_used)
   665 apply blast
   666 apply (fastsimp dest: Outpts_parts_used)
   667 apply blast
   668 done
   669 
   670 (*can't prove the same on evs10 for it doesn't have a freshness assumption!*)
   671 
   672 
   673 (*END unicity theorems*)
   674 
   675 
   676 (*BEGIN counterguarantees about spy's knowledge*)
   677 
   678 (*on nonces*)
   679 
   680 lemma Spy_knows_Na: 
   681       "\<lbrakk> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
   682       \<Longrightarrow> Nonce Na \<in> analz (knows Spy evs)"
   683 apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
   684 done
   685 
   686 lemma Spy_knows_Nb: 
   687       "\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
   688       \<Longrightarrow> Nonce Nb \<in> analz (knows Spy evs)"
   689 apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst])
   690 done
   691 
   692 
   693 (*on Pairkey*)
   694 
   695 lemma Pairkey_Gets_analz_knows_Spy: 
   696       "\<lbrakk> Gets A \<lbrace>Nonce (Pairkey(A,B)), Certificate\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
   697       \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
   698 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   699 done
   700 
   701 lemma Pairkey_Inputs_imp_Gets: 
   702      "\<lbrakk> Inputs A (Card A)             
   703            \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
   704              Cert1, Cert3, Cert2\<rbrace> \<in> set evs;           
   705          A \<noteq> Spy; evs \<in> srb \<rbrakk>     
   706       \<Longrightarrow> Gets A \<lbrace>Nonce (Pairkey(A,B)), Cert1\<rbrace> \<in> set evs"
   707 apply (erule rev_mp, erule srb.induct)
   708 apply (simp_all (no_asm_simp))
   709 apply force
   710 done
   711 
   712 lemma Pairkey_Inputs_analz_knows_Spy: 
   713      "\<lbrakk> Inputs A (Card A)             
   714            \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
   715              Cert1, Cert3, Cert2\<rbrace> \<in> set evs;           
   716          evs \<in> srb \<rbrakk>     
   717      \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
   718 apply (case_tac "A = Spy")
   719 apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
   720 apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
   721 done
   722 
   723 (* This fails on base case because of XOR properties.
   724 lemma Pairkey_authentic:
   725   "\<lbrakk> Nonce (Pairkey(A,B)) \<in> parts (knows Spy evs);
   726      Card A \<notin> cloned; evs \<in> sr \<rbrakk>
   727  \<Longrightarrow> \<exists> cert. Says Server A \<lbrace>Nonce (Pairkey(A,B)), Cert\<rbrace> \<in> set evs"
   728 apply (erule rev_mp)
   729 apply (erule sr.induct, simp_all)
   730 apply clarify
   731 oops
   732 
   733  1. \<And>x a b.
   734        \<lbrakk>Card A \<notin> cloned; Pairkey (A, B) = Pairkey (a, b); Card a \<in> cloned;
   735         Card b \<in> cloned\<rbrakk>
   736        \<Longrightarrow> False
   737 *)
   738 
   739 
   740 (*END counterguarantees on spy's knowledge*)
   741 
   742 
   743 (*BEGIN rewrite rules for parts operator*)
   744 
   745 declare shrK_disj_sesK [THEN not_sym, iff] 
   746 declare pin_disj_sesK [THEN not_sym, iff]
   747 declare crdK_disj_sesK [THEN not_sym, iff]
   748 declare pairK_disj_sesK [THEN not_sym, iff]
   749 
   750 
   751 ML
   752 {*
   753 structure ShoupRubinBella =
   754 struct
   755 
   756 fun prepare_tac ctxt = 
   757  (*SR_U8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
   758  (*SR_U8*)   clarify_tac (local_claset_of ctxt) 15 THEN
   759  (*SR_U9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
   760  (*SR_U11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 
   761 
   762 fun parts_prepare_tac ctxt = 
   763            prepare_tac ctxt THEN
   764  (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
   765  (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
   766  (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
   767  (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
   768  (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
   769 
   770 fun analz_prepare_tac ctxt = 
   771          prepare_tac ctxt THEN
   772          dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
   773  (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
   774          REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
   775 
   776 end
   777 *}
   778 
   779 method_setup prepare = {*
   780     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
   781   "to launch a few simple facts that'll help the simplifier"
   782 
   783 method_setup parts_prepare = {*
   784     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   785   "additional facts to reason about parts"
   786 
   787 method_setup analz_prepare = {*
   788     Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   789   "additional facts to reason about analz"
   790 
   791 
   792 
   793 lemma Spy_parts_keys [simp]: "evs \<in> srb \<Longrightarrow>  
   794   (Key (shrK P) \<in> parts (knows Spy evs)) = (Card P \<in> cloned) \<and>  
   795   (Key (pin P) \<in> parts (knows Spy evs)) = (P \<in> bad \<or> Card P \<in> cloned) \<and>  
   796   (Key (crdK C) \<in> parts (knows Spy evs)) = (C \<in> cloned) \<and>  
   797   (Key (pairK(A,B)) \<in> parts (knows Spy evs)) = (Card B \<in> cloned)"
   798 apply (erule srb.induct)
   799 apply parts_prepare
   800 apply simp_all
   801 apply (blast intro: parts_insertI)
   802 done
   803 
   804 (*END rewrite rules for parts operator*)
   805 
   806 (*BEGIN rewrite rules for analz operator*)
   807 
   808 
   809 lemma Spy_analz_shrK[simp]: "evs \<in> srb \<Longrightarrow>  
   810   (Key (shrK P) \<in> analz (knows Spy evs)) = (Card P \<in> cloned)"
   811 apply (auto dest!: Spy_knows_cloned)
   812 done
   813 
   814 lemma Spy_analz_crdK[simp]: "evs \<in> srb \<Longrightarrow>  
   815   (Key (crdK C) \<in> analz (knows Spy evs)) = (C \<in> cloned)"
   816 apply (auto dest!: Spy_knows_cloned)
   817 done
   818 
   819 lemma Spy_analz_pairK[simp]: "evs \<in> srb \<Longrightarrow>  
   820   (Key (pairK(A,B)) \<in> analz (knows Spy evs)) = (Card B \<in> cloned)"
   821 apply (auto dest!: Spy_knows_cloned)
   822 done
   823 
   824 
   825 
   826 
   827 (*Because initState contains a set of nonces, this is needed for base case of
   828   analz_image_freshK*)
   829 lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
   830 apply auto
   831 done
   832 
   833 method_setup sc_analz_freshK = {*
   834     Scan.succeed (fn ctxt =>
   835      (SIMPLE_METHOD
   836       (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   837           REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   838           ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
   839               addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
   840                   @{thm knows_Spy_Outpts_secureM_srb_Spy},
   841                   @{thm shouprubin_assumes_securemeans},
   842                   @{thm analz_image_Key_Un_Nonce}]))]))) *}
   843     "for proving the Session Key Compromise theorem for smartcard protocols"
   844 
   845 
   846 lemma analz_image_freshK [rule_format]: 
   847      "evs \<in> srb \<Longrightarrow>      \<forall> K KK.  
   848           (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) =  
   849           (K \<in> KK \<or> Key K \<in> analz (knows Spy evs))"
   850 apply (erule srb.induct)
   851 apply analz_prepare
   852 apply sc_analz_freshK
   853 apply spy_analz
   854 done
   855 
   856 
   857 lemma analz_insert_freshK: "evs \<in> srb \<Longrightarrow>   
   858          Key K \<in> analz (insert (Key K') (knows Spy evs)) =  
   859          (K = K' \<or> Key K \<in> analz (knows Spy evs))"
   860 apply (simp only: analz_image_freshK_simps analz_image_freshK)
   861 done
   862 
   863 (*END rewrite rules for analz operator*)
   864 
   865 (*BEGIN authenticity theorems*)
   866 
   867 
   868 
   869 
   870 lemma Na_Nb_certificate_authentic: 
   871      "\<lbrakk> Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs);  
   872          \<not>illegalUse(Card B); 
   873          evs \<in> srb \<rbrakk>           
   874      \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
   875                 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   876                 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
   877 apply (erule rev_mp, erule srb.induct)
   878 apply parts_prepare
   879 apply simp_all
   880 (*Fake*)
   881 apply spy_analz
   882 (*SR_U7F*)
   883 apply clarify
   884 (*SR_U8*)
   885 apply clarify
   886 done
   887 
   888 lemma Nb_certificate_authentic:
   889       "\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);  
   890          B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
   891          evs \<in> srb \<rbrakk>    
   892      \<Longrightarrow> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key (sesK(Nb,pairK(A,B))),  
   893                              Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
   894 apply (erule rev_mp, erule srb.induct)
   895 apply parts_prepare
   896 apply (case_tac [17] "Aa = Spy")
   897 apply simp_all
   898 (*Fake*)
   899 apply spy_analz
   900 (*SR_U7F, SR_U10F*)
   901 apply clarify+
   902 done
   903 
   904 
   905 
   906 (*Discovering the very origin of the Nb certificate...*)
   907 lemma Outpts_A_Card_imp_pairK_parts: 
   908      "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, 
   909                     Key K, Certificate\<rbrace> \<in> set evs;  
   910         evs \<in> srb \<rbrakk>   
   911     \<Longrightarrow> \<exists> Na. Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs)"
   912 apply (erule rev_mp, erule srb.induct)
   913 apply parts_prepare
   914 apply simp_all
   915 (*Fake*)
   916 apply (blast dest: parts_insertI)
   917 (*SR_U7*)
   918 apply force
   919 (*SR_U7F*)
   920 apply force
   921 (*SR_U8*)
   922 apply blast
   923 (*SR_U10*)
   924 apply (blast dest: Inputs_imp_knows_Spy_secureM_srb parts.Inj Inputs_A_Card_9 Gets_imp_knows_Spy elim: knows_Spy_partsEs)
   925 (*SR_U10F*)
   926 apply (blast dest: Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] 
   927                    Inputs_A_Card_9 Gets_imp_knows_Spy 
   928              elim: knows_Spy_partsEs)
   929 done
   930 
   931                
   932 lemma Nb_certificate_authentic_bis: 
   933      "\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);  
   934          B \<noteq> Spy; \<not>illegalUse(Card B); 
   935          evs \<in> srb \<rbrakk>    
   936  \<Longrightarrow> \<exists> Na. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
   937                    Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
   938                    Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
   939 apply (erule rev_mp, erule srb.induct)
   940 apply parts_prepare
   941 apply (simp_all (no_asm_simp))
   942 (*Fake*)
   943 apply spy_analz
   944 (*SR_U7*)
   945 apply blast
   946 (*SR_U7F*)
   947 apply blast
   948 (*SR_U8*)
   949 apply force
   950 (*SR_U10*)
   951 apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] elim: knows_Spy_partsEs)
   952 (*SR_U10F*)
   953 apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] elim: knows_Spy_partsEs)
   954 (*SR_U11*)
   955 apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_imp_pairK_parts)
   956 done
   957 
   958 
   959 lemma Pairkey_certificate_authentic: 
   960     "\<lbrakk> Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace> \<in> parts (knows Spy evs);    
   961          Card A \<notin> cloned; evs \<in> srb \<rbrakk>        
   962      \<Longrightarrow> Pk = Pairkey(A,B) \<and>              
   963          Says Server A \<lbrace>Nonce Pk,  
   964                         Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace> 
   965            \<in> set evs"
   966 apply (erule rev_mp, erule srb.induct)
   967 apply parts_prepare
   968 apply (simp_all (no_asm_simp))
   969 (*Fake*)
   970 apply spy_analz
   971 (*SR_U8*)
   972 apply force
   973 done
   974 
   975 
   976 lemma sesK_authentic: 
   977      "\<lbrakk> Key (sesK(Nb,pairK(A,B))) \<in> parts (knows Spy evs);  
   978          A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
   979          evs \<in> srb \<rbrakk>           
   980       \<Longrightarrow> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>  
   981            \<in> set evs"
   982 apply (erule rev_mp, erule srb.induct)
   983 apply parts_prepare
   984 apply (simp_all)
   985 (*fake*)
   986 apply spy_analz
   987 (*forge*)
   988 apply (fastsimp dest: analz.Inj)
   989 (*SR_U7: used B\<noteq>Spy*)
   990 (*SR_U7F*)
   991 apply clarify
   992 (*SR_U10: used A\<noteq>Spy*)
   993 (*SR_U10F*)
   994 apply clarify
   995 done
   996 
   997 
   998 (*END authenticity theorems*)
   999 
  1000 
  1001 (*BEGIN confidentiality theorems*)
  1002 
  1003 
  1004 lemma Confidentiality: 
  1005      "\<lbrakk> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>  
  1006            \<notin> set evs; 
  1007         A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
  1008         evs \<in> srb \<rbrakk>           
  1009       \<Longrightarrow> Key (sesK(Nb,pairK(A,B))) \<notin> analz (knows Spy evs)"
  1010 apply (blast intro: sesK_authentic)
  1011 done
  1012 
  1013 lemma Confidentiality_B: 
  1014      "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
  1015           \<in> set evs;  
  1016         Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;  
  1017         A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); Card B \<notin> cloned; 
  1018         evs \<in> srb \<rbrakk>  
  1019       \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
  1020 apply (erule rev_mp, erule rev_mp, erule srb.induct)
  1021 apply analz_prepare
  1022 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
  1023 (*Fake*)
  1024 apply spy_analz
  1025 (*Forge*)
  1026 apply (rotate_tac 7)
  1027 apply (drule parts.Inj)
  1028 apply (fastsimp dest: Outpts_B_Card_form_7)
  1029 (*SR_U7*)
  1030 apply (blast dest!: Outpts_B_Card_form_7)
  1031 (*SR_U7F*)
  1032 apply clarify
  1033 apply (drule Outpts_parts_used)
  1034 apply simp
  1035 (*faster than
  1036   by (fast_tac (claset() addDs [Outpts_parts_used] addss (simpset())) 1)
  1037 *)
  1038 (*SR_U10*)
  1039 apply (fastsimp dest: Outpts_B_Card_form_7)
  1040 (*SR_U10F - uses assumption Card A not cloned*)
  1041 apply clarify
  1042 apply (drule Outpts_B_Card_form_7, assumption)
  1043 apply simp
  1044 (*Oops1*)
  1045 apply (blast dest!: Outpts_B_Card_form_7)
  1046 (*Oops2*)
  1047 apply (blast dest!: Outpts_B_Card_form_7 Outpts_A_Card_form_10)
  1048 done
  1049 
  1050 
  1051 (*END confidentiality theorems*)
  1052 
  1053 
  1054 (*BEGIN authentication theorems*)
  1055 
  1056 lemma A_authenticates_B: 
  1057      "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;
  1058         \<not>illegalUse(Card B); 
  1059         evs \<in> srb \<rbrakk>           
  1060  \<Longrightarrow> \<exists> Na. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,   
  1061                 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
  1062                 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
  1063 apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
  1064 done
  1065 
  1066 lemma A_authenticates_B_Gets: 
  1067      "\<lbrakk> Gets A \<lbrace>Nonce Nb, Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>\<rbrace>  
  1068            \<in> set evs;  
  1069          \<not>illegalUse(Card B); 
  1070          evs \<in> srb \<rbrakk>           
  1071     \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb, pairK (A, B))),   
  1072                              Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
  1073                              Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
  1074 apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
  1075 done
  1076 
  1077 
  1078 lemma A_authenticates_B_bis: 
  1079      "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Cert2\<rbrace> \<in> set evs;  
  1080         \<not>illegalUse(Card B); 
  1081         evs \<in> srb \<rbrakk>           
  1082  \<Longrightarrow> \<exists> Cert1. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
  1083                 \<in> set evs"
  1084 apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
  1085 done
  1086 
  1087 
  1088 
  1089 
  1090 
  1091 
  1092 lemma B_authenticates_A: 
  1093      "\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;  
  1094          B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
  1095          evs \<in> srb \<rbrakk>  
  1096       \<Longrightarrow> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, 
  1097          Key (sesK(Nb,pairK(A,B))), Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
  1098 apply (erule rev_mp)
  1099 apply (erule srb.induct)
  1100 apply (simp_all (no_asm_simp))
  1101 apply (blast dest: Says_imp_knows_Spy [THEN parts.Inj] Nb_certificate_authentic)
  1102 done
  1103 
  1104 
  1105 lemma B_authenticates_A_bis: 
  1106      "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;
  1107         Gets B (Cert2) \<in> set evs;  
  1108          B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
  1109          evs \<in> srb \<rbrakk>  
  1110       \<Longrightarrow> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Cert2\<rbrace> \<in> set evs"
  1111 apply (blast dest: Outpts_B_Card_form_7 B_authenticates_A)
  1112 done
  1113 
  1114 
  1115 (*END authentication theorems*)
  1116 
  1117 
  1118 lemma Confidentiality_A: 
  1119       "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
  1120                        Key K, Certificate\<rbrace> \<in> set evs;  
  1121          Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;  
  1122          A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
  1123          evs \<in> srb \<rbrakk>           
  1124      \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
  1125 apply (drule A_authenticates_B)
  1126 prefer 3
  1127 apply (erule exE)
  1128 apply (drule Confidentiality_B)
  1129 apply auto
  1130 done
  1131 
  1132 
  1133 lemma Outpts_imp_knows_agents_secureM_srb: 
  1134    "\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> X \<in> knows A evs"
  1135 apply (simp (no_asm_simp) add: Outpts_imp_knows_agents_secureM)
  1136 done
  1137 
  1138 
  1139 (*BEGIN key distribution theorems*)
  1140 lemma A_keydist_to_B: 
  1141    "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;  
  1142          \<not>illegalUse(Card B); 
  1143          evs \<in> srb \<rbrakk>           
  1144      \<Longrightarrow> Key K \<in> analz (knows B evs)"
  1145 apply (drule A_authenticates_B)
  1146 prefer 3
  1147 apply (erule exE)
  1148 apply (rule Outpts_imp_knows_agents_secureM_srb [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
  1149 apply assumption+
  1150 done
  1151 
  1152 
  1153 lemma B_keydist_to_A: 
  1154 "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;  
  1155    Gets B (Cert2) \<in> set evs;  
  1156    B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
  1157    evs \<in> srb \<rbrakk>  
  1158  \<Longrightarrow> Key K \<in> analz (knows A evs)"
  1159 apply (frule Outpts_B_Card_form_7)
  1160 apply assumption apply simp
  1161 apply (frule B_authenticates_A)
  1162 apply (rule_tac [5] Outpts_imp_knows_agents_secureM_srb [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
  1163 apply simp+
  1164 done
  1165 
  1166 (*END key distribution theorems*)
  1167 
  1168 
  1169 
  1170 
  1171 (*BEGIN further theorems about authenticity of verifiers - useful to cards,
  1172   and somewhat to agents *)
  1173 
  1174 (*MSG11
  1175 If B receives the verifier of msg11, then the verifier originated with msg7.
  1176 This is clearly not available to B: B can't check the form of the verifier because he doesn't know pairK(A,B)
  1177 *)
  1178 lemma Nb_certificate_authentic_B: 
  1179      "\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;  
  1180         B \<noteq> Spy; \<not>illegalUse(Card B); 
  1181         evs \<in> srb \<rbrakk>  
  1182      \<Longrightarrow> \<exists> Na. 
  1183             Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
  1184                 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
  1185                 Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
  1186 apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN Nb_certificate_authentic_bis])
  1187 done
  1188 
  1189 (*MSG10
  1190 If A obtains the verifier of msg10, then the verifier originated with msg7:
  1191 A_authenticates_B. It is useful to A, who can check the form of the 
  1192 verifier by application of Outpts_A_Card_form_10.
  1193 *)
  1194 
  1195 (*MSG9
  1196 The first verifier verifies the Pairkey to the card: since it's encrypted
  1197 under Ka, it must come from the server (if A's card is not cloned).
  1198 The second verifier verifies both nonces, since it's encrypted under the
  1199 pairK, it must originate with B's card  (if A and B's cards not cloned).
  1200 The third verifier verifies Na: since it's encrytped under the card's key,
  1201 it originated with the card; so the card does not need to save Na
  1202 in the first place and do a comparison now: it just verifies Na through the
  1203 verifier. Three theorems related to these three statements.
  1204 
  1205 Recall that a card can check the form of the verifiers (can decrypt them),
  1206 while an agent in general cannot, if not provided with a suitable theorem.
  1207 *)
  1208 
  1209 (*Card A can't reckon the pairkey - we need to guarantee its integrity!*)
  1210 lemma Pairkey_certificate_authentic_A_Card: 
  1211      "\<lbrakk> Inputs A (Card A)   
  1212              \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
  1213                Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,  
  1214                Cert2, Cert3\<rbrace> \<in> set evs; 
  1215          A \<noteq> Spy; Card A \<notin> cloned; evs \<in> srb \<rbrakk>   
  1216      \<Longrightarrow> Pk = Pairkey(A,B) \<and>  
  1217          Says Server A \<lbrace>Nonce (Pairkey(A,B)),  
  1218                   Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>\<rbrace>   
  1219            \<in> set evs "
  1220 apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
  1221 done
  1222 (*the second conjunct of the thesis might be regarded as a form of integrity 
  1223   in the sense of Neuman-Ts'o*)
  1224 
  1225 lemma Na_Nb_certificate_authentic_A_Card: 
  1226       "\<lbrakk> Inputs A (Card A)   
  1227              \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
  1228           Cert1, Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs; 
  1229       A \<noteq> Spy; \<not>illegalUse(Card B); evs \<in> srb \<rbrakk> 
  1230    \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb, pairK (A, B))),    
  1231                              Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
  1232                              Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
  1233            \<in> set evs "
  1234 apply (frule Inputs_A_Card_9)
  1235 apply assumption+
  1236 apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
  1237 done
  1238 
  1239 lemma Na_authentic_A_Card: 
  1240      "\<lbrakk> Inputs A (Card A)   
  1241              \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
  1242                 Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
  1243          A \<noteq> Spy; evs \<in> srb \<rbrakk>   
  1244      \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>  
  1245            \<in> set evs"
  1246 apply (blast dest: Inputs_A_Card_9)
  1247 done
  1248 
  1249 (* These three theorems for Card A can be put together trivially.
  1250 They are separated to highlight the different requirements on agents
  1251 and their cards.*)
  1252 
  1253 
  1254 lemma Inputs_A_Card_9_authentic: 
  1255   "\<lbrakk> Inputs A (Card A)   
  1256              \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
  1257                Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,  
  1258                Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs; 
  1259     A \<noteq> Spy; Card A \<notin> cloned; \<not>illegalUse(Card B); evs \<in> srb \<rbrakk>   
  1260     \<Longrightarrow>  Says Server A \<lbrace>Nonce Pk, Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace>   
  1261            \<in> set evs  \<and> 
  1262        Outpts (Card B) B \<lbrace>Nonce Nb, Agent A,  Key (sesK(Nb, pairK (A, B))),    
  1263                              Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
  1264                              Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
  1265            \<in> set evs  \<and> 
  1266          Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>  
  1267            \<in> set evs"
  1268 apply (blast dest: Inputs_A_Card_9 Na_Nb_certificate_authentic Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
  1269 done
  1270 
  1271 
  1272 (*MSG8
  1273 Nothing to prove because the message is a cleartext that comes from the 
  1274 network*)
  1275 
  1276 (*Other messages: nothing to prove because the verifiers involved are new*)
  1277 
  1278 (*END further theorems about authenticity of verifiers*)
  1279 
  1280 
  1281 
  1282 (* BEGIN trivial guarantees on outputs for agents *)
  1283 
  1284 (*MSG4*)
  1285 lemma SR_U4_imp: 
  1286      "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> 
  1287            \<in> set evs;  
  1288          A \<noteq> Spy; evs \<in> srb \<rbrakk>                 
  1289      \<Longrightarrow> \<exists> Pk V. Gets A \<lbrace>Pk, V\<rbrace> \<in> set evs"
  1290 apply (blast dest: Outpts_A_Card_4 Inputs_A_Card_3)
  1291 done
  1292 (*weak: could strengthen the model adding verifier for the Pairkey to msg3*)
  1293 
  1294 
  1295 (*MSG7*)
  1296 lemma SR_U7_imp: 
  1297      "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,  
  1298                       Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
  1299                       Cert2\<rbrace> \<in> set evs;  
  1300          B \<noteq> Spy; evs \<in> srb \<rbrakk>  
  1301      \<Longrightarrow> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
  1302 apply (blast dest: Outpts_B_Card_7 Inputs_B_Card_6)
  1303 done
  1304 
  1305 (*MSG10*)
  1306 lemma SR_U10_imp: 
  1307      "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
  1308                            Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
  1309          \<in> set evs;  
  1310         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
  1311      \<Longrightarrow> \<exists> Cert1 Cert2.  
  1312                    Gets A \<lbrace>Nonce (Pairkey (A, B)), Cert1\<rbrace> \<in> set evs \<and>  
  1313                    Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
  1314 apply (blast dest: Outpts_A_Card_10 Inputs_A_Card_9)
  1315 done
  1316 
  1317 
  1318 (*END trivial guarantees on outputs for agents*)
  1319 
  1320 
  1321 
  1322 (*INTEGRITY*)
  1323 lemma Outpts_Server_not_evs: 
  1324       "evs \<in> srb \<Longrightarrow> Outpts (Card Server) P X \<notin> set evs"
  1325 apply (erule srb.induct)
  1326 apply auto
  1327 done
  1328 
  1329 text{*@{term step2_integrity} also is a reliability theorem*}
  1330 lemma Says_Server_message_form: 
  1331      "\<lbrakk> Says Server A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs;  
  1332          evs \<in> srb \<rbrakk>                   
  1333      \<Longrightarrow> \<exists> B. Pk = Nonce (Pairkey(A,B)) \<and>  
  1334          Certificate = Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>"
  1335 apply (erule rev_mp)
  1336 apply (erule srb.induct)
  1337 apply auto
  1338 apply (blast dest!: Outpts_Server_not_evs)+
  1339 done
  1340 (*cannot be made useful to A in form of a Gets event*)
  1341 
  1342 text{*
  1343   step4integrity is @{term Outpts_A_Card_form_4}
  1344 
  1345   step7integrity is @{term Outpts_B_Card_form_7}
  1346 *}
  1347 
  1348 lemma step8_integrity: 
  1349      "\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs;  
  1350          B \<noteq> Server; B \<noteq> Spy; evs \<in> srb \<rbrakk>                   
  1351      \<Longrightarrow> \<exists> Cert2 K.   
  1352     Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
  1353 apply (erule rev_mp)
  1354 apply (erule srb.induct)
  1355 prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
  1356 apply auto
  1357 done
  1358 
  1359 
  1360 text{*  step9integrity is @{term Inputs_A_Card_form_9}
  1361         step10integrity is @{term Outpts_A_Card_form_10}.
  1362 *}
  1363 
  1364 
  1365 lemma step11_integrity: 
  1366      "\<lbrakk> Says A B (Certificate) \<in> set evs; 
  1367          \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;  
  1368          A \<noteq> Spy; evs \<in> srb \<rbrakk>  
  1369      \<Longrightarrow> \<exists> K Nb.  
  1370       Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs"
  1371 apply (erule rev_mp)
  1372 apply (erule srb.induct)
  1373 apply auto
  1374 done
  1375 
  1376 end
  1377