src/HOL/Auth/NS_Public_Bad.thy
changeset 2318 6d3f7c7f70b0
child 2451 ce85a2aafc7a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Dec 05 18:07:27 1996 +0100
     1.3 @@ -0,0 +1,56 @@
     1.4 +(*  Title:      HOL/Auth/NS_Public_Bad
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
    1.10 +Flawed version, vulnerable to Lowe's attack.
    1.11 +
    1.12 +From page 260 of
    1.13 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.14 +  Proc. Royal Soc. 426 (1989)
    1.15 +*)
    1.16 +
    1.17 +NS_Public_Bad = Public + 
    1.18 +
    1.19 +consts  lost    :: agent set        (*No need for it to be a variable*)
    1.20 +	ns_public  :: event list set
    1.21 +inductive ns_public
    1.22 +  intrs 
    1.23 +         (*Initial trace is empty*)
    1.24 +    Nil  "[]: ns_public"
    1.25 +
    1.26 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    1.27 +           invent new nonces here, but he can also use NS1.  Common to
    1.28 +           all similar protocols.*)
    1.29 +    Fake "[| evs: ns_public;  B ~= Spy;  
    1.30 +             X: synth (analz (sees lost Spy evs)) |]
    1.31 +          ==> Says Spy B X  # evs : ns_public"
    1.32 +
    1.33 +         (*Alice initiates a protocol run, sending a nonce to Bob*)
    1.34 +    NS1  "[| evs: ns_public;  A ~= B |]
    1.35 +          ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
    1.36 +                : ns_public"
    1.37 +
    1.38 +         (*Bob responds to Alice's message with a further nonce*)
    1.39 +    NS2  "[| evs: ns_public;  A ~= B;
    1.40 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    1.41 +               : set_of_list evs |]
    1.42 +          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs
    1.43 +                : ns_public"
    1.44 +
    1.45 +         (*Alice proves her existence by sending NB back to Bob.*)
    1.46 +    NS3  "[| evs: ns_public;  A ~= B;
    1.47 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    1.48 +               : set_of_list evs;
    1.49 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    1.50 +               : set_of_list evs |]
    1.51 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    1.52 +
    1.53 +  (**Oops message??**)
    1.54 +
    1.55 +rules
    1.56 +  (*Spy has access to his own key for spoof messages*)
    1.57 +  Spy_in_lost "Spy: lost"
    1.58 +
    1.59 +end