src/HOL/Auth/ZhouGollmann.thy
changeset 14146 0edd2d57eaf8
parent 14145 2e31b8cc8788
child 14207 f20fbb141673
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Tue Aug 12 13:35:03 2003 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Wed Aug 13 12:28:53 2003 +0200
     1.3 @@ -101,6 +101,21 @@
     1.4  declare symKey_neq_priEK [THEN not_sym, simp]
     1.5  
     1.6  
     1.7 +text{*A "possibility property": there are traces that reach the end*}
     1.8 +lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
     1.9 +     \<exists>L. \<exists>evs \<in> zg.
    1.10 +           Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K,
    1.11 +               Crypt (priK TTP) {|Number f_con, Agent A, Agent B, Nonce L, Key K|} |}
    1.12 +               \<in> set evs"
    1.13 +apply (intro exI bexI)
    1.14 +apply (rule_tac [2] zg.Nil
    1.15 +                    [THEN zg.ZG1, THEN zg.Reception [of _ A B],
    1.16 +                     THEN zg.ZG2, THEN zg.Reception [of _ B A],
    1.17 +                     THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 
    1.18 +                     THEN zg.ZG4])
    1.19 +apply (possibility, auto)
    1.20 +done
    1.21 +
    1.22  subsection {*Basic Lemmas*}
    1.23  
    1.24  lemma Gets_imp_Says: