Theory ZhouGollmann

(*  Title:      HOL/Auth/ZhouGollmann.thy
    Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
    Copyright   2003  University of Cambridge

The protocol of
  Jianying Zhou and Dieter Gollmann,
  A Fair Non-Repudiation Protocol,
  Security and Privacy 1996 (Oakland)
  55-61
*)

theory ZhouGollmann imports Public begin

abbreviation
  TTP :: agent where "TTP == Server"

abbreviation f_sub :: nat where "f_sub == 5"
abbreviation f_nro :: nat where "f_nro == 2"
abbreviation f_nrr :: nat where "f_nrr == 3"
abbreviation f_con :: nat where "f_con == 4"


definition broken :: "agent set" where    
    ― ‹the compromised honest agents; TTP is included as it's not allowed to
        use the protocol
   "broken == bad - {Spy}"

declare broken_def [simp]

inductive_set zg :: "event list set"
  where

  Nil:  "[]  zg"

| Fake: "[| evsf  zg;  X  synth (analz (spies evsf)) |]
         ==> Says Spy B X  # evsf  zg"

| Reception:  "[| evsr  zg; Says A B X  set evsr |] ==> Gets B X # evsr  zg"

  (*L is fresh for honest agents.
    We don't require K to be fresh because we don't bother to prove secrecy!
    We just assume that the protocol's objective is to deliver K fairly,
    rather than to keep M secret.*)
| ZG1: "[| evs1  zg;  Nonce L  used evs1; C = Crypt K (Number m);
           K  symKeys;
           NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, C|]
       ==> Says A B Number f_nro, Agent B, Nonce L, C, NRO # evs1  zg"

  (*B must check that NRO is A's signature to learn the sender's name*)
| ZG2: "[| evs2  zg;
           Gets B Number f_nro, Agent B, Nonce L, C, NRO  set evs2;
           NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, C;
           NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, C|]
       ==> Says B A Number f_nrr, Agent A, Nonce L, NRR # evs2    zg"

  (*A must check that NRR is B's signature to learn the sender's name;
    without spy, the matching label would be enough*)
| ZG3: "[| evs3  zg; C = Crypt K M; K  symKeys;
           Says A B Number f_nro, Agent B, Nonce L, C, NRO  set evs3;
           Gets A Number f_nrr, Agent A, Nonce L, NRR  set evs3;
           NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, C;
           sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K|]
       ==> Says A TTP Number f_sub, Agent B, Nonce L, Key K, sub_K
             # evs3  zg"

 (*TTP checks that sub_K is A's signature to learn who issued K, then
   gives credentials to A and B.  The Notes event models the availability of
   the credentials, but the act of fetching them is not modelled.  We also
   give con_K to the Spy. This makes the threat model more dangerous, while 
   also allowing lemma @{text Crypt_used_imp_spies} to omit the condition
   @{term "K ≠ priK TTP"}. *)
| ZG4: "[| evs4  zg; K  symKeys;
           Gets TTP Number f_sub, Agent B, Nonce L, Key K, sub_K
              set evs4;
           sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
           con_K = Crypt (priK TTP) Number f_con, Agent A, Agent B,
                                      Nonce L, Key K|]
       ==> Says TTP Spy con_K
           #
           Notes TTP Number f_con, Agent A, Agent B, Nonce L, Key K, con_K
           # evs4  zg"


declare Says_imp_knows_Spy [THEN analz.Inj, dest]
declare Fake_parts_insert_in_Un  [dest]
declare analz_into_parts [dest]

declare symKey_neq_priEK [simp]
declare symKey_neq_priEK [THEN not_sym, simp]


textA "possibility property": there are traces that reach the end
lemma "[|A  B; TTP  A; TTP  B; K  symKeys|] ==>
     L. evs  zg.
           Notes TTP Number f_con, Agent A, Agent B, Nonce L, Key K,
               Crypt (priK TTP) Number f_con, Agent A, Agent B, Nonce L, Key K
                set evs"
apply (intro exI bexI)
apply (rule_tac [2] zg.Nil
                    [THEN zg.ZG1, THEN zg.Reception [of _ A B],
                     THEN zg.ZG2, THEN zg.Reception [of _ B A],
                     THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
                     THEN zg.ZG4])
apply (basic_possibility, auto)
done

subsection Basic Lemmas

lemma Gets_imp_Says:
     "[| Gets B X  set evs; evs  zg |] ==> A. Says A B X  set evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
done

lemma Gets_imp_knows_Spy:
     "[| Gets B X  set evs; evs  zg |]  ==> X  spies evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)


textLets us replace proofs about termused evs by simpler proofs 
about termparts (spies evs).
lemma Crypt_used_imp_spies:
     "[| Crypt K X  used evs; evs  zg |]
      ==> Crypt K X  parts (spies evs)"
apply (erule rev_mp)
apply (erule zg.induct)
apply (simp_all add: parts_insert_knows_A) 
done

lemma Notes_TTP_imp_Gets:
     "[|Notes TTP Number f_con, Agent A, Agent B, Nonce L, Key K, con_K
            set evs;
        sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
        evs  zg|]
    ==> Gets TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
done

textFor reasoning about C, which is encrypted in message ZG2
lemma ZG2_msg_in_parts_spies:
     "[|Gets B F, B', L, C, X  set evs; evs  zg|]
      ==> C  parts (spies evs)"
by (blast dest: Gets_imp_Says)

(*classical regularity lemma on priK*)
lemma Spy_see_priK [simp]:
     "evs  zg ==> (Key (priK A)  parts (spies evs)) = (A  bad)"
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
done

textSo that blast can use it too
declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]

lemma Spy_analz_priK [simp]:
     "evs  zg ==> (Key (priK A)  analz (spies evs)) = (A  bad)"
by auto 


subsectionAbout NRO: Validity for termB

textBelow we prove that if termNRO exists then termA definitely
sent it, provided termA is not broken.

textStrong conclusion for a good agent
lemma NRO_validity_good:
     "[|NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, C;
        NRO  parts (spies evs);
        A  bad;  evs  zg |]
     ==> Says A B Number f_nro, Agent B, Nonce L, C, NRO  set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
done

lemma NRO_sender:
     "[|Says A' B n, b, l, C, Crypt (priK A) X  set evs; evs  zg|]
    ==> A'  {A,Spy}"
apply (erule rev_mp)  
apply (erule zg.induct, simp_all)
done

textHolds also for termA = Spy!
theorem NRO_validity:
     "[|Gets B Number f_nro, Agent B, Nonce L, C, NRO  set evs;
        NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, C;
        A  broken;  evs  zg |]
     ==> Says A B Number f_nro, Agent B, Nonce L, C, NRO  set evs"
apply (drule Gets_imp_Says, assumption) 
apply clarify 
apply (frule NRO_sender, auto)
txtWe are left with the case where the sender is termSpy and not
  equal to termA, because termA  bad. 
  Thus theorem NRO_validity_good› applies.
apply (blast dest: NRO_validity_good [OF refl])
done


subsectionAbout NRR: Validity for termA

textBelow we prove that if termNRR exists then termB definitely
sent it, provided termB is not broken.

textStrong conclusion for a good agent
lemma NRR_validity_good:
     "[|NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, C;
        NRR  parts (spies evs);
        B  bad;  evs  zg |]
     ==> Says B A Number f_nrr, Agent A, Nonce L, NRR  set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct) 
apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
done

lemma NRR_sender:
     "[|Says B' A n, a, l, Crypt (priK B) X  set evs; evs  zg|]
    ==> B'  {B,Spy}"
apply (erule rev_mp)  
apply (erule zg.induct, simp_all)
done

textHolds also for termB = Spy!
theorem NRR_validity:
     "[|Says B' A Number f_nrr, Agent A, Nonce L, NRR  set evs;
        NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, C;
        B  broken; evs  zg|]
    ==> Says B A Number f_nrr, Agent A, Nonce L, NRR  set evs"
apply clarify 
apply (frule NRR_sender, auto)
txtWe are left with the case where termB' = Spy and  termB'  B,
  i.e. termB  bad, when we can apply NRR_validity_good›.
 apply (blast dest: NRR_validity_good [OF refl])
done


subsectionProofs About termsub_K

textBelow we prove that if termsub_K exists then termA definitely
sent it, provided termA is not broken.

textStrong conclusion for a good agent
lemma sub_K_validity_good:
     "[|sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
        sub_K  parts (spies evs);
        A  bad;  evs  zg |]
     ==> Says A TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txtFake 
apply (blast dest!: Fake_parts_sing_imp_Un)
done

lemma sub_K_sender:
     "[|Says A' TTP n, b, l, k, Crypt (priK A) X  set evs;  evs  zg|]
    ==> A'  {A,Spy}"
apply (erule rev_mp)  
apply (erule zg.induct, simp_all)
done

textHolds also for termA = Spy!
theorem sub_K_validity:
     "[|Gets TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs;
        sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
        A  broken;  evs  zg |]
     ==> Says A TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs"
apply (drule Gets_imp_Says, assumption) 
apply clarify 
apply (frule sub_K_sender, auto)
txtWe are left with the case where the sender is termSpy and not
  equal to termA, because termA  bad. 
  Thus theorem sub_K_validity_good› applies.
apply (blast dest: sub_K_validity_good [OF refl])
done



subsectionProofs About termcon_K

textBelow we prove that if termcon_K exists, then termTTP has it,
and therefore termA and termB) can get it too.  Moreover, we know
that termA sent termsub_K

lemma con_K_validity:
     "[|con_K  used evs;
        con_K = Crypt (priK TTP)
                  Number f_con, Agent A, Agent B, Nonce L, Key K;
        evs  zg |]
    ==> Notes TTP Number f_con, Agent A, Agent B, Nonce L, Key K, con_K
           set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txtFake
apply (blast dest!: Fake_parts_sing_imp_Un)
txtZG2 
apply (blast dest: parts_cut)
done

textIf termTTP holds termcon_K then termA sent
 termsub_K.  We assume that termA is not broken.  Importantly, nothing
  needs to be assumed about the form of termcon_K!
lemma Notes_TTP_imp_Says_A:
     "[|Notes TTP Number f_con, Agent A, Agent B, Nonce L, Key K, con_K
            set evs;
        sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
        A  broken; evs  zg|]
     ==> Says A TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txtZG4
apply clarify 
apply (rule sub_K_validity, auto) 
done

textIf termcon_K exists, then termA sent termsub_K.  We again
   assume that termA is not broken.
theorem B_sub_K_validity:
     "[|con_K  used evs;
        con_K = Crypt (priK TTP) Number f_con, Agent A, Agent B,
                                   Nonce L, Key K;
        sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
        A  broken; evs  zg|]
     ==> Says A TTP Number f_sub, Agent B, Nonce L, Key K, sub_K  set evs"
by (blast dest: con_K_validity Notes_TTP_imp_Says_A)


subsectionProving fairness

textCannot prove that, if termB has NRO, then  termA has her NRR.
It would appear that termB has a small advantage, though it is
useless to win disputes: termB needs to present termcon_K as well.

textStrange: unicity of the label protects termA?
lemma A_unicity: 
     "[|NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, Crypt K M;
        NRO  parts (spies evs);
        Says A B Number f_nro, Agent B, Nonce L, Crypt K M', NRO'
           set evs;
        A  bad; evs  zg |]
     ==> M'=M"
apply clarify
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
txtZG1: freshness
apply (blast dest: parts.Body) 
done


textFairness lemma: if termsub_K exists, then termA holds 
NRR.  Relies on unicity of labels.
lemma sub_K_implies_NRR:
     "[| NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, Crypt K M;
         NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, Crypt K M;
         sub_K  parts (spies evs);
         NRO  parts (spies evs);
         sub_K = Crypt (priK A) Number f_sub, Agent B, Nonce L, Key K;
         A  bad;  evs  zg |]
     ==> Gets A Number f_nrr, Agent A, Nonce L, NRR  set evs"
apply clarify
apply hypsubst_thin
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txtFake
apply blast 
txtZG1: freshness
apply (blast dest: parts.Body) 
txtZG3 
apply (blast dest: A_unicity [OF refl]) 
done


lemma Crypt_used_imp_L_used:
     "[| Crypt (priK TTP) F, A, B, L, K  used evs; evs  zg |]
      ==> L  used evs"
apply (erule rev_mp)
apply (erule zg.induct, auto)
txtFake
apply (blast dest!: Fake_parts_sing_imp_Un)
txtZG2: freshness
apply (blast dest: parts.Body) 
done


textFairness for termA: if termcon_K and termNRO exist, 
then termA holds NRR.  termA must be uncompromised, but there is no
assumption about termB.
theorem A_fairness_NRO:
     "[|con_K  used evs;
        NRO  parts (spies evs);
        con_K = Crypt (priK TTP)
                      Number f_con, Agent A, Agent B, Nonce L, Key K;
        NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, Crypt K M;
        NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, Crypt K M;
        A  bad;  evs  zg |]
    ==> Gets A Number f_nrr, Agent A, Nonce L, NRR  set evs"
apply clarify
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   txtFake
   apply (simp add: parts_insert_knows_A) 
   apply (blast dest: Fake_parts_sing_imp_Un) 
  txtZG1
  apply (blast dest: Crypt_used_imp_L_used) 
 txtZG2
 apply (blast dest: parts_cut)
txtZG4 
apply (blast intro: sub_K_implies_NRR [OF refl] 
             dest: Gets_imp_knows_Spy [THEN parts.Inj])
done

textFairness for termB: NRR exists at all, then termB holds NRO.
termB must be uncompromised, but there is no assumption about termA.
theorem B_fairness_NRR:
     "[|NRR  used evs;
        NRR = Crypt (priK B) Number f_nrr, Agent A, Nonce L, C;
        NRO = Crypt (priK A) Number f_nro, Agent B, Nonce L, C;
        B  bad; evs  zg |]
    ==> Gets B Number f_nro, Agent B, Nonce L, C, NRO  set evs"
apply clarify
apply (erule rev_mp)
apply (erule zg.induct)
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
txtFake
apply (blast dest!: Fake_parts_sing_imp_Un)
txtZG2
apply (blast dest: parts_cut)
done


textIf termcon_K exists at all, then termB can get it, by con_K_validity›.  Cannot conclude that also NRO is available to termB,
because if termA were unfair, termA could build message 3 without
building message 1, which contains NRO.

end