src/HOL/Auth/OtwayRees_AN.ML

 
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
-\        ==> EX K. EX NA. EX evs: otway.                                 \
+\        ==> EX K. EX NA. EX evs: otway.                                      \
 \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \             : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
 by possibility_tac;

 goal thy 
  "!!evs. [| Says Server B                                           \
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
 \             : set evs;                                            \
-\           evs : otway |]                                     \
+\           evs : otway |]                                          \
 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);

 
 
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway ==>                                   \
-\      EX A' B' NA' NB'. ALL A B NA NB.                    \
-\       Says Server B                                      \
+ "!!evs. evs : otway ==>                                            \
+\      EX A' B' NA' NB'. ALL A B NA NB.                             \
+\       Says Server B                                               \
 \         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));

 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
     Does not in itself guarantee security: an attack could violate 
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
-\        ==> Says Server B                                                 \
-\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
-\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
-\            : set evs -->                                                 \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
+\        ==> Says Server B                                         \
+\             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
+\               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
+\            : set evs -->                                         \
+\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
 \            Key K ~: analz (sees Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac (!simpset addcongs [conj_cong]