src/HOL/Auth/NS_Shared.thy
author paulson
Wed Aug 21 13:25:27 1996 +0200 (1996-08-21)
changeset 1934 58573e7041b4
child 1943 20574dca5a3e
permissions -rw-r--r--
Separation of theory Event into two parts:
Shared for general shared-key material
NS_Shared for the Needham-Schroeder shared-key protocol
     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)|}) 
    30                  # evs : 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|} (serverKey B))|}
    41                    (serverKey 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|} (serverKey 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|} (serverKey B))) 
    57                : set_of_list evs
    58           |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : ns_shared"
    59 
    60          (*Alice responds with (Suc N), if she has seen the key before.*)
    61     NS5  "[| evs: ns_shared;  A ~= B;  
    62              (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    63              (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    64                : set_of_list evs
    65           |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : ns_shared"
    66 
    67 end