src/HOL/Auth/NS_Shared.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5434 9b4bed3f394c
child 11104 f2024fed9f0c
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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;  X: synth (analz (spies evs)) |]
    25           ==> Says Spy B X # evs : ns_shared"
    26 
    27          (*Alice initiates a protocol run, requesting to talk to any B*)
    28     NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
    29           ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    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  "[| evs2: ns_shared;  Key KAB ~: used evs2;
    37              Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    38           ==> Says Server A 
    39                 (Crypt (shrK A)
    40                    {|Nonce NA, Agent B, Key KAB,
    41                      (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    42                 # evs2 : ns_shared"
    43 
    44           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    45             Need A ~= Server because we allow messages to self.*)
    46     NS3  "[| evs3: ns_shared;  A ~= Server;
    47              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    48                : set evs3;
    49              Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    50           ==> Says A B X # evs3 : ns_shared"
    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  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
    55              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    56           ==> Says B A (Crypt K (Nonce NB)) # evs4
    57                 : ns_shared"
    58 
    59          (*Alice responds with Nonce NB if she has seen the key before.
    60            Maybe should somehow check Nonce NA again.
    61            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    62            Letting the Spy add or subtract 1 lets him send ALL nonces.
    63            Instead we distinguish the messages by sending the nonce twice.*)
    64     NS5  "[| evs5: ns_shared;  
    65              Says B' A (Crypt K (Nonce NB)) : set evs5;
    66              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    67                : set evs5 |]
    68           ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
    69   
    70          (*This message models possible leaks of session keys.
    71            The two Nonces identify the protocol run: the rule insists upon
    72            the true senders in order to make them accurate.*)
    73     Oops "[| evso: ns_shared;  Says B A (Crypt K (Nonce NB)) : set evso;
    74              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    75                : set evso |]
    76           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
    77 
    78 end