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
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@3519
    15
consts  ns_shared   :: event list set
paulson@3519
    16
inductive "ns_shared"
paulson@1934
    17
  intrs 
paulson@1934
    18
         (*Initial trace is empty*)
paulson@3519
    19
    Nil  "[]: ns_shared"
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@3519
    24
    Fake "[| evs: ns_shared;  B ~= Spy;  
paulson@3519
    25
             X: synth (analz (sees Spy evs)) |]
paulson@3519
    26
          ==> Says Spy B X # evs : ns_shared"
paulson@1934
    27
paulson@1965
    28
         (*Alice initiates a protocol run, requesting to talk to any B*)
paulson@3659
    29
    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
paulson@3659
    30
          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
paulson@3519
    31
                :  ns_shared"
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@3659
    37
    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
paulson@3659
    38
             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
paulson@2451
    39
          ==> Says Server A 
paulson@2451
    40
                (Crypt (shrK A)
paulson@2516
    41
                   {|Nonce NA, Agent B, Key KAB,
paulson@2516
    42
                     (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
paulson@3659
    43
                # evs2 : ns_shared"
paulson@1934
    44
paulson@1934
    45
          (*We can't assume S=Server.  Agent A "remembers" her nonce.
paulson@1997
    46
            Can inductively show A ~= Server*)
paulson@3659
    47
    NS3  "[| evs3: ns_shared;  A ~= B;
paulson@2284
    48
             Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
paulson@3659
    49
               : set evs3;
paulson@3659
    50
             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
paulson@3659
    51
          ==> Says A B X # evs3 : ns_shared"
paulson@1934
    52
paulson@1934
    53
         (*Bob's nonce exchange.  He does not know who the message came
paulson@1934
    54
           from, but responds to A because she is mentioned inside.*)
paulson@3659
    55
    NS4  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
paulson@3659
    56
             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
paulson@3659
    57
          ==> Says B A (Crypt K (Nonce NB)) # evs4
paulson@3519
    58
                : ns_shared"
paulson@1934
    59
paulson@2069
    60
         (*Alice responds with Nonce NB if she has seen the key before.
paulson@2069
    61
           Maybe should somehow check Nonce NA again.
paulson@2069
    62
           We do NOT send NB-1 or similar as the Spy cannot spoof such things.
paulson@2069
    63
           Letting the Spy add or subtract 1 lets him send ALL nonces.
paulson@2069
    64
           Instead we distinguish the messages by sending the nonce twice.*)
paulson@3659
    65
    NS5  "[| evs5: ns_shared;  A ~= B;  
paulson@3659
    66
             Says B' A (Crypt K (Nonce NB)) : set evs5;
paulson@2284
    67
             Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
paulson@3659
    68
               : set evs5 |]
paulson@3659
    69
          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
paulson@2069
    70
  
paulson@2069
    71
         (*This message models possible leaks of session keys.
paulson@2131
    72
           The two Nonces identify the protocol run: the rule insists upon
paulson@2131
    73
           the true senders in order to make them accurate.*)
paulson@3659
    74
    Oops "[| evso: ns_shared;  A ~= Spy;
paulson@3659
    75
             Says B A (Crypt K (Nonce NB)) : set evso;
paulson@2284
    76
             Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
paulson@3659
    77
               : set evso |]
paulson@3659
    78
          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
paulson@1934
    79
paulson@1934
    80
end