src/HOL/Auth/OtwayRees.thy

   Burrows, Abadi and Needham (1989).  A Logic of Authentication.
   Proc. Royal Soc. 426
 
 This is the original version, which encrypts Nonce NB.*}
 
-consts  otway   :: "event list set"
-inductive "otway"
-  intros
+inductive_set otway :: "event list set"
+  where
          (*Initial trace is empty*)
    Nil:  "[] \<in> otway"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-   Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
+ | Fake: "[| evsf \<in> otway;  X \<in> synth (analz (knows Spy evsf)) |]
           ==> Says Spy B X  # evsf \<in> otway"
 
          (*A message that has been sent can be received by the
            intended recipient.*)
-   Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
+ | Reception: "[| evsr \<in> otway;  Says A B X \<in>set evsr |]
                ==> Gets B X # evsr \<in> otway"
 
          (*Alice initiates a protocol run*)
-   OR1:  "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
+ | OR1:  "[| evs1 \<in> otway;  Nonce NA \<notin> used evs1 |]
           ==> Says A B {|Nonce NA, Agent A, Agent B,
                          Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
                  # evs1 : otway"
 
          (*Bob's response to Alice's message.  Note that NB is encrypted.*)
-   OR2:  "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
+ | OR2:  "[| evs2 \<in> otway;  Nonce NB \<notin> used evs2;
              Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
           ==> Says B Server
                   {|Nonce NA, Agent A, Agent B, X,
                     Crypt (shrK B)
                       {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                  # evs2 : otway"
 
          (*The Server receives Bob's message and checks that the three NAs
            match.  Then he sends a new session key to Bob with a packet for
            forwarding to Alice.*)
-   OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
+ | OR3:  "[| evs3 \<in> otway;  Key KAB \<notin> used evs3;
              Gets Server
                   {|Nonce NA, Agent A, Agent B,
                     Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
                     Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set evs3 |]

                  # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.
            Need B \<noteq> Server because we allow messages to self.*)
-   OR4:  "[| evs4 \<in> otway;  B \<noteq> Server;
+ | OR4:  "[| evs4 \<in> otway;  B \<noteq> Server;
              Says B Server {|Nonce NA, Agent A, Agent B, X',
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
                : set evs4;
              Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs4 |]
           ==> Says B A {|Nonce NA, X|} # evs4 : otway"
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.*)
-   Oops: "[| evso \<in> otway;
+ | Oops: "[| evso \<in> otway;
              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evso |]
           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"