src/HOL/Auth/WooLam.thy
changeset 11185 1b737b4c2108
parent 5434 9b4bed3f394c
child 11251 a6816d47f41d
     1.1 --- a/src/HOL/Auth/WooLam.thy	Tue Feb 27 12:28:42 2001 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Feb 27 16:13:23 2001 +0100
     1.3 @@ -20,46 +20,46 @@
     1.4  inductive woolam
     1.5    intrs 
     1.6           (*Initial trace is empty*)
     1.7 -    Nil  "[]: woolam"
     1.8 +    Nil  "[] \\<in> woolam"
     1.9  
    1.10           (** These rules allow agents to send messages to themselves **)
    1.11  
    1.12           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.13             invent new nonces here, but he can also use NS1.  Common to
    1.14             all similar protocols.*)
    1.15 -    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
    1.16 -          ==> Says Spy B X  # evs : woolam"
    1.17 +    Fake "[| evsf \\<in> woolam;  X \\<in> synth (analz (spies evsf)) |]
    1.18 +          ==> Says Spy B X  # evsf \\<in> woolam"
    1.19  
    1.20           (*Alice initiates a protocol run*)
    1.21 -    WL1  "[| evs1: woolam |]
    1.22 -          ==> Says A B (Agent A) # evs1 : woolam"
    1.23 +    WL1  "[| evs1 \\<in> woolam |]
    1.24 +          ==> Says A B (Agent A) # evs1 \\<in> woolam"
    1.25  
    1.26           (*Bob responds to Alice's message with a challenge.*)
    1.27 -    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
    1.28 -          ==> Says B A (Nonce NB) # evs2 : woolam"
    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: woolam;
    1.36 -             Says A  B (Agent A)  : set evs3;
    1.37 -             Says B' A (Nonce NB) : set evs3 |]
    1.38 -          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
    1.39 +    WL3  "[| evs3 \\<in> woolam;
    1.40 +             Says A  B (Agent A)  \\<in> set evs3;
    1.41 +             Says B' A (Nonce NB) \\<in> set evs3 |]
    1.42 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 \\<in> woolam"
    1.43  
    1.44           (*Bob forwards Alice's response to the Server.  NOTE: usually
    1.45             the messages are shown in chronological order, for clarity.
    1.46             But here, exchanging the two events would cause the lemma
    1.47             WL4_analz_spies to pick up the wrong assumption!*)
    1.48 -    WL4  "[| evs4: woolam;  
    1.49 -             Says A'  B X         : set evs4;
    1.50 -             Says A'' B (Agent A) : set evs4 |]
    1.51 -          ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
    1.52 +    WL4  "[| evs4 \\<in> woolam;  
    1.53 +             Says A'  B X         \\<in> set evs4;
    1.54 +             Says A'' B (Agent A) \\<in> set evs4 |]
    1.55 +          ==> Says B Server {|Agent A, Agent B, X|} # evs4 \\<in> woolam"
    1.56  
    1.57           (*Server decrypts Alice's response for Bob.*)
    1.58 -    WL5  "[| evs5: woolam;  
    1.59 +    WL5  "[| evs5 \\<in> woolam;  
    1.60               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.61 -               : set evs5 |]
    1.62 +               \\<in> set evs5 |]
    1.63            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    1.64 -                 # evs5 : woolam"
    1.65 +                 # evs5 \\<in> woolam"
    1.66  
    1.67  end