src/HOL/Auth/WooLam.thy
changeset 2283 68829cf138fc
parent 2274 1b1b46adc9b3
child 2451 ce85a2aafc7a
     1.1 --- a/src/HOL/Auth/WooLam.thy	Fri Nov 29 15:31:13 1996 +0100
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Nov 29 17:58:18 1996 +0100
     1.3 @@ -16,47 +16,48 @@
     1.4  
     1.5  WooLam = Shared + 
     1.6  
     1.7 -consts  woolam   :: "agent set => event list set"
     1.8 -inductive "woolam lost"
     1.9 +consts  lost    :: agent set        (*No need for it to be a variable*)
    1.10 +	woolam  :: event list set
    1.11 +inductive woolam
    1.12    intrs 
    1.13           (*Initial trace is empty*)
    1.14 -    Nil  "[]: woolam lost"
    1.15 +    Nil  "[]: woolam"
    1.16  
    1.17           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.18             invent new nonces here, but he can also use NS1.  Common to
    1.19             all similar protocols.*)
    1.20 -    Fake "[| evs: woolam lost;  B ~= Spy;  
    1.21 +    Fake "[| evs: woolam;  B ~= Spy;  
    1.22               X: synth (analz (sees lost Spy evs)) |]
    1.23 -          ==> Says Spy B X  # evs : woolam lost"
    1.24 +          ==> Says Spy B X  # evs : woolam"
    1.25  
    1.26           (*Alice initiates a protocol run*)
    1.27 -    WL1  "[| evs: woolam lost;  A ~= B |]
    1.28 -          ==> Says A B (Agent A) # evs : woolam lost"
    1.29 +    WL1  "[| evs: woolam;  A ~= B |]
    1.30 +          ==> Says A B (Agent A) # evs : woolam"
    1.31  
    1.32           (*Bob responds to Alice's message with a challenge.*)
    1.33 -    WL2  "[| evs: woolam lost;  A ~= B;
    1.34 +    WL2  "[| evs: woolam;  A ~= B;
    1.35               Says A' B (Agent A) : set_of_list evs |]
    1.36 -          ==> Says B A (Nonce (newN evs)) # evs : woolam lost"
    1.37 +          ==> Says B A (Nonce (newN evs)) # evs : woolam"
    1.38  
    1.39           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.40             B is *not* properly determined -- Alice essentially broadcasts
    1.41             her reply.*)
    1.42 -    WL3  "[| evs: woolam lost;  A ~= B;
    1.43 +    WL3  "[| evs: woolam;  A ~= B;
    1.44               Says B' A (Nonce NB) : set_of_list evs;
    1.45               Says A  B (Agent A)  : set_of_list evs |]
    1.46 -          ==> Says A B (Crypt (Nonce NB) (shrK A)) # evs : woolam lost"
    1.47 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    1.48  
    1.49           (*Bob forwards Alice's response to the Server.*)
    1.50 -    WL4  "[| evs: woolam lost;  B ~= Server;  
    1.51 +    WL4  "[| evs: woolam;  B ~= Server;  
    1.52               Says A'  B X         : set_of_list evs;
    1.53               Says A'' B (Agent A) : set_of_list evs |]
    1.54 -          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam lost"
    1.55 +          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    1.56  
    1.57           (*Server decrypts Alice's response for Bob.*)
    1.58 -    WL5  "[| evs: woolam lost;  B ~= Server;
    1.59 -             Says B' Server {|Agent A, Agent B, Crypt (Nonce NB) (shrK A)|}
    1.60 +    WL5  "[| evs: woolam;  B ~= Server;
    1.61 +             Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.62                 : set_of_list evs |]
    1.63 -          ==> Says Server B (Crypt {|Agent A, Nonce NB|} (shrK B))
    1.64 -                 # evs : woolam lost"
    1.65 +          ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    1.66 +                 # evs : woolam"
    1.67  
    1.68  end