src/HOL/Auth/NS_Shared.thy
author paulson
Tue Sep 03 18:24:42 1996 +0200 (1996-09-03)
changeset 1943 20574dca5a3e
parent 1934 58573e7041b4
child 1965 789c12ea0b30
permissions -rw-r--r--
Renaming and simplification
     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*)
    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             May assume WLOG that she is NOT the Enemy: the Fake rule
    45             covers this case.  Can inductively show A ~= Server*)
    46     NS3  "[| evs: ns_shared;  A ~= B;
    47              Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    48                : set_of_list evs;
    49              A = Friend i;
    50              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs
    51           |] ==> Says A B X # evs : ns_shared"
    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;  A ~= B;  
    56              Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs
    57           |] ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
    58 
    59          (*Alice responds with the Nonce, if she has seen the key before.
    60            We do NOT use N-1 or similar as the Enemy cannot spoof such things.
    61            Allowing the Enemy to add or subtract 1 allows him to send ALL
    62                nonces.  Instead we distinguish the messages by sending the
    63                nonce twice.*)
    64     NS5  "[| evs: ns_shared;  A ~= B;  
    65              Says B' A (Crypt (Nonce N) K) : set_of_list evs;
    66              Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    67                : set_of_list evs
    68           |] ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
    69 
    70 end