src/HOL/Auth/NS_Shared.thy
author paulson
Fri Sep 05 12:24:13 1997 +0200 (1997-09-05)
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
permissions -rw-r--r--
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
     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 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;  B ~= Spy;  
    25              X: synth (analz (sees Spy evs)) |]
    26           ==> Says Spy B X # evs : ns_shared"
    27 
    28          (*Alice initiates a protocol run, requesting to talk to any B*)
    29     NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
    30           ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    31                 :  ns_shared"
    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  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    38              Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    39           ==> Says Server A 
    40                 (Crypt (shrK A)
    41                    {|Nonce NA, Agent B, Key KAB,
    42                      (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    43                 # evs2 : ns_shared"
    44 
    45           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    46             Can inductively show A ~= Server*)
    47     NS3  "[| evs3: ns_shared;  A ~= B;
    48              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    49                : set evs3;
    50              Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    51           ==> Says A B X # evs3 : 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  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
    56              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    57           ==> Says B A (Crypt K (Nonce NB)) # evs4
    58                 : ns_shared"
    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  "[| evs5: ns_shared;  A ~= B;  
    66              Says B' A (Crypt K (Nonce NB)) : set evs5;
    67              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    68                : set evs5 |]
    69           ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
    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 "[| evso: ns_shared;  A ~= Spy;
    75              Says B A (Crypt K (Nonce NB)) : set evso;
    76              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    77                : set evso |]
    78           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
    79 
    80 end