src/HOL/Auth/WooLam.thy
changeset 23746 a455e69c31cc
parent 16417 9bc16273c2d4
child 37936 1e4c5015a72e
     1.1 --- a/src/HOL/Auth/WooLam.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -18,9 +18,8 @@
     1.4    Computer Security Foundations Workshop
     1.5  *}
     1.6  
     1.7 -consts  woolam  :: "event list set"
     1.8 -inductive woolam
     1.9 -  intros
    1.10 +inductive_set woolam :: "event list set"
    1.11 +  where
    1.12           (*Initial trace is empty*)
    1.13     Nil:  "[] \<in> woolam"
    1.14  
    1.15 @@ -29,20 +28,20 @@
    1.16           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.17             invent new nonces here, but he can also use NS1.  Common to
    1.18             all similar protocols.*)
    1.19 -   Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
    1.20 + | Fake: "[| evsf \<in> woolam;  X \<in> synth (analz (spies evsf)) |]
    1.21            ==> Says Spy B X  # evsf \<in> woolam"
    1.22  
    1.23           (*Alice initiates a protocol run*)
    1.24 -   WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
    1.25 + | WL1:  "evs1 \<in> woolam ==> Says A B (Agent A) # evs1 \<in> woolam"
    1.26  
    1.27           (*Bob responds to Alice's message with a challenge.*)
    1.28 -   WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
    1.29 + | WL2:  "[| evs2 \<in> woolam;  Says A' B (Agent A) \<in> set evs2 |]
    1.30            ==> Says B A (Nonce NB) # evs2 \<in> woolam"
    1.31  
    1.32           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.33             B is *not* properly determined -- Alice essentially broadcasts
    1.34             her reply.*)
    1.35 -   WL3:  "[| evs3 \<in> woolam;
    1.36 + | WL3:  "[| evs3 \<in> woolam;
    1.37               Says A  B (Agent A)  \<in> set evs3;
    1.38               Says B' A (Nonce NB) \<in> set evs3 |]
    1.39            ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \<in> woolam"
    1.40 @@ -51,13 +50,13 @@
    1.41             the messages are shown in chronological order, for clarity.
    1.42             But here, exchanging the two events would cause the lemma
    1.43             WL4_analz_spies to pick up the wrong assumption!*)
    1.44 -   WL4:  "[| evs4 \<in> woolam;
    1.45 + | WL4:  "[| evs4 \<in> woolam;
    1.46               Says A'  B X         \<in> set evs4;
    1.47               Says A'' B (Agent A) \<in> set evs4 |]
    1.48            ==> Says B Server {|Agent A, Agent B, X|} # evs4 \<in> woolam"
    1.49  
    1.50           (*Server decrypts Alice's response for Bob.*)
    1.51 -   WL5:  "[| evs5 \<in> woolam;
    1.52 + | WL5:  "[| evs5 \<in> woolam;
    1.53               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.54                 \<in> set evs5 |]
    1.55            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})