src/HOL/Auth/NS_Shared.thy
changeset 5434 9b4bed3f394c
parent 5359 bd539b72d484
child 11104 f2024fed9f0c
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -21,12 +21,11 @@
     1.4           (*The spy 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 ~= Spy;  
     1.8 -             X: synth (analz (spies evs)) |]
     1.9 +    Fake "[| evs: ns_shared;  X: synth (analz (spies evs)) |]
    1.10            ==> Says Spy B X # evs : ns_shared"
    1.11  
    1.12           (*Alice initiates a protocol run, requesting to talk to any B*)
    1.13 -    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
    1.14 +    NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
    1.15            ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    1.16                  :  ns_shared"
    1.17  
    1.18 @@ -34,7 +33,7 @@
    1.19             !! It may respond more than once to A's request !!
    1.20  	   Server doesn't know who the true sender is, hence the A' in
    1.21                 the sender field.*)
    1.22 -    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    1.23 +    NS2  "[| evs2: ns_shared;  Key KAB ~: used evs2;
    1.24               Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    1.25            ==> Says Server A 
    1.26                  (Crypt (shrK A)
    1.27 @@ -43,8 +42,8 @@
    1.28                  # evs2 : ns_shared"
    1.29  
    1.30            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.31 -            Can inductively show A ~= Server*)
    1.32 -    NS3  "[| evs3: ns_shared;  A ~= B;
    1.33 +            Need A ~= Server because we allow messages to self.*)
    1.34 +    NS3  "[| evs3: ns_shared;  A ~= Server;
    1.35               Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    1.36                 : set evs3;
    1.37               Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    1.38 @@ -52,7 +51,7 @@
    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  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
    1.43 +    NS4  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
    1.44               Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    1.45            ==> Says B A (Crypt K (Nonce NB)) # evs4
    1.46                  : ns_shared"
    1.47 @@ -62,7 +61,7 @@
    1.48             We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.49             Letting the Spy add or subtract 1 lets him send ALL nonces.
    1.50             Instead we distinguish the messages by sending the nonce twice.*)
    1.51 -    NS5  "[| evs5: ns_shared;  A ~= B;  
    1.52 +    NS5  "[| evs5: ns_shared;  
    1.53               Says B' A (Crypt K (Nonce NB)) : set evs5;
    1.54               Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    1.55                 : set evs5 |]