src/HOL/Auth/NS_Shared.thy
changeset 1976 1cff1f4fdb8a
parent 1965 789c12ea0b30
child 1997 6efba890341e
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Sep 11 18:00:53 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Sep 11 18:40:55 1996 +0200
     1.3 @@ -21,12 +21,12 @@
     1.4           (*The enemy MAY say anything he CAN say.  We do not expect him to
     1.5             invent new nonces here, but he can also use NS1.  Common to
     1.6             all similar protocols.*)
     1.7 -    Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
     1.8 -          |] ==> Says Enemy B X # evs : ns_shared"
     1.9 +    Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    1.10 +          ==> Says Enemy B X # evs : ns_shared"
    1.11  
    1.12           (*Alice initiates a protocol run, requesting to talk to any B*)
    1.13 -    NS1  "[| evs: ns_shared;  A ~= Server
    1.14 -          |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    1.15 +    NS1  "[| evs: ns_shared;  A ~= Server |]
    1.16 +          ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    1.17                   : ns_shared"
    1.18  
    1.19           (*Server's response to Alice's message.
    1.20 @@ -34,8 +34,8 @@
    1.21  	   Server doesn't know who the true sender is, hence the A' in
    1.22                 the sender field.*)
    1.23      NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
    1.24 -             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
    1.25 -          |] ==> Says Server A 
    1.26 +             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    1.27 +          ==> Says Server A 
    1.28                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    1.29                             (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    1.30                     (shrK A)) # evs : ns_shared"
    1.31 @@ -47,14 +47,14 @@
    1.32               Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    1.33                 : set_of_list evs;
    1.34               A = Friend i;
    1.35 -             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
    1.36 -          |] ==> Says A B X # evs : ns_shared"
    1.37 +             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    1.38 +          ==> Says A B X # evs : ns_shared"
    1.39  
    1.40           (*Bob's nonce exchange.  He does not know who the message came
    1.41             from, but responds to A because she is mentioned inside.*)
    1.42      NS4  "[| evs: ns_shared;  A ~= B;  
    1.43 -             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs
    1.44 -          |] ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    1.45 +             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
    1.46 +          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    1.47  
    1.48           (*Alice responds with the Nonce, if she has seen the key before.
    1.49             We do NOT use N-1 or similar as the Enemy cannot spoof such things.
    1.50 @@ -64,7 +64,7 @@
    1.51      NS5  "[| evs: ns_shared;  A ~= B;  
    1.52               Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    1.53               Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    1.54 -               : set_of_list evs
    1.55 -          |] ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    1.56 +               : set_of_list evs |]
    1.57 +          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    1.58  
    1.59  end