src/HOL/Auth/Yahalom2.thy
changeset 14200 d8598e24f8fa
parent 13956 8fe7e12290e1
child 14207 f20fbb141673
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:40:27 2003 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 23 15:41:33 2003 +0200
     1.3 @@ -80,14 +80,16 @@
     1.4  declare analz_into_parts [dest]
     1.5  
     1.6  text{*A "possibility property": there are traces that reach the end*}
     1.7 -lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
     1.8 +lemma "Key K \<notin> used []
     1.9 +       ==> \<exists>X NB. \<exists>evs \<in> yahalom.
    1.10               Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
    1.11  apply (intro exI bexI)
    1.12  apply (rule_tac [2] yahalom.Nil
    1.13                      [THEN yahalom.YM1, THEN yahalom.Reception,
    1.14                       THEN yahalom.YM2, THEN yahalom.Reception,
    1.15                       THEN yahalom.YM3, THEN yahalom.Reception,
    1.16 -                     THEN yahalom.YM4], possibility)
    1.17 +                     THEN yahalom.YM4])
    1.18 +apply (possibility, simp add: used_Cons) 
    1.19  done
    1.20  
    1.21  lemma Gets_imp_Says: