src/HOL/Auth/NS_Shared.thy
changeset 2516 4d68fbe6378b
parent 2451 ce85a2aafc7a
child 3465 e85c24717cad
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -26,20 +26,20 @@
     1.4            ==> Says Spy B X # evs : ns_shared lost"
     1.5  
     1.6           (*Alice initiates a protocol run, requesting to talk to any B*)
     1.7 -    NS1  "[| evs: ns_shared lost;  A ~= Server |]
     1.8 -          ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
     1.9 -                  # evs  :  ns_shared lost"
    1.10 +    NS1  "[| evs: ns_shared lost;  A ~= Server;  Nonce NA ~: used evs |]
    1.11 +          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
    1.12 +                :  ns_shared lost"
    1.13  
    1.14           (*Server's response to Alice's message.
    1.15             !! It may respond more than once to A's request !!
    1.16  	   Server doesn't know who the true sender is, hence the A' in
    1.17                 the sender field.*)
    1.18 -    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
    1.19 +    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    1.20               Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    1.21            ==> Says Server A 
    1.22                  (Crypt (shrK A)
    1.23 -                   {|Nonce NA, Agent B, Key (newK(length evs)),   
    1.24 -                    (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) 
    1.25 +                   {|Nonce NA, Agent B, Key KAB,
    1.26 +                     (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    1.27                  # evs : ns_shared lost"
    1.28  
    1.29            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.30 @@ -52,9 +52,9 @@
    1.31  
    1.32           (*Bob's nonce exchange.  He does not know who the message came
    1.33             from, but responds to A because she is mentioned inside.*)
    1.34 -    NS4  "[| evs: ns_shared lost;  A ~= B;  
    1.35 +    NS4  "[| evs: ns_shared lost;  A ~= B;  Nonce NB ~: used evs;
    1.36               Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    1.37 -          ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs
    1.38 +          ==> Says B A (Crypt K (Nonce NB)) # evs
    1.39                  : ns_shared lost"
    1.40  
    1.41           (*Alice responds with Nonce NB if she has seen the key before.