src/HOL/Auth/NS_Public_Bad.thy
author paulson
Thu Dec 05 18:07:27 1996 +0100 (1996-12-05)
changeset 2318 6d3f7c7f70b0
child 2451 ce85a2aafc7a
permissions -rw-r--r--
Public-key examples
     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 |]
    32           ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
    33                 : ns_public"
    34 
    35          (*Bob responds to Alice's message with a further nonce*)
    36     NS2  "[| evs: ns_public;  A ~= B;
    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 (newN evs)|}) # evs
    40                 : 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