src/HOL/Auth/NS_Shared.thy
author paulson
Thu Sep 18 13:24:04 1997 +0200 (1997-09-18)
changeset 3683 aafe719dff14
parent 3659 eddedfe2f3f8
child 4537 4e835bd9fada
permissions -rw-r--r--
Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems
     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 (spies 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