src/HOL/Auth/NS_Shared.thy
author paulson
Thu Sep 26 12:50:48 1996 +0200 (1996-09-26)
changeset 2032 1bbf1bdcaf56
parent 1997 6efba890341e
child 2069 a1c623f70407
permissions -rw-r--r--
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
paulson@1934
     1
(*  Title:      HOL/Auth/NS_Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
paulson@1934
     7
paulson@1934
     8
From page 247 of
paulson@1934
     9
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@1934
    10
  Proc. Royal Soc. 426 (1989)
paulson@1934
    11
*)
paulson@1934
    12
paulson@1934
    13
NS_Shared = Shared + 
paulson@1934
    14
paulson@2032
    15
consts  ns_shared   :: "agent set => event list set"
paulson@2032
    16
inductive "ns_shared lost"
paulson@1934
    17
  intrs 
paulson@1934
    18
         (*Initial trace is empty*)
paulson@2032
    19
    Nil  "[]: ns_shared lost"
paulson@1934
    20
paulson@2032
    21
         (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@1934
    22
           invent new nonces here, but he can also use NS1.  Common to
paulson@1934
    23
           all similar protocols.*)
paulson@2032
    24
    Fake "[| evs: ns_shared lost;  B ~= Spy;  
paulson@2032
    25
             X: synth (analz (sees lost Spy evs)) |]
paulson@2032
    26
          ==> Says Spy B X # evs : ns_shared lost"
paulson@1934
    27
paulson@1965
    28
         (*Alice initiates a protocol run, requesting to talk to any B*)
paulson@2032
    29
    NS1  "[| evs: ns_shared lost;  A ~= Server |]
paulson@1976
    30
          ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
paulson@2032
    31
                 : ns_shared lost"
paulson@1934
    32
paulson@1934
    33
         (*Server's response to Alice's message.
paulson@1934
    34
           !! It may respond more than once to A's request !!
paulson@1934
    35
	   Server doesn't know who the true sender is, hence the A' in
paulson@1934
    36
               the sender field.*)
paulson@2032
    37
    NS2  "[| evs: ns_shared lost;  A ~= B;  A ~= Server;
paulson@1976
    38
             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
paulson@1976
    39
          ==> Says Server A 
paulson@1934
    40
                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
paulson@1943
    41
                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
paulson@2032
    42
                   (shrK A)) # evs : ns_shared lost"
paulson@1934
    43
paulson@1934
    44
          (*We can't assume S=Server.  Agent A "remembers" her nonce.
paulson@1997
    45
            Can inductively show A ~= Server*)
paulson@2032
    46
    NS3  "[| evs: ns_shared lost;  A ~= B;
paulson@1943
    47
             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
paulson@1934
    48
               : set_of_list evs;
paulson@1976
    49
             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
paulson@2032
    50
          ==> Says A B X # evs : ns_shared lost"
paulson@1934
    51
paulson@1934
    52
         (*Bob's nonce exchange.  He does not know who the message came
paulson@1934
    53
           from, but responds to A because she is mentioned inside.*)
paulson@2032
    54
    NS4  "[| evs: ns_shared lost;  A ~= B;  
paulson@1976
    55
             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
paulson@2032
    56
          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared lost"
paulson@1934
    57
paulson@1943
    58
         (*Alice responds with the Nonce, if she has seen the key before.
paulson@2032
    59
           We do NOT use N-1 or similar as the Spy cannot spoof such things.
paulson@2032
    60
           Allowing the Spy to add or subtract 1 allows him to send ALL
paulson@1943
    61
               nonces.  Instead we distinguish the messages by sending the
paulson@1943
    62
               nonce twice.*)
paulson@2032
    63
    NS5  "[| evs: ns_shared lost;  A ~= B;  
paulson@1943
    64
             Says B' A (Crypt (Nonce N) K) : set_of_list evs;
paulson@1943
    65
             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
paulson@1976
    66
               : set_of_list evs |]
paulson@2032
    67
          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared lost"
paulson@1934
    68
paulson@1934
    69
end