src/HOL/Auth/NS_Shared.thy
author paulson
Fri Sep 13 13:22:08 1996 +0200 (1996-09-13)
changeset 1997 6efba890341e
parent 1976 1cff1f4fdb8a
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness argument
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@1934
    15
consts  ns_shared   :: "event list set"
paulson@1934
    16
inductive ns_shared
paulson@1934
    17
  intrs 
paulson@1934
    18
         (*Initial trace is empty*)
paulson@1934
    19
    Nil  "[]: ns_shared"
paulson@1934
    20
paulson@1934
    21
         (*The enemy 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@1976
    24
    Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
paulson@1976
    25
          ==> Says Enemy B X # evs : ns_shared"
paulson@1934
    26
paulson@1965
    27
         (*Alice initiates a protocol run, requesting to talk to any B*)
paulson@1976
    28
    NS1  "[| evs: ns_shared;  A ~= Server |]
paulson@1976
    29
          ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
paulson@1943
    30
                 : ns_shared"
paulson@1934
    31
paulson@1934
    32
         (*Server's response to Alice's message.
paulson@1934
    33
           !! It may respond more than once to A's request !!
paulson@1934
    34
	   Server doesn't know who the true sender is, hence the A' in
paulson@1934
    35
               the sender field.*)
paulson@1934
    36
    NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
paulson@1976
    37
             Says A' Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
paulson@1976
    38
          ==> Says Server A 
paulson@1934
    39
                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
paulson@1943
    40
                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
paulson@1943
    41
                   (shrK A)) # evs : ns_shared"
paulson@1934
    42
paulson@1934
    43
          (*We can't assume S=Server.  Agent A "remembers" her nonce.
paulson@1997
    44
            Can inductively show A ~= Server*)
paulson@1934
    45
    NS3  "[| evs: ns_shared;  A ~= B;
paulson@1943
    46
             Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) 
paulson@1934
    47
               : set_of_list evs;
paulson@1976
    48
             Says A Server {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
paulson@1976
    49
          ==> Says A B X # evs : ns_shared"
paulson@1934
    50
paulson@1934
    51
         (*Bob's nonce exchange.  He does not know who the message came
paulson@1934
    52
           from, but responds to A because she is mentioned inside.*)
paulson@1934
    53
    NS4  "[| evs: ns_shared;  A ~= B;  
paulson@1976
    54
             Says A' B (Crypt {|Key K, Agent A|} (shrK B)) : set_of_list evs |]
paulson@1976
    55
          ==> Says B A (Crypt (Nonce (newN evs)) K) # evs : ns_shared"
paulson@1934
    56
paulson@1943
    57
         (*Alice responds with the Nonce, if she has seen the key before.
paulson@1943
    58
           We do NOT use N-1 or similar as the Enemy cannot spoof such things.
paulson@1943
    59
           Allowing the Enemy to add or subtract 1 allows him to send ALL
paulson@1943
    60
               nonces.  Instead we distinguish the messages by sending the
paulson@1943
    61
               nonce twice.*)
paulson@1934
    62
    NS5  "[| evs: ns_shared;  A ~= B;  
paulson@1943
    63
             Says B' A (Crypt (Nonce N) K) : set_of_list evs;
paulson@1943
    64
             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
paulson@1976
    65
               : set_of_list evs |]
paulson@1976
    66
          ==> Says A B (Crypt {|Nonce N, Nonce N|} K) # evs : ns_shared"
paulson@1934
    67
paulson@1934
    68
end