# HG changeset patch
# User paulson
# Date 1060770533 -7200
# Node ID 0edd2d57eaf829c98cf185fab533366a3425747c
# Parent  2e31b8cc8788308bf6d47cf439cb08c2784b6a62
possibility proof!

diff -r 2e31b8cc8788 -r 0edd2d57eaf8 src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Tue Aug 12 13:35:03 2003 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Wed Aug 13 12:28:53 2003 +0200
@@ -101,6 +101,21 @@
 declare symKey_neq_priEK [THEN not_sym, simp]
 
 
+text{*A "possibility property": there are traces that reach the end*}
+lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==>
+     \<exists>L. \<exists>evs \<in> 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|} |}
+               \<in> 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: