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