src/HOL/Auth/NS_Public_Bad.thy
author paulson
Thu Jan 09 10:22:11 1997 +0100 (1997-01-09)
changeset 2497 47de509bdd55
parent 2451 ce85a2aafc7a
child 2516 4d68fbe6378b
permissions -rw-r--r--
New treatment of nonce creation
     1 (*  Title:      HOL/Auth/NS_Public_Bad
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     7 Flawed version, vulnerable to Lowe's attack.
     8 
     9 From page 260 of
    10   Burrows, Abadi and Needham.  A Logic of Authentication.
    11   Proc. Royal Soc. 426 (1989)
    12 *)
    13 
    14 NS_Public_Bad = Public + 
    15 
    16 consts  lost    :: agent set        (*No need for it to be a variable*)
    17 	ns_public  :: event list set
    18 inductive ns_public
    19   intrs 
    20          (*Initial trace is empty*)
    21     Nil  "[]: ns_public"
    22 
    23          (*The spy MAY say anything he CAN say.  We do not expect him to
    24            invent new nonces here, but he can also use NS1.  Common to
    25            all similar protocols.*)
    26     Fake "[| evs: ns_public;  B ~= Spy;  
    27              X: synth (analz (sees lost Spy evs)) |]
    28           ==> Says Spy B X  # evs : ns_public"
    29 
    30          (*Alice initiates a protocol run, sending a nonce to Bob*)
    31     NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
    32           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    33                 # evs  :  ns_public"
    34 
    35          (*Bob responds to Alice's message with a further nonce*)
    36     NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    37              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    38                : set_of_list evs |]
    39           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    40                 # evs  :  ns_public"
    41 
    42          (*Alice proves her existence by sending NB back to Bob.*)
    43     NS3  "[| evs: ns_public;  A ~= B;
    44              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    45                : set_of_list evs;
    46              Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    47                : set_of_list evs |]
    48           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    49 
    50   (**Oops message??**)
    51 
    52 rules
    53   (*Spy has access to his own key for spoof messages*)
    54   Spy_in_lost "Spy: lost"
    55 
    56 end