src/HOL/Auth/NS_Shared.thy
author paulson
Tue Oct 08 10:21:04 1996 +0200 (1996-10-08)
changeset 2069 a1c623f70407
parent 2032 1bbf1bdcaf56
child 2131 3106a99d30a5
permissions -rw-r--r--
Addition of Revl rule, and tidying
     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 evs)|} # evs
    31                  : 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 {|Nonce NA, Agent B, Key (newK evs),   
    41                            (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    42                    (shrK A)) # evs : ns_shared lost"
    43 
    44           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    45             Can inductively show A ~= Server*)
    46     NS3  "[| evs: ns_shared lost;  A ~= B;
    47              Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
    48                : set_of_list evs;
    49              Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    50           ==> Says A B X # evs : ns_shared lost"
    51 
    52          (*Bob's nonce exchange.  He does not know who the message came
    53            from, but responds to A because she is mentioned inside.*)
    54     NS4  "[| evs: ns_shared lost;  A ~= B;  
    55              Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
    56           ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
    57 
    58          (*Alice responds with Nonce NB if she has seen the key before.
    59            Maybe should somehow check Nonce NA again.
    60            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    61            Letting the Spy add or subtract 1 lets him send ALL nonces.
    62            Instead we distinguish the messages by sending the nonce twice.*)
    63     NS5  "[| evs: ns_shared lost;  A ~= B;  
    64              Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    65              Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    66                : set_of_list evs |]
    67           ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
    68   
    69          (*This message models possible leaks of session keys.
    70            The two Nonces identify the protocol run.*)
    71     Revl "[| evs: ns_shared lost;  A ~= Spy;
    72              Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    73              Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    74                : set_of_list evs |]
    75           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    76 
    77 end