src/HOL/Auth/NS_Public_Bad.thy
author paulson
Thu Jan 23 18:13:07 1997 +0100 (1997-01-23)
changeset 2549 0c723635b9e6
parent 2516 4d68fbe6378b
child 3465 e85c24717cad
permissions -rw-r--r--
Cosmetic improvements
     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 
    19 inductive ns_public
    20   intrs 
    21          (*Initial trace is empty*)
    22     Nil  "[]: ns_public"
    23 
    24          (*The spy MAY say anything he CAN say.  We do not expect him to
    25            invent new nonces here, but he can also use NS1.  Common to
    26            all similar protocols.*)
    27     Fake "[| evs: ns_public;  B ~= Spy;  
    28              X: synth (analz (sees lost Spy evs)) |]
    29           ==> Says Spy B X  # evs : ns_public"
    30 
    31          (*Alice initiates a protocol run, sending a nonce to Bob*)
    32     NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
    33           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    34                 # evs  :  ns_public"
    35 
    36          (*Bob responds to Alice's message with a further nonce*)
    37     NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    38              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
    39                : set_of_list evs |]
    40           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    41                 # evs  :  ns_public"
    42 
    43          (*Alice proves her existence by sending NB back to Bob.*)
    44     NS3  "[| evs: ns_public;  A ~= B;
    45              Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    46                : set_of_list evs;
    47              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    48                : set_of_list evs |]
    49           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    50 
    51   (**Oops message??**)
    52 
    53 rules
    54   (*Spy has access to his own key for spoof messages*)
    55   Spy_in_lost "Spy: lost"
    56 
    57 end