Theory ShoupRubin

(*  Author:     Giampaolo Bella, Catania University
*)

sectionOriginal Shoup-Rubin protocol

theory ShoupRubin imports Smartcard begin

axiomatization sesK :: "nat*key => key"
where
   (*sesK is injective on each component*) 
   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m'  k = k')" and
   (*all long-term keys differ from sesK*)
   shrK_disj_sesK [iff]: "shrK A  sesK(m,pk)" and
   crdK_disj_sesK [iff]: "crdK C  sesK(m,pk)" and
   pin_disj_sesK  [iff]: "pin P  sesK(m,pk)" and
   pairK_disj_sesK[iff]:"pairK(A,B)  sesK(m,pk)" and

   (*needed for base case in analz_image_freshK*)
   Atomic_distrib [iff]: "Atomic`(KEY`K  NONCE`N) =
                   Atomic`(KEY`K)  Atomic`(NONCE`N)" and

  (*this protocol makes the assumption of secure means
    between each agent and his smartcard*)
   shouprubin_assumes_securemeans [iff]: "evs  sr  secureM"

definition Unique :: "[event, event list] => bool" ("Unique _ on _") where
   "Unique ev on evs == 
      ev  set (tl (dropWhile (% z. z  ev) evs))"


inductive_set sr :: "event list set"
  where

    Nil:  "[] sr"



  | Fake: " evsF sr;  X synth (analz (knows Spy evsF)); 
             illegalUse(Card B) 
           Says Spy A X # 
              Inputs Spy (Card B) X # evsF  sr"

(*In general this rule causes the assumption Card B ∉ cloned
  in most guarantees for B - starting with confidentiality -
  otherwise pairK_confidential could not apply*)
  | Forge:
         " evsFo  sr; Nonce Nb  analz (knows Spy evsFo);
             Key (pairK(A,B))  knows Spy evsFo 
           Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo  sr"



  | Reception: " evsR sr; Says A B X  set evsR 
               Gets B X # evsR  sr"



(*A AND THE SERVER *)
  | SR1:  " evs1 sr; A  Server
           Says A Server Agent A, Agent B 
                # evs1  sr"

  | SR2:  " evs2 sr; 
             Gets Server Agent A, Agent B  set evs2 
           Says Server A Nonce (Pairkey(A,B)), 
                           Crypt (shrK A) Nonce (Pairkey(A,B)), Agent B
                  
                # evs2  sr"




(*A AND HER CARD*)
(*A cannot decrypt the verifier for she dosn't know shrK A,
  but the pairkey is recognisable*)
  | SR3:  " evs3 sr; legalUse(Card A);
             Says A Server Agent A, Agent B  set evs3;
             Gets A Nonce Pk, Certificate  set evs3 
           Inputs A (Card A) (Agent A)
                # evs3  sr"   (*however A only queries her card 
if she has previously contacted the server to initiate with some B. 
Otherwise she would do so even if the Server had not been active. 
Still, this doesn't and can't mean that the pairkey originated with 
the server*)
 
(*The card outputs the nonce Na to A*)               
  | SR4:  " evs4 sr;  A  Server; 
             Nonce Na  used evs4; legalUse(Card A);
             Inputs A (Card A) (Agent A)  set evs4  
        Outpts (Card A) A Nonce Na, Crypt (crdK (Card A)) (Nonce Na)
              # evs4  sr"

(*The card can be exploited by the spy*)
(*because of the assumptions on the card, A is certainly not server nor spy*)
  | SR4Fake: " evs4F sr; Nonce Na  used evs4F; 
                illegalUse(Card A);
                Inputs Spy (Card A) (Agent A)  set evs4F  
       Outpts (Card A) Spy Nonce Na, Crypt (crdK (Card A)) (Nonce Na)
            # evs4F  sr"




(*A TOWARDS B*)
  | SR5:  " evs5 sr; 
             Outpts (Card A) A Nonce Na, Certificate  set evs5;
              p q. Certificate  p, q 
           Says A B Agent A, Nonce Na # evs5  sr"
(*A must check that the verifier is not a compound message, 
  otherwise this would also fire after SR7 *)




(*B AND HIS CARD*)
  | SR6:  " evs6 sr; legalUse(Card B);
             Gets B Agent A, Nonce Na  set evs6 
           Inputs B (Card B) Agent A, Nonce Na 
                # evs6  sr"

(*B gets back from the card the session key and various verifiers*)
  | SR7:  " evs7 sr; 
             Nonce Nb  used evs7; legalUse(Card B); B  Server;
             K = sesK(Nb,pairK(A,B));
             Key K  used evs7;
             Inputs B (Card B) Agent A, Nonce Na  set evs7
     Outpts (Card B) B Nonce Nb, Key K,
                            Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                            Crypt (pairK(A,B)) (Nonce Nb) 
                # evs7  sr"

 (*The card can be exploited by the spy*)
(*because of the assumptions on the card, A is certainly not server nor spy*)
  | SR7Fake:  " evs7F sr; Nonce Nb  used evs7F; 
                 illegalUse(Card B);
                 K = sesK(Nb,pairK(A,B));
                 Key K  used evs7F;
                 Inputs Spy (Card B) Agent A, Nonce Na  set evs7F 
           Outpts (Card B) Spy Nonce Nb, Key K,
                            Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                            Crypt (pairK(A,B)) (Nonce Nb) 
                # evs7F  sr"




(*B TOWARDS A*)
(*having sent an input that mentions A is the only memory B relies on,
  since the output doesn't mention A - lack of explicitness*) 
  | SR8:  " evs8 sr;  
             Inputs B (Card B) Agent A, Nonce Na  set evs8;
             Outpts (Card B) B Nonce Nb, Key K, 
                                 Cert1, Cert2  set evs8 
           Says B A Nonce Nb, Cert1 # evs8  sr"
  



(*A AND HER CARD*)
(*A cannot check the form of the verifiers - although I can prove the form of
  Cert2 - and just feeds her card with what she's got*)
  | SR9:  " evs9 sr; legalUse(Card A);
             Gets A Nonce Pk, Cert1  set evs9;
             Outpts (Card A) A Nonce Na, Cert2  set evs9; 
             Gets A Nonce Nb, Cert3  set evs9;
              p q. Cert2  p, q 
           Inputs A (Card A) 
                 Agent B, Nonce Na, Nonce Nb, Nonce Pk,
                  Cert1, Cert3, Cert2 
                # evs9  sr"

(*But the card will only give outputs to the inputs of the correct form*)
  | SR10: " evs10 sr; legalUse(Card A); A  Server;
             K = sesK(Nb,pairK(A,B));
             Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, 
                                 Nonce (Pairkey(A,B)),
                                 Crypt (shrK A) Nonce (Pairkey(A,B)), 
                                                   Agent B,
                                 Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                                 Crypt (crdK (Card A)) (Nonce Na)
                set evs10 
           Outpts (Card A) A Key K, Crypt (pairK(A,B)) (Nonce Nb)
                 # evs10  sr"

(*The card can be exploited by the spy*)
(*because of the assumptions on the card, A is certainly not server nor spy*)
  | SR10Fake: " evs10F sr; 
                 illegalUse(Card A);
                 K = sesK(Nb,pairK(A,B));
                 Inputs Spy (Card A) Agent B, Nonce Na, Nonce Nb, 
                                       Nonce (Pairkey(A,B)),
                                       Crypt (shrK A) Nonce (Pairkey(A,B)), 
                                                        Agent B,
                                       Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                                       Crypt (crdK (Card A)) (Nonce Na)
                    set evs10F 
           Outpts (Card A) Spy Key K, Crypt (pairK(A,B)) (Nonce Nb)
                 # evs10F  sr"




(*A TOWARDS B*)
(*having initiated with B is the only memory A relies on,
  since the output doesn't mention B - lack of explicitness*) 
  | SR11: " evs11 sr;
             Says A Server Agent A, Agent B  set evs11;
             Outpts (Card A) A Key K, Certificate  set evs11 
           Says A B (Certificate) 
                 # evs11  sr"



    (*Both peers may leak by accident the session keys obtained from their
      cards*)
  | Oops1:
     " evsO1  sr;
         Outpts (Card B) B Nonce Nb, Key K, Certificate, 
                             Crypt (pairK(A,B)) (Nonce Nb)  set evsO1 
      Notes Spy Key K, Nonce Nb, Agent A, Agent B # evsO1  sr"

  | Oops2:
     " evsO2  sr;
         Outpts (Card A) A Key K, Crypt (pairK(A,B)) (Nonce Nb) 
            set evsO2 
     Notes Spy Key K, Nonce Nb, Agent A, Agent B # evsO2  sr"






(*To solve Fake case when it doesn't involve analz - used to be condensed
  into Fake_parts_insert_tac*)
declare Fake_parts_insert_in_Un  [dest]
declare analz_into_parts [dest]
(*declare parts_insertI [intro]*)



(*General facts about message reception*)
lemma Gets_imp_Says: 
       " Gets B X  set evs; evs  sr    A. Says A B X  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Gets_imp_knows_Spy: 
     " Gets B X  set evs; evs  sr    X  knows Spy evs"
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
done

lemma Gets_imp_knows_Spy_parts_Snd: 
     " Gets B X, Y  set evs; evs  sr    Y  parts (knows Spy evs)"
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy parts.Inj parts.Snd)
done

lemma Gets_imp_knows_Spy_analz_Snd: 
     " Gets B X, Y  set evs; evs  sr    Y  analz (knows Spy evs)"
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy analz.Inj analz.Snd)
done

(*end general facts*)



(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help
  the simplifier, especially in analz_image_freshK*)


lemma Inputs_imp_knows_Spy_secureM_sr: 
      " Inputs Spy C X  set evs; evs  sr   X  knows Spy evs"
apply (simp (no_asm_simp) add: Inputs_imp_knows_Spy_secureM)
done

lemma knows_Spy_Inputs_secureM_sr_Spy: 
      "evs sr  knows Spy (Inputs Spy C X # evs) = insert X (knows Spy evs)"
apply (simp (no_asm_simp))
done

lemma knows_Spy_Inputs_secureM_sr: 
    " A  Spy; evs sr   knows Spy (Inputs A C X # evs) =  knows Spy evs"
apply (simp (no_asm_simp))
done

lemma knows_Spy_Outpts_secureM_sr_Spy: 
      "evs sr  knows Spy (Outpts C Spy X # evs) = insert X (knows Spy evs)"
apply (simp (no_asm_simp))
done

lemma knows_Spy_Outpts_secureM_sr: 
     " A  Spy; evs sr   knows Spy (Outpts C A X # evs) =  knows Spy evs"
apply (simp (no_asm_simp))
done

(*End lemmas on secure means for shouprubin*)




(*BEGIN technical lemmas - evolution of forwarding lemmas*)

(*If an honest agent uses a smart card, then the card is his/her own, is
  not stolen, and the agent has received suitable data to feed the card. 
  In other words, these are guarantees that an honest agent can only use 
  his/her own card, and must use it correctly.
  On the contrary, the spy can "Inputs" any cloned cards also by the Fake rule.

  Instead of Auto_tac, proofs here used to asm-simplify and then force-tac.
*)
lemma Inputs_A_Card_3: 
    " Inputs A C (Agent A)  set evs; A  Spy; evs  sr   
      legalUse(C)  C = (Card A)   
      ( Pk Certificate. Gets A Pk, Certificate  set evs)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Inputs_B_Card_6: 
     " Inputs B C Agent A, Nonce Na  set evs; B  Spy; evs  sr   
       legalUse(C)  C = (Card B)  Gets B Agent A, Nonce Na  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Inputs_A_Card_9: 
     " Inputs A C Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
                                           Cert1, Cert2, Cert3  set evs; 
         A  Spy; evs  sr   
   legalUse(C)  C = (Card A)   
      Gets A Nonce Pk, Cert1  set evs       
      Outpts (Card A) A Nonce Na, Cert3  set evs           
      Gets A Nonce Nb, Cert2  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done


(*The two occurrences of A in the Outpts event don't match SR4Fake, where
  A cannot be the Spy. Hence the card is legally usable by rule SR4*)
lemma Outpts_A_Card_4: 
     " Outpts C A Nonce Na, (Crypt (crdK (Card A)) (Nonce Na))  set evs;  
         evs  sr   
      legalUse(C)  C = (Card A)   
         Inputs A (Card A) (Agent A)  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done


(*First certificate is made explicit so that a comment similar to the previous
  applies. This also provides Na to the Inputs event in the conclusion*)
lemma Outpts_B_Card_7: 
      " Outpts C B Nonce Nb, Key K,  
                      Crypt (pairK(A,B)) Nonce Na, Nonce Nb,  
                      Cert2  set evs;  
         evs  sr   
      legalUse(C)  C = (Card B)   
         Inputs B (Card B) Agent A, Nonce Na  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_A_Card_10: 
     " Outpts C A Key K, (Crypt (pairK(A,B)) (Nonce Nb))  set evs; 
         evs  sr   
      legalUse(C)  C = (Card A)   
         ( Na Ver1 Ver2 Ver3.  
       Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
                              Ver1, Ver2, Ver3  set evs)"
apply (erule rev_mp, erule sr.induct)
apply auto
done



(*
A can't check the form of the certificate, and so cannot associate the sesion 
key to the other peer! This already shows that the protocol fails to satisfy 
the principle of goal availability for the goal of key association.
Similar reasoning below for the goal of confidentiality will be even more
accessible.
*)
lemma Outpts_A_Card_10_imp_Inputs: 
     " Outpts (Card A) A Key K, Certificate  set evs; evs  sr   
      ( B Na Nb Ver1 Ver2 Ver3.  
       Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
                              Ver1, Ver2, Ver3  set evs)"
apply (erule rev_mp, erule sr.induct)
apply simp_all
apply blast+
done




(*Weaker version: if the agent can't check the forms of the verifiers, then
  the agent must not be the spy so as to solve SR4Fake. The verifier must be
  recognised as some cyphertex in order to distinguish from case SR7, 
  concerning B's output, which also begins with a nonce.
*)
lemma Outpts_honest_A_Card_4: 
     " Outpts C A Nonce Na, Crypt K X set evs; 
         A  Spy;  evs  sr   
      legalUse(C)  C = (Card A)   
         Inputs A (Card A) (Agent A)  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done

(*alternative formulation of same theorem
Goal "⟦ Outpts C A ⦃Nonce Na, Certificate⦄ ∈ set evs;  
         ∀ p q. Certificate ≠ ⦃p, q⦄;    
         A ≠ Spy; evs ∈ sr ⟧  
     ⟹ legalUse(C) ∧ C = (Card A) ∧  
         Inputs A (Card A) (Agent A) ∈ set evs"
same proof
*)


lemma Outpts_honest_B_Card_7: 
     " Outpts C B Nonce Nb, Key K, Cert1, Cert2  set evs;  
         B  Spy; evs  sr   
      legalUse(C)  C = (Card B)   
         ( A Na. Inputs B (Card B) Agent A, Nonce Na  set evs)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_honest_A_Card_10: 
     " Outpts C A Key K, Certificate  set evs;  
         A  Spy; evs  sr   
      legalUse (C)  C = (Card A)   
         ( B Na Nb Pk Ver1 Ver2 Ver3.  
          Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, Pk,  
                              Ver1, Ver2, Ver3  set evs)"
apply (erule rev_mp, erule sr.induct)
apply simp_all
apply blast+
done
(*-END-*)


(*Even weaker versions: if the agent can't check the forms of the verifiers
  and the agent may be the spy, then we must know what card the agent
  is getting the output from. 
*)
lemma Outpts_which_Card_4: 
    " Outpts (Card A) A Nonce Na, Crypt K X  set evs; evs  sr   
     Inputs A (Card A) (Agent A)  set evs"
apply (erule rev_mp, erule sr.induct)
apply (simp_all (no_asm_simp))
apply clarify
done

lemma Outpts_which_Card_7: 
  " Outpts (Card B) B Nonce Nb, Key K, Cert1, Cert2  set evs;  
         evs  sr   
       A Na. Inputs B (Card B) Agent A, Nonce Na  set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_which_Card_10: 
     " Outpts (Card A) A Key (sesK(Nb,pairK(A,B))),  
                             Crypt (pairK(A,B)) (Nonce Nb)   set evs;  
         evs  sr   
      Na. Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), 
                            Crypt (shrK A) Nonce (Pairkey(A,B)), Agent B,  
                            Crypt (pairK(A,B)) Nonce Na, Nonce Nb,  
                            Crypt (crdK (Card A)) (Nonce Na)   set evs"
apply (erule rev_mp, erule sr.induct)
apply auto
done


(*Lemmas on the form of outputs*)


(*A needs to check that the verifier is a cipher for it to come from SR4
  otherwise it could come from SR7 *)
lemma Outpts_A_Card_form_4: 
  " Outpts (Card A) A Nonce Na, Certificate  set evs;  
          p q. Certificate  p, q; evs  sr   
      Certificate = (Crypt (crdK (Card A)) (Nonce Na))"
apply (erule rev_mp, erule sr.induct)
apply (simp_all (no_asm_simp))
done

lemma Outpts_B_Card_form_7: 
   " Outpts (Card B) B Nonce Nb, Key K, Cert1, Cert2  set evs; 
         evs  sr           
        A Na.    
          K = sesK(Nb,pairK(A,B))                        
          Cert1 = (Crypt (pairK(A,B)) Nonce Na, Nonce Nb)   
          Cert2 = (Crypt (pairK(A,B)) (Nonce Nb))"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_A_Card_form_10: 
   " Outpts (Card A) A Key K, Certificate  set evs; evs  sr   
        B Nb.  
          K = sesK(Nb,pairK(A,B))   
          Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
apply (erule rev_mp, erule sr.induct)
apply (simp_all (no_asm_simp))
done

lemma Outpts_A_Card_form_bis: 
  " Outpts (Card A') A' Key (sesK(Nb,pairK(A,B))), Certificate  set evs; 
         evs  sr   
       A' = A   
          Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
apply (erule rev_mp, erule sr.induct)
apply (simp_all (no_asm_simp))
done

(*… and Inputs *)

lemma Inputs_A_Card_form_9: 
     " Inputs A (Card A) Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
                             Cert1, Cert2, Cert3  set evs; 
         evs  sr   
      Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
apply (erule rev_mp)
apply (erule sr.induct)
apply (simp_all (no_asm_simp))
(*Fake*)
apply force
(*SR9*)
apply (blast dest!: Outpts_A_Card_form_4)
done
(* Pk, Cert1, Cert2 cannot be made explicit because they traversed the network in the clear *)

(*General guarantees on Inputs and Outpts*)

(*for any agents*)


lemma Inputs_Card_legalUse: 
  " Inputs A (Card A) X  set evs; evs  sr   legalUse(Card A)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_Card_legalUse: 
  " Outpts (Card A) A X  set evs; evs  sr   legalUse(Card A)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

(*for honest agents*)

lemma Inputs_Card: " Inputs A C X  set evs; A  Spy; evs  sr   
       C = (Card A)  legalUse(C)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Outpts_Card: " Outpts C A X  set evs; A  Spy; evs  sr   
       C = (Card A)  legalUse(C)"
apply (erule rev_mp, erule sr.induct)
apply auto
done

lemma Inputs_Outpts_Card: 
     " Inputs A C X  set evs  Outpts C A Y  set evs;  
         A  Spy; evs  sr   
      C = (Card A)  legalUse(Card A)"
apply (blast dest: Inputs_Card Outpts_Card)
done


(*for the spy - they stress that the model behaves as it is meant to*) 

(*The or version can be also proved directly.
  It stresses that the spy may use either her own legally usable card or
  all the illegally usable cards.
*)
lemma Inputs_Card_Spy: 
  " Inputs Spy C X  set evs  Outpts C Spy X  set evs; evs  sr   
       C = (Card Spy)  legalUse(Card Spy)   
          ( A. C = (Card A)  illegalUse(Card A))"
apply (erule rev_mp, erule sr.induct)
apply auto
done


(*END technical lemmas*)






(*BEGIN unicity theorems: certain items uniquely identify a smart card's
                          output*)

(*A's card's first output: the nonce uniquely identifies the rest*)
lemma Outpts_A_Card_unique_nonce:
     " Outpts (Card A) A Nonce Na, Crypt (crdK (Card A)) (Nonce Na)  
            set evs;   
         Outpts (Card A') A' Nonce Na, Crypt (crdK (Card A')) (Nonce Na) 
            set evs;   
         evs  sr   A=A'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
apply (fastforce dest: Outpts_parts_used)
apply blast
done

(*B's card's output: the NONCE uniquely identifies the rest*)
lemma Outpts_B_Card_unique_nonce: 
     " Outpts (Card B) B Nonce Nb, Key SK, Cert1, Cert2  set evs;   
         Outpts (Card B') B' Nonce Nb, Key SK', Cert1', Cert2'  set evs;   
         evs  sr   B=B'  SK=SK'  Cert1=Cert1'  Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
apply (fastforce dest: Outpts_parts_used)
apply blast
done


(*B's card's output: the SESKEY uniquely identifies the rest*)
lemma Outpts_B_Card_unique_key: 
     " Outpts (Card B) B Nonce Nb, Key SK, Cert1, Cert2  set evs;   
         Outpts (Card B') B' Nonce Nb', Key SK, Cert1', Cert2'  set evs;   
         evs  sr   B=B'  Nb=Nb'  Cert1=Cert1'  Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
apply (fastforce dest: Outpts_parts_used)
apply blast
done

lemma Outpts_A_Card_unique_key: " Outpts (Card A) A Key K, V  set evs;   
         Outpts (Card A') A' Key K, V'  set evs;   
         evs  sr   A=A'  V=V'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
apply (blast dest: Outpts_A_Card_form_bis)
apply blast
done


(*Revised unicity theorems - applies to both steps 4 and 7*)
lemma Outpts_A_Card_Unique: 
  " Outpts (Card A) A Nonce Na, rest  set evs; evs  sr   
      Unique (Outpts (Card A) A Nonce Na, rest) on evs"
apply (erule rev_mp, erule sr.induct, simp_all add: Unique_def)
apply (fastforce dest: Outpts_parts_used)
apply blast
apply (fastforce dest: Outpts_parts_used)
apply blast
done

(*can't prove the same on evs10 for it doesn't have a freshness assumption!*)


(*END unicity theorems*)


(*BEGIN counterguarantees about spy's knowledge*)

(*on nonces*)

lemma Spy_knows_Na: 
      " Says A B Agent A, Nonce Na  set evs; evs  sr   
       Nonce Na  analz (knows Spy evs)"
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
done

lemma Spy_knows_Nb: 
      " Says B A Nonce Nb, Certificate  set evs; evs  sr   
       Nonce Nb  analz (knows Spy evs)"
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst])
done


(*on Pairkey*)

lemma Pairkey_Gets_analz_knows_Spy: 
      " Gets A Nonce (Pairkey(A,B)), Certificate  set evs; evs  sr   
       Nonce (Pairkey(A,B))  analz (knows Spy evs)"
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
done

lemma Pairkey_Inputs_imp_Gets: 
     " Inputs A (Card A)             
           Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
             Cert1, Cert3, Cert2  set evs;           
         A  Spy; evs  sr      
       Gets A Nonce (Pairkey(A,B)), Cert1  set evs"
apply (erule rev_mp, erule sr.induct)
apply (simp_all (no_asm_simp))
apply force
done

lemma Pairkey_Inputs_analz_knows_Spy: 
     " Inputs A (Card A)             
           Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
             Cert1, Cert3, Cert2  set evs;           
         evs  sr      
      Nonce (Pairkey(A,B))  analz (knows Spy evs)"
apply (case_tac "A = Spy")
apply (fastforce dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
done

(* This fails on base case because of XOR properties.
lemma Pairkey_authentic:
  "⟦ Nonce (Pairkey(A,B)) ∈ parts (knows Spy evs);
     Card A ∉ cloned; evs ∈ sr ⟧
 ⟹ ∃ cert. Says Server A ⦃Nonce (Pairkey(A,B)), Cert⦄ ∈ set evs"
apply (erule rev_mp)
apply (erule sr.induct, simp_all)
apply clarify
oops

 1. ⋀x a b.
       ⟦Card A ∉ cloned; Pairkey (A, B) = Pairkey (a, b); Card a ∈ cloned;
        Card b ∈ cloned⟧
       ⟹ False
*)

(*END counterguarantees on spy's knowledge*)


(*BEGIN rewrite rules for parts operator*)


declare shrK_disj_sesK [THEN not_sym, iff] 
declare pin_disj_sesK [THEN not_sym, iff]
declare crdK_disj_sesK [THEN not_sym, iff]
declare pairK_disj_sesK [THEN not_sym, iff]


ML

structure ShoupRubin =
struct

fun prepare_tac ctxt = 
 (*SR8*)   forward_tac ctxt [@{thm Outpts_B_Card_form_7}] 14 THEN
           eresolve_tac ctxt [exE] 15 THEN eresolve_tac ctxt [exE] 15 THEN 
 (*SR9*)   forward_tac ctxt [@{thm Outpts_A_Card_form_4}] 16 THEN 
 (*SR11*)  forward_tac ctxt [@{thm Outpts_A_Card_form_10}] 21 THEN
           eresolve_tac ctxt [exE] 22 THEN eresolve_tac ctxt [exE] 22

fun parts_prepare_tac ctxt = 
           prepare_tac ctxt THEN
 (*SR9*)   dresolve_tac ctxt [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
 (*SR9*)   dresolve_tac ctxt [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
 (*Oops1*) dresolve_tac ctxt [@{thm Outpts_B_Card_form_7}] 25    THEN               
 (*Oops2*) dresolve_tac ctxt [@{thm Outpts_A_Card_form_10}] 27 THEN                
 (*Base*)  (force_tac ctxt) 1

fun analz_prepare_tac ctxt =
         prepare_tac ctxt THEN
         dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN 
 (*SR9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN 
         REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)

end


method_setup prepare = 
    Scan.succeed (SIMPLE_METHOD o ShoupRubin.prepare_tac)
  "to launch a few simple facts that will help the simplifier"

method_setup parts_prepare = 
    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt))
  "additional facts to reason about parts"

method_setup analz_prepare = 
    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.analz_prepare_tac ctxt))
  "additional facts to reason about analz"


(*Treatment of pins is here for completeness. This protocol doesn't use pins*)
lemma Spy_parts_keys [simp]: "evs  sr   
  (Key (shrK P)  parts (knows Spy evs)) = (Card P  cloned)   
  (Key (pin P)  parts (knows Spy evs)) = (P  bad  Card P  cloned)   
  (Key (crdK C)  parts (knows Spy evs)) = (C  cloned)   
  (Key (pairK(A,B))  parts (knows Spy evs)) = (Card B  cloned)"
apply (erule sr.induct)
apply parts_prepare
apply simp_all
apply (blast intro: parts_insertI)
done


(*END rewrite rules for parts operator*)

(*BEGIN rewrite rules for analz operator*)

lemma Spy_analz_shrK[simp]: "evs  sr   
  (Key (shrK P)  analz (knows Spy evs)) = (Card P  cloned)" 
apply (auto dest!: Spy_knows_cloned)
done

lemma Spy_analz_crdK[simp]: "evs  sr   
  (Key (crdK C)  analz (knows Spy evs)) = (C  cloned)"
apply (auto dest!: Spy_knows_cloned)
done

lemma Spy_analz_pairK[simp]: "evs  sr   
  (Key (pairK(A,B))  analz (knows Spy evs)) = (Card B  cloned)"
apply (auto dest!: Spy_knows_cloned)
done



(*Because initState contains a set of nonces, this is needed for base case of
  analz_image_freshK*)
lemma analz_image_Key_Un_Nonce:
  "analz (Key ` K  Nonce ` N) = Key ` K  Nonce ` N"
  by (auto simp del: parts_image)

method_setup sc_analz_freshK = 
    Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD
      (EVERY [REPEAT_FIRST
       (resolve_tac ctxt [allI, ballI, impI]),
        REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
        ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
          addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
                    @{thm knows_Spy_Outpts_secureM_sr_Spy},
                    @{thm shouprubin_assumes_securemeans}, 
                    @{thm analz_image_Key_Un_Nonce}]))])))
    "for proving the Session Key Compromise theorem for smartcard protocols"


lemma analz_image_freshK [rule_format]: 
     "evs  sr        K KK.  
          (Key K  analz (Key`KK  (knows Spy evs))) =  
          (K  KK  Key K  analz (knows Spy evs))"
apply (erule sr.induct)
apply analz_prepare
apply sc_analz_freshK
apply spy_analz
done


lemma analz_insert_freshK: "evs  sr    
         Key K  analz (insert (Key K') (knows Spy evs)) =  
         (K = K'  Key K  analz (knows Spy evs))"
apply (simp only: analz_image_freshK_simps analz_image_freshK)
done

(*END rewrite rules for analz operator*)

(*BEGIN authenticity theorems*)




(*Card B ∉ cloned needed for Fake
  B ∉ bad needed for SR7Fake; equivalent to Card B ∉ stolen
*)

lemma Na_Nb_certificate_authentic: 
     " Crypt (pairK(A,B)) Nonce Na, Nonce Nb  parts (knows Spy evs);  
         ¬illegalUse(Card B); 
         evs  sr            
      Outpts (Card B) B Nonce Nb, Key (sesK(Nb,pairK(A,B))),   
                Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply simp_all
(*Fake*)
apply spy_analz
(*SR7F*)
apply clarify
done

(* Card B ∉ cloned needed for Fake and SR7F
   B ≠ Spy needed for SR7
   B ∉ bad - or Card B ∉ stolen - needed for SR7F
   Card A ∉ cloned needed for SR10F
   A ∉ bad - or Card A ∉ stolen - needed for SR10F

   Non-trivial case done by the simplifier.*)
lemma Nb_certificate_authentic: 
      " Crypt (pairK(A,B)) (Nonce Nb)  parts (knows Spy evs);  
         B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
         evs  sr     
      Outpts (Card A) A Key (sesK(Nb,pairK(A,B))),  
                             Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply (case_tac [17] "Aa = Spy")
apply simp_all
(*Fake*)
apply spy_analz
(*SR7F, SR10F*)
apply clarify+
done



(*Discovering the very origin of the Nb certificate... non needed!*)
(*lemma*)
lemma Outpts_A_Card_imp_pairK_parts: 
     " Outpts (Card A) A            
         Key K, Crypt (pairK(A,B)) (Nonce Nb)  set evs;  
         evs  sr    
       Na. Crypt (pairK(A,B)) Nonce Na, Nonce Nb  parts (knows Spy evs)"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply simp_all
(*Fake*)
apply (blast dest: parts_insertI)
(*SR7*)
apply force
(*SR7F*)
apply force
(*SR8*)
apply blast
(*SR10*)
apply (blast dest: Inputs_imp_knows_Spy_secureM_sr parts.Inj Inputs_A_Card_9 Gets_imp_knows_Spy elim: knows_Spy_partsEs)
(*SR10F*)
apply (blast dest: Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj] 
                   Inputs_A_Card_9 Gets_imp_knows_Spy 
             elim: knows_Spy_partsEs)
done



lemma Nb_certificate_authentic_bis: 
     " Crypt (pairK(A,B)) (Nonce Nb)  parts (knows Spy evs);  
         B  Spy; ¬illegalUse(Card B); 
         evs  sr     
       Na. Outpts (Card B) B Nonce Nb, Key (sesK(Nb,pairK(A,B))),   
                   Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                   Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply (simp_all (no_asm_simp))
(*Fake*)
apply spy_analz
(*SR7*)
apply blast
(*SR7F*)
apply blast
(*SR10*)
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj] elim: knows_Spy_partsEs)
(*SR10F*)
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_sr [THEN parts.Inj] elim: knows_Spy_partsEs)
(*SR11*)
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_imp_pairK_parts)
done


lemma Pairkey_certificate_authentic: 
    " Crypt (shrK A) Nonce Pk, Agent B  parts (knows Spy evs);    
         Card A  cloned; evs  sr         
      Pk = Pairkey(A,B)               
         Says Server A Nonce Pk,  
                        Crypt (shrK A) Nonce Pk, Agent B 
            set evs"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply (simp_all (no_asm_simp))
(*Fake*)
apply spy_analz
done


(*Alternatively:  A ∉ bad; Card A ∉ cloned; B ∉ bad; Card B ∉ cloned;*)
lemma sesK_authentic: 
     " Key (sesK(Nb,pairK(A,B)))  parts (knows Spy evs);  
         A  Spy; B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
         evs  sr            
       Notes Spy Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B  
            set evs"
apply (erule rev_mp, erule sr.induct)
apply parts_prepare
apply (simp_all (no_asm_simp))
(*fake*)
apply spy_analz
(*forge*)
apply (fastforce dest: analz.Inj)
(*SR7: used B≠Spy*)
(*SR7F*)
apply clarify
(*SR10: used A≠Spy*)
(*SR10F*)
apply clarify
(*Oops*)
apply simp_all
done


(*END authenticity theorems*)


(*BEGIN confidentiality theorems*)

(*If B were bad and his card stolen, they spy could use B's card but would 
  not obtain this K because B's card only issues new session keys out
  of new nonces. 
  If A were bad, then her card could be stolen, hence the spy could feed it
  with Nb and get this K. Thus, A∉bad can be replaced by Card A ∉ stolen
  Hence these are the minimal assumptions:
        A ∉ bad; B ≠ Spy; Card A ∉ cloned; Card B ∉ cloned; 
         A ≠ Spy; B ≠ Spy; ¬illegalUse(Card A); Card B ∉ cloned;
*)

lemma Confidentiality: 
     " Notes Spy Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B  
            set evs; 
        A  Spy; B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
        evs  sr            
       Key (sesK(Nb,pairK(A,B)))  analz (knows Spy evs)"
apply (blast intro: sesK_authentic)
done

lemma Confidentiality_B: 
     " Outpts (Card B) B Nonce Nb, Key K, Certificate,          
                             Crypt (pairK(A,B)) (Nonce Nb)  set evs;  
         Notes Spy Key K, Nonce Nb, Agent A, Agent B  set evs;  
         A  Spy; B  Spy; ¬illegalUse(Card A); Card B  cloned; 
         evs  sr   
       Key K  analz (knows Spy evs)"
apply (erule rev_mp, erule rev_mp, erule sr.induct)
apply analz_prepare
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
(*Fake*)
apply spy_analz
(*Forge*)
apply (rotate_tac 7)
apply (drule parts.Inj)
apply (fastforce dest: Outpts_B_Card_form_7)
(*SR7*)
apply (blast dest!: Outpts_B_Card_form_7)
(*SR7F*)
apply clarify
apply (drule Outpts_parts_used)
apply simp
(*faster than
  apply (fastforce dest: Outpts_parts_used)
*)
(*SR10*)
apply (fastforce dest: Outpts_B_Card_form_7)
(*SR10F - uses assumption Card A not cloned*)
apply clarify
apply (drule Outpts_B_Card_form_7, assumption)
apply simp
(*Oops1*)
apply (blast dest!: Outpts_B_Card_form_7)
(*Oops2*)
apply (blast dest!: Outpts_B_Card_form_7 Outpts_A_Card_form_10)
done

(*Confidentiality_A can be is faster to prove in forward style, using
the authentication theorems. So it is moved below*)


(*END confidentiality theorems*)



(*BEGIN authentication theorems*)

lemma A_authenticates_B: 
     " Outpts (Card A) A Key K, Crypt (pairK(A,B)) (Nonce Nb)  set evs;  
         ¬illegalUse(Card B); 
         evs  sr            
       Na. 
            Outpts (Card B) B Nonce Nb, Key K,   
                Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
done

lemma A_authenticates_B_Gets: 
     " Gets A Nonce Nb, Crypt (pairK(A,B)) Nonce Na, Nonce Nb  
            set evs;  
         ¬illegalUse(Card B); 
         evs  sr            
      Outpts (Card B) B Nonce Nb, Key (sesK(Nb, pairK (A, B))),   
                             Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                             Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
done




lemma B_authenticates_A: 
     " Gets B (Crypt (pairK(A,B)) (Nonce Nb))  set evs;  
         B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
         evs  sr   
       Outpts (Card A) A            
       Key (sesK(Nb,pairK(A,B))), Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (erule rev_mp)
apply (erule sr.induct)
apply (simp_all (no_asm_simp))
apply (blast dest: Says_imp_knows_Spy [THEN parts.Inj] Nb_certificate_authentic)
done


(*END authentication theorems*)

lemma Confidentiality_A: " Outpts (Card A) A            
           Key K, Crypt (pairK(A,B)) (Nonce Nb)  set evs;  
         Notes Spy Key K, Nonce Nb, Agent A, Agent B  set evs;  
         A  Spy; B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
         evs  sr            
      Key K  analz (knows Spy evs)"
apply (drule A_authenticates_B)
prefer 3
apply (erule exE)
apply (drule Confidentiality_B)
apply auto
done

lemma Outpts_imp_knows_agents_secureM_sr: 
   " Outpts (Card A) A X  set evs; evs  sr   X  knows A evs"
apply (simp (no_asm_simp) add: Outpts_imp_knows_agents_secureM)
done


(*BEGIN key distribution theorems*)


(*Alternatively: B ∉ bad; Card B ∉ cloned;*)
lemma A_keydist_to_B: 
     " Outpts (Card A) A            
           Key K, Crypt (pairK(A,B)) (Nonce Nb)  set evs;  
         ¬illegalUse(Card B); 
         evs  sr            
      Key K  analz (knows B evs)"
apply (drule A_authenticates_B)
prefer 3
apply (erule exE)
apply (rule Outpts_imp_knows_agents_secureM_sr [THEN analz.Inj, THEN analz.Snd, THEN analz.Fst])
apply assumption+
done


(*Alternatively: A ∉ bad; B ∉ bad; Card A ∉ cloned; Card B ∉ cloned;*)
lemma B_keydist_to_A: 
     " Outpts (Card B) B Nonce Nb, Key K, Certificate,          
                             (Crypt (pairK(A,B)) (Nonce Nb))  set evs;  
         Gets B (Crypt (pairK(A,B)) (Nonce Nb))  set evs;  
         B  Spy; ¬illegalUse(Card A); ¬illegalUse(Card B); 
         evs  sr   
      Key K  analz (knows A evs)"
apply (frule B_authenticates_A)
apply (drule_tac [5] Outpts_B_Card_form_7)
apply (rule_tac [6] Outpts_imp_knows_agents_secureM_sr [THEN analz.Inj, THEN analz.Fst])
prefer 6 apply force
apply assumption+
done

(*END key distribution theorems*)








(*BEGIN further theorems about authenticity of verifiers
  (useful to agents and cards).                          *)

(*MSG11
If B receives the verifier of msg11, then the verifier originated with msg7.
Alternatively: A ∉ bad; B ∉ bad; Card A ∉ cloned; Card B ∉ cloned;
*)
lemma Nb_certificate_authentic_B: 
     " Gets B (Crypt (pairK(A,B)) (Nonce Nb))  set evs;  
        B  Spy; ¬illegalUse(Card B); 
        evs  sr   
      Na. 
            Outpts (Card B) B Nonce Nb, Key (sesK(Nb,pairK(A,B))),   
                Crypt (pairK(A,B)) Nonce Na, Nonce Nb, 
                Crypt (pairK(A,B)) (Nonce Nb)  set evs"
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN Nb_certificate_authentic_bis])
done
(*Useless to B: B can't check the form of the verifier because he doesn't know
  pairK(A,B) *)

(*MSG10
If A obtains the verifier of msg10, then the verifier originated with msg7:
A_authenticates_B. It is useful to A, who can check the form of the 
verifier by application of Outpts_A_Card_form_10.
*)

(*MSG9
The first verifier verifies the Pairkey to the card: since it's encrypted
under Ka, it must come from the server (if A's card is not cloned).
The second verifier verifies both nonces, since it's encrypted under the
pairK, it must originate with B's card  (if A and B's cards not cloned).
The third verifier verifies Na: since it's encrytped under the card's key,
it originated with the card; so the card does not need to save Na
in the first place and do a comparison now: it just verifies Na through the
verifier. Three theorems related to these three statements.

Recall that a card can check the form of the verifiers (can decrypt them),
while an agent in general cannot, if not provided with a suitable theorem.
*)

(*Card A can't reckon the pairkey - we need to guarantee its integrity!*)
lemma Pairkey_certificate_authentic_A_Card: 
     " Inputs A (Card A)   
             Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
               Crypt (shrK A) Nonce Pk, Agent B,  
               Cert2, Cert3  set evs; 
         A  Spy; Card A  cloned; evs  sr    
      Pk = Pairkey(A,B)   
         Says Server A Nonce (Pairkey(A,B)),  
                  Crypt (shrK A) Nonce (Pairkey(A,B)), Agent B   
            set evs "
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
done
(*the second conjunct of the thesis might be regarded as a form of integrity 
  in the sense of Neuman-Ts'o*)

lemma Na_Nb_certificate_authentic_A_Card: 
      " Inputs A (Card A)   
             Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
               Cert1,  
               Crypt (pairK(A,B)) Nonce Na, Nonce Nb, Cert3  set evs; 
      A  Spy; ¬illegalUse(Card B); evs  sr  
      Outpts (Card B) B Nonce Nb, Key (sesK(Nb, pairK (A, B))),    
                             Crypt (pairK(A,B)) Nonce Na, Nonce Nb,  
                             Crypt (pairK(A,B)) (Nonce Nb)  
            set evs "
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
done

lemma Na_authentic_A_Card: 
     " Inputs A (Card A)   
             Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
                Cert1, Cert2, Cert3  set evs; 
         A  Spy; evs  sr    
      Outpts (Card A) A Nonce Na, Cert3  
            set evs"
apply (blast dest: Inputs_A_Card_9)
done

(* The last three theorems for Card A can be put togheter trivially.
They are separated to highlight the different requirements on agents
and their cards.*)


(*Alternatively:
  A ≠ Spy; B ∉ bad; Card A ∉ cloned; Card B ∉ cloned; evs ∈ sr ⟧ *)
lemma Inputs_A_Card_9_authentic: 
  " Inputs A (Card A)   
             Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
               Crypt (shrK A) Nonce Pk, Agent B,  
               Crypt (pairK(A,B)) Nonce Na, Nonce Nb, Cert3  set evs; 
    A  Spy; Card A  cloned;¬illegalUse(Card B); evs  sr    
      Says Server A Nonce Pk, Crypt (shrK A) Nonce Pk, Agent B   
            set evs   
         Outpts (Card B) B Nonce Nb, Key (sesK(Nb, pairK (A, B))),    
                             Crypt (pairK(A,B)) Nonce Na, Nonce Nb,  
                             Crypt (pairK(A,B)) (Nonce Nb)  
            set evs   
         Outpts (Card A) A Nonce Na, Cert3  
            set evs"
apply (blast dest: Inputs_A_Card_9 Na_Nb_certificate_authentic Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
done

(*MSG8
Nothing to prove because the message is a cleartext that comes from the 
network*)

(*Other messages: nothing to prove because the verifiers involved are new*)


(*END further theorems about authenticity of verifiers*)



(* BEGIN trivial guarantees on outputs for agents *)

(*MSG4*)
lemma SR4_imp: 
     " Outpts (Card A) A Nonce Na, Crypt (crdK (Card A)) (Nonce Na) 
            set evs;  
         A  Spy; evs  sr                  
       Pk V. Gets A Pk, V  set evs"
apply (blast dest: Outpts_A_Card_4 Inputs_A_Card_3)
done
(*weak: could strengthen the model adding verifier for the Pairkey to msg3*)


(*MSG7*)
lemma SR7_imp: 
     " Outpts (Card B) B Nonce Nb, Key K,  
                      Crypt (pairK(A,B)) Nonce Na, Nonce Nb,  
                      Cert2  set evs;  
         B  Spy; evs  sr   
      Gets B Agent A, Nonce Na  set evs"
apply (blast dest: Outpts_B_Card_7 Inputs_B_Card_6)
done

(*MSG10*)
lemma SR10_imp: 
     " Outpts (Card A) A Key K, Crypt (pairK(A,B)) (Nonce Nb)  
            set evs;  
         A  Spy; evs  sr   
       Cert1 Cert2.  
                   Gets A Nonce (Pairkey (A, B)), Cert1  set evs   
                   Gets A Nonce Nb, Cert2  set evs"
apply (blast dest: Outpts_A_Card_10 Inputs_A_Card_9)
done


(*END trivial guarantees on outputs for agents*)



(*INTEGRITY*)
lemma Outpts_Server_not_evs: "evs  sr  Outpts (Card Server) P X  set evs"
apply (erule sr.induct)
apply auto
done

texttermstep2_integrity also is a reliability theorem
lemma Says_Server_message_form: 
     " Says Server A Pk, Certificate  set evs;  
         evs  sr                    
       B. Pk = Nonce (Pairkey(A,B))   
         Certificate = Crypt (shrK A) Nonce (Pairkey(A,B)), Agent B"
apply (erule rev_mp)
apply (erule sr.induct)
apply auto
apply (blast dest!: Outpts_Server_not_evs)+
done
(*cannot be made useful to A in form of a Gets event*)

text
  step4integrity is termOutpts_A_Card_form_4

  step7integrity is termOutpts_B_Card_form_7


lemma step8_integrity: 
     " Says B A Nonce Nb, Certificate  set evs;  
         B  Server; B  Spy; evs  sr                    
       Cert2 K.   
          Outpts (Card B) B Nonce Nb, Key K, Certificate, Cert2  set evs"
apply (erule rev_mp)
apply (erule sr.induct)
prefer 18 apply (fastforce dest: Outpts_A_Card_form_10)
apply auto
done


textstep9integrity is termInputs_A_Card_form_9

        step10integrity is termOutpts_A_Card_form_10.


lemma step11_integrity: 
     " Says A B (Certificate)  set evs; 
          p q. Certificate  p, q;  
         A  Spy; evs  sr   
       K.  
            Outpts (Card A) A Key K, Certificate  set evs"
apply (erule rev_mp)
apply (erule sr.induct)
apply auto
done

end