Reformatting
authorpaulson
Wed Sep 11 18:40:55 1996 +0200 (1996-09-11)
changeset 19761cff1f4fdb8a
parent 1975 eec67972b1bf
child 1977 26edb2771d94
Reformatting
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
     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
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Wed Sep 11 18:00:53 1996 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Wed Sep 11 18:40:55 1996 +0200
     2.3 @@ -21,12 +21,12 @@
     2.4           (*The enemy MAY say anything he CAN say.  We do not expect him to
     2.5             invent new nonces here, but he can also use NS1.  Common to
     2.6             all similar protocols.*)
     2.7 -    Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
     2.8 -          |] ==> Says Enemy B X  # evs : otway"
     2.9 +    Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    2.10 +          ==> Says Enemy B X  # evs : otway"
    2.11  
    2.12           (*Alice initiates a protocol run*)
    2.13 -    OR1  "[| evs: otway;  A ~= B
    2.14 -          |] ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    2.15 +    OR1  "[| evs: otway;  A ~= B |]
    2.16 +          ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    2.17                              Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    2.18                                    (shrK A) |} 
    2.19                   # evs : otway"
    2.20 @@ -35,8 +35,8 @@
    2.21  	   the sender is, hence the A' in the sender field.
    2.22             We modify the published protocol by NOT encrypting NB.*)
    2.23      OR2  "[| evs: otway;  B ~= Server;
    2.24 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
    2.25 -          |] ==> Says B Server 
    2.26 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.27 +          ==> Says B Server 
    2.28                    {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    2.29                      Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.30                   # evs : otway"
    2.31 @@ -50,8 +50,8 @@
    2.32                      Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    2.33                      Nonce NB, 
    2.34                      Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.35 -               : set_of_list evs
    2.36 -          |] ==> Says Server B 
    2.37 +               : set_of_list evs |]
    2.38 +          ==> Says Server B 
    2.39                    {|Nonce NA, 
    2.40                      Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    2.41                      Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    2.42 @@ -63,15 +63,15 @@
    2.43               Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.44                 : set_of_list evs;
    2.45               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    2.46 -               : set_of_list evs
    2.47 -          |] ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    2.48 +               : set_of_list evs |]
    2.49 +          ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    2.50  
    2.51           (*Alice checks her Nonce, then sends a dummy message to Bob,
    2.52             using the new session key.*)
    2.53      OR5  "[| evs: otway;  
    2.54               Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.55                 : set_of_list evs;
    2.56 -             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
    2.57 -          |] ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    2.58 +             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.59 +          ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    2.60  
    2.61  end