# Theory ZhouGollmann

Up to index of Isabelle/HOL/Auth

theory ZhouGollmann
imports Public
begin

    (*  Title:      HOL/Auth/ZhouGollmann
        ID:         $Id: ZhouGollmann.thy,v 1.8 2005/06/17 14:13:06 haftmann Exp $
        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

    syntax
      TTP :: agent

    translations
      "TTP" == " Server "

    syntax
      f_sub :: nat
      f_nro :: nat
      f_nrr :: nat
      f_con :: nat

    translations
      "f_sub" == " 5 "
      "f_nro" == " 2 "
      "f_nrr" == " 3 "
      "f_con" == " 4 "

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

    declare broken_def [simp]

    consts  zg  :: "event list set"

    inductive zg
      intros

      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]

    text{*A "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 (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)

    text{*Lets us replace proofs about @{term "used evs"} by simpler proofs
    about @{term "parts (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

    text{*For 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

    text{*So 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

    subsection{*About NRO: Validity for @{term B}*}

    text{*Below we prove that if @{term NRO} exists then @{term A} definitely
    sent it, provided @{term A} is not broken.*}

    text{*Strong 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

    text{*Holds also for @{term "A = 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)
    txt{*We are left with the case where the sender is @{term Spy} and not
      equal to @{term A}, because @{term "A ∉ bad"}.
      Thus theorem @{text NRO_validity_good} applies.*}
    apply (blast dest: NRO_validity_good [OF refl])
    done

    subsection{*About NRR: Validity for @{term A}*}

    text{*Below we prove that if @{term NRR} exists then @{term B} definitely
    sent it, provided @{term B} is not broken.*}

    text{*Strong 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

    text{*Holds also for @{term "B = 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)
    txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' ≠ B"},
      i.e. @{term "B ∉ bad"}, when we can apply @{text NRR_validity_good}.*}
     apply (blast dest: NRR_validity_good [OF refl])
    done

    subsection{*Proofs About @{term sub_K}*}

    text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
    sent it, provided @{term A} is not broken.  *}

    text{*Strong 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)
    txt{*Fake*}
    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

    text{*Holds also for @{term "A = 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)
    txt{*We are left with the case where the sender is @{term Spy} and not
      equal to @{term A}, because @{term "A ∉ bad"}.
      Thus theorem @{text sub_K_validity_good} applies.*}
    apply (blast dest: sub_K_validity_good [OF refl])
    done

    subsection{*Proofs About @{term con_K}*}

    text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
    and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
    that @{term A} sent @{term sub_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)
    txt{*Fake*}
    apply (blast dest!: Fake_parts_sing_imp_Un)
    txt{*ZG2*}
    apply (blast dest: parts_cut)
    done

    text{*If @{term TTP} holds @{term con_K} then @{term A} sent
     @{term sub_K}.  We assume that @{term A} is not broken.  Importantly, nothing
      needs to be assumed about the form of @{term con_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)
    txt{*ZG4*}
    apply clarify
    apply (rule sub_K_validity, auto)
    done

    text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
       assume that @{term A} 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)

    subsection{*Proving fairness*}

    text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
    It would appear that @{term B} has a small advantage, though it is
    useless to win disputes: @{term B} needs to present @{term con_K} as well.*}

    text{*Strange: unicity of the label protects @{term A}?*}
    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)
    txt{*ZG1: freshness*}
    apply (blast dest: parts.Body)
    done

    text{*Fairness lemma: if @{term sub_K} exists, then @{term A} 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 (erule rev_mp)
    apply (erule rev_mp)
    apply (erule zg.induct)
    apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
    txt{*Fake*}
    apply blast
    txt{*ZG1: freshness*}
    apply (blast dest: parts.Body)
    txt{*ZG3*}
    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)
    txt{*Fake*}
    apply (blast dest!: Fake_parts_sing_imp_Un)
    txt{*ZG2: freshness*}
    apply (blast dest: parts.Body)
    done

    text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist,
    then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
    assumption about @{term B}.*}
    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)
       txt{*Fake*}
       apply (simp add: parts_insert_knows_A)
       apply (blast dest: Fake_parts_sing_imp_Un)
      txt{*ZG1*}
      apply (blast dest: Crypt_used_imp_L_used)
     txt{*ZG2*}
     apply (blast dest: parts_cut)
    txt{*ZG4*}
    apply (blast intro: sub_K_implies_NRR [OF refl]
                 dest: Gets_imp_knows_Spy [THEN parts.Inj])
    done

    text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
    @{term B} must be uncompromised, but there is no assumption about @{term
    A}. *}
    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)
    txt{*Fake*}
    apply (blast dest!: Fake_parts_sing_imp_Un)
    txt{*ZG2*}
    apply (blast dest: parts_cut)
    done

    text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
    con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
    because if @{term A} were unfair, @{term A} could build message 3 without
    building message 1, which contains NRO. *}

    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 (priEK TTP)
                     {|Number f_con, Agent A, Agent B, Nonce L, Key K|}|}
                 ∈ set evs

### Basic Lemmas

lemma Gets_imp_Says:

      [| Gets B X ∈ set evs; evs ∈ zg |] ==> ∃A. Says A B X ∈ set evs

lemma Gets_imp_knows_Spy:

      [| Gets B X ∈ set evs; evs ∈ zg |] ==> X ∈ knows Spy evs

lemma Crypt_used_imp_spies:

      [| Crypt K X ∈ used evs; evs ∈ zg |] ==> Crypt K X ∈ parts (knows Spy evs)

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 (priEK 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

lemma ZG2_msg_in_parts_spies:

      [| Gets B {|F, B', L, C, X|} ∈ set evs; evs ∈ zg |]
      ==> C ∈ parts (knows Spy evs)

lemma Spy_see_priK:

      evs ∈ zg ==> (Key (priEK A) ∈ parts (knows Spy evs)) = (A ∈ bad)

lemma Spy_analz_priK:

      evs ∈ zg ==> (Key (priEK A) ∈ analz (knows Spy evs)) = (A ∈ bad)

### About NRO: Validity for @{term B}

lemma NRO_validity_good:

      [| NRO = Crypt (priEK A) {|Number f_nro, Agent B, Nonce L, C|};
         NRO ∈ parts (knows Spy evs); A ∉ bad; evs ∈ zg |]
      ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} ∈ set evs

lemma NRO_sender:

      [| Says A' B {|n, b, l, C, Crypt (priEK A) X|} ∈ set evs; evs ∈ zg |]
      ==> A' ∈ {A, Spy}

theorem NRO_validity:

      [| Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} ∈ set evs;
         NRO = Crypt (priEK 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

### About NRR: Validity for @{term A}

lemma NRR_validity_good:

      [| NRR = Crypt (priEK B) {|Number f_nrr, Agent A, Nonce L, C|};
         NRR ∈ parts (knows Spy evs); B ∉ bad; evs ∈ zg |]
      ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} ∈ set evs

lemma NRR_sender:

      [| Says B' A {|n, a, l, Crypt (priEK B) X|} ∈ set evs; evs ∈ zg |]
      ==> B' ∈ {B, Spy}

theorem NRR_validity:

      [| Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} ∈ set evs;
         NRR = Crypt (priEK 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

### Proofs About @{term sub_K}

lemma sub_K_validity_good:

      [| sub_K = Crypt (priEK A) {|Number f_sub, Agent B, Nonce L, Key K|};
         sub_K ∈ parts (knows Spy evs); A ∉ bad; evs ∈ zg |]
      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} ∈ set evs

lemma sub_K_sender:

      [| Says A' TTP {|n, b, l, k, Crypt (priEK A) X|} ∈ set evs; evs ∈ zg |]
      ==> A' ∈ {A, Spy}

theorem sub_K_validity:

      [| Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} ∈ set evs;
         sub_K = Crypt (priEK 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

### Proofs About @{term con_K}

lemma con_K_validity:

      [| con_K ∈ used evs;
         con_K = Crypt (priEK 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

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 (priEK 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

theorem B_sub_K_validity:

      [| con_K ∈ used evs;
         con_K = Crypt (priEK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
         sub_K = Crypt (priEK 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

### Proving fairness

lemma A_unicity:

      [| NRO = Crypt (priEK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
         NRO ∈ parts (knows Spy evs);
         Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|} ∈ set evs;
         A ∉ bad; evs ∈ zg |]
      ==> M' = M

lemma sub_K_implies_NRR:

      [| NRO = Crypt (priEK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
         NRR = Crypt (priEK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
         sub_K ∈ parts (knows Spy evs); NRO ∈ parts (knows Spy evs);
         sub_K = Crypt (priEK 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

lemma Crypt_used_imp_L_used:

      [| Crypt (priEK TTP) {|F, A, B, L, K|} ∈ used evs; evs ∈ zg |] ==> L ∈ used evs

theorem A_fairness_NRO:

      [| con_K ∈ used evs; NRO ∈ parts (knows Spy evs);
         con_K = Crypt (priEK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
         NRO = Crypt (priEK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
         NRR = Crypt (priEK 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

theorem B_fairness_NRR:

      [| NRR ∈ used evs; NRR = Crypt (priEK B) {|Number f_nrr, Agent A, Nonce L, C|};
         NRO = Crypt (priEK 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