src/HOL/Auth/NS_Shared.thy
author paulson
Fri Sep 13 13:22:08 1996 +0200 (1996-09-13)
changeset 1997 6efba890341e
parent 1976 1cff1f4fdb8a
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness 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   :: "event list set"
    16 inductive ns_shared
    17   intrs 
    18          (*Initial trace is empty*)
    19     Nil  "[]: ns_shared"
    20 
    21          (*The enemy 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;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    25           ==> Says Enemy B X # evs : ns_shared"
    26 
    27          (*Alice initiates a protocol run, requesting to talk to any B*)
    28     NS1  "[| evs: ns_shared;  A ~= Server |]
    29           ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    30                  : ns_shared"
    31 
    32          (*Server's response to Alice's message.
    33            !! It may respond more than once to A's request !!
    34 	   Server doesn't know who the true sender is, hence the A' in
    35                the sender field.*)
    36     NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
    37              Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    38           ==> Says Server A 
    39                   (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    40                            (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    41                    (shrK A)) # evs : ns_shared"
    42 
    43           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    44             Can inductively show A ~= Server*)
    45     NS3  "[| evs: ns_shared;  A ~= B;
    46              Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    47                : set_of_list evs;
    48              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    49           ==> Says A B X # evs : ns_shared"
    50 
    51          (*Bob's nonce exchange.  He does not know who the message came
    52            from, but responds to A because she is mentioned inside.*)
    53     NS4  "[| evs: ns_shared;  A ~= B;  
    54              Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
    55           ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    56 
    57          (*Alice responds with the Nonce, if she has seen the key before.
    58            We do NOT use N-1 or similar as the Enemy cannot spoof such things.
    59            Allowing the Enemy to add or subtract 1 allows him to send ALL
    60                nonces.  Instead we distinguish the messages by sending the
    61                nonce twice.*)
    62     NS5  "[| evs: ns_shared;  A ~= B;  
    63              Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    64              Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    65                : set_of_list evs |]
    66           ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    67 
    68 end