src/HOL/Auth/WooLam.thy
changeset 5434 9b4bed3f394c
parent 3683 aafe719dff14
child 11185 1b737b4c2108
     1.1 --- a/src/HOL/Auth/WooLam.thy	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -22,20 +22,20 @@
     1.4           (*Initial trace is empty*)
     1.5      Nil  "[]: woolam"
     1.6  
     1.7 +         (** These rules allow agents to send messages to themselves **)
     1.8 +
     1.9           (*The spy MAY say anything he CAN say.  We do not expect him to
    1.10             invent new nonces here, but he can also use NS1.  Common to
    1.11             all similar protocols.*)
    1.12 -    Fake "[| evs: woolam;  B ~= Spy;  
    1.13 -             X: synth (analz (spies evs)) |]
    1.14 +    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
    1.15            ==> Says Spy B X  # evs : woolam"
    1.16  
    1.17           (*Alice initiates a protocol run*)
    1.18 -    WL1  "[| evs1: woolam;  A ~= B |]
    1.19 +    WL1  "[| evs1: woolam |]
    1.20            ==> Says A B (Agent A) # evs1 : woolam"
    1.21  
    1.22           (*Bob responds to Alice's message with a challenge.*)
    1.23 -    WL2  "[| evs2: woolam;  A ~= B;  
    1.24 -             Says A' B (Agent A) : set evs2 |]
    1.25 +    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
    1.26            ==> Says B A (Nonce NB) # evs2 : woolam"
    1.27  
    1.28           (*Alice responds to Bob's challenge by encrypting NB with her key.
    1.29 @@ -50,13 +50,13 @@
    1.30             the messages are shown in chronological order, for clarity.
    1.31             But here, exchanging the two events would cause the lemma
    1.32             WL4_analz_spies to pick up the wrong assumption!*)
    1.33 -    WL4  "[| evs4: woolam;  B ~= Server;  
    1.34 +    WL4  "[| evs4: woolam;  
    1.35               Says A'  B X         : set evs4;
    1.36               Says A'' B (Agent A) : set evs4 |]
    1.37            ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
    1.38  
    1.39           (*Server decrypts Alice's response for Bob.*)
    1.40 -    WL5  "[| evs5: woolam;  B ~= Server;
    1.41 +    WL5  "[| evs5: woolam;  
    1.42               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    1.43                 : set evs5 |]
    1.44            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})