Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/OtwayRees_Bad.thy
changeset 14200 d8598e24f8fa
parent 13507 febb8e5d2a9d
child 14207 f20fbb141673 
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:40:27 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 23 15:41:33 2003 +0200
@@ -90,15 +90,16 @@
 declare Fake_parts_insert_in_Un  [dest]
 
 (*A "possibility property": there are traces that reach the end*)
-lemma "B \<noteq> Server
-      ==> \<exists>K. \<exists>NA. \<exists>evs \<in> otway.
+lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
+      ==> \<exists>NA. \<exists>evs \<in> otway.
             Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
               \<in> set evs"
 apply (intro exI bexI)
 apply (rule_tac [2] otway.Nil
                     [THEN otway.OR1, THEN otway.Reception,
                      THEN otway.OR2, THEN otway.Reception,
-                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
+                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
+apply (possibility, simp add: used_Cons) 
 done
 
 lemma Gets_imp_Says [dest!]:
isabelle