src/HOL/Auth/WooLam.thy
changeset 23746 a455e69c31cc
parent 16417 9bc16273c2d4
child 37936 1e4c5015a72e
--- a/src/HOL/Auth/WooLam.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Auth/WooLam.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -18,9 +18,8 @@
   Computer Security Foundations Workshop
 *}
 
-consts  woolam  :: "event list set"
-inductive woolam
-  intros
+inductive_set woolam :: "event list set"
+  where
          (*Initial trace is empty*)
    Nil:  "[] \<in> woolam"
 
@@ -29,20 +28,20 @@
          (*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> woolam;  X \<in> synth (analz (spies evsf)) |]
+ | Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
           ==> Says Spy B X  # evsf \<in> woolam"
 
          (*Alice initiates a protocol run*)
-   WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
+ | WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
 
          (*Bob responds to Alice's message with a challenge.*)
-   WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
+ | WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
           ==> Says B A (Nonce NB) # evs2 \<in> woolam"
 
          (*Alice responds to Bob's challenge by encrypting NB with her key.
            B is *not* properly determined -- Alice essentially broadcasts
            her reply.*)
-   WL3:  "[| evs3 \<in> woolam;
+ | WL3:  "[| evs3 \<in> woolam;
              Says A  B (Agent A)  \<in> set evs3;
              Says B' A (Nonce NB) \<in> set evs3 |]
           ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
@@ -51,13 +50,13 @@
            the messages are shown in chronological order, for clarity.
            But here, exchanging the two events would cause the lemma
            WL4_analz_spies to pick up the wrong assumption!*)
-   WL4:  "[| evs4 \<in> woolam;
+ | WL4:  "[| evs4 \<in> woolam;
              Says A'  B X         \<in> set evs4;
              Says A'' B (Agent A) \<in> set evs4 |]
           ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
 
          (*Server decrypts Alice's response for Bob.*)
-   WL5:  "[| evs5 \<in> woolam;
+ | WL5:  "[| evs5 \<in> woolam;
              Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
                \<in> set evs5 |]
           ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})