src/HOL/Auth/NS_Shared.thy
author paulson
Thu Dec 19 11:58:39 1996 +0100 (1996-12-19)
changeset 2451 ce85a2aafc7a
parent 2378 fc103154ad8f
child 2516 4d68fbe6378b
permissions -rw-r--r--
Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument
     1 (*  Title:      HOL/Auth/NS_Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
     7 
     8 From page 247 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 NS_Shared = Shared + 
    14 
    15 consts  ns_shared   :: agent set => event list set
    16 inductive "ns_shared lost"
    17   intrs 
    18          (*Initial trace is empty*)
    19     Nil  "[]: ns_shared lost"
    20 
    21          (*The spy MAY say anything he CAN say.  We do not expect him to
    22            invent new nonces here, but he can also use NS1.  Common to
    23            all similar protocols.*)
    24     Fake "[| evs: ns_shared lost;  B ~= Spy;  
    25              X: synth (analz (sees lost Spy evs)) |]
    26           ==> Says Spy B X # evs : ns_shared lost"
    27 
    28          (*Alice initiates a protocol run, requesting to talk to any B*)
    29     NS1  "[| evs: ns_shared lost;  A ~= Server |]
    30           ==> Says A Server {|Agent A, Agent B, Nonce (newN(length evs))|}
    31                   # evs  :  ns_shared lost"
    32 
    33          (*Server's response to Alice's message.
    34            !! It may respond more than once to A's request !!
    35 	   Server doesn't know who the true sender is, hence the A' in
    36                the sender field.*)
    37     NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
    38              Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    39           ==> Says Server A 
    40                 (Crypt (shrK A)
    41                    {|Nonce NA, Agent B, Key (newK(length evs)),   
    42                     (Crypt (shrK B) {|Key (newK(length evs)), Agent A|})|}) 
    43                 # evs : ns_shared lost"
    44 
    45           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    46             Can inductively show A ~= Server*)
    47     NS3  "[| evs: ns_shared lost;  A ~= B;
    48              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    49                : set_of_list evs;
    50              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    51           ==> Says A B X # evs : ns_shared lost"
    52 
    53          (*Bob's nonce exchange.  He does not know who the message came
    54            from, but responds to A because she is mentioned inside.*)
    55     NS4  "[| evs: ns_shared lost;  A ~= B;  
    56              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set_of_list evs |]
    57           ==> Says B A (Crypt K (Nonce (newN(length evs)))) # evs
    58                 : ns_shared lost"
    59 
    60          (*Alice responds with Nonce NB if she has seen the key before.
    61            Maybe should somehow check Nonce NA again.
    62            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    63            Letting the Spy add or subtract 1 lets him send ALL nonces.
    64            Instead we distinguish the messages by sending the nonce twice.*)
    65     NS5  "[| evs: ns_shared lost;  A ~= B;  
    66              Says B' A (Crypt K (Nonce NB)) : set_of_list evs;
    67              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    68                : set_of_list evs |]
    69           ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared lost"
    70   
    71          (*This message models possible leaks of session keys.
    72            The two Nonces identify the protocol run: the rule insists upon
    73            the true senders in order to make them accurate.*)
    74     Oops "[| evs: ns_shared lost;  A ~= Spy;
    75              Says B A (Crypt K (Nonce NB)) : set_of_list evs;
    76              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    77                : set_of_list evs |]
    78           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    79 
    80 end