src/HOL/Auth/Yahalom.ML

 
 Pretty.setdepth 25;
 
 
 (*A "possibility property": there are traces that reach the end*)
-Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
+Goal "A ~= Server \
 \     ==> EX X NB K. EX evs: yahalom.          \
 \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
           yahalom.YM4) 2);
 by possibility_tac;
 result();
 
 
 (**** Inductive proofs about yahalom ****)
-
-(*Nobody sends themselves messages*)
-Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
-by (etac yahalom.induct 1);
-by Auto_tac;
-qed_spec_mp "not_Says_to_self";
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
 
 
 (** For reasoning about the encrypted portion of messages **)
 
 (*Lets us treat YM4 using a similar argument as for the Fake case.*)

 
 
 (*Describes the form of K when the Server sends this message.  Useful for
   Oops as well as main secrecy property.*)
 Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
-\          : set evs;                                                   \
-\        evs : yahalom |]                                          \
+\          : set evs;   evs : yahalom |]                                \
 \     ==> K ~: range shrK";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);