src/HOL/Auth/NS_Shared.thy
changeset 14200 d8598e24f8fa
parent 13956 8fe7e12290e1
child 14207 f20fbb141673
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 23 15:40:27 2003 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 23 15:41:33 2003 +0200
     1.3 @@ -80,12 +80,14 @@
     1.4  
     1.5  
     1.6  text{*A "possibility property": there are traces that reach the end*}
     1.7 -lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
     1.8 -                              Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
     1.9 +lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
    1.10 +       ==> \<exists>N. \<exists>evs \<in> ns_shared.
    1.11 +                    Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    1.12  apply (intro exI bexI)
    1.13  apply (rule_tac [2] ns_shared.Nil
    1.14         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    1.15 -	THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
    1.16 +	THEN ns_shared.NS4, THEN ns_shared.NS5])
    1.17 +apply (possibility, simp add: used_Cons) 
    1.18  done
    1.19  
    1.20  (*This version is similar, while instantiating ?K and ?N to epsilon-terms