src/HOL/Auth/NS_Public.thy
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
     1 (*  Title:      HOL/Auth/NS_Public
     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 Version incorporating Lowe's fix (inclusion of B's identity in round 2).
     8 *)
     9 
    10 NS_Public = Public + 
    11 
    12 consts  lost       :: agent set        (*No need for it to be a variable*)
    13 	ns_public  :: event list set
    14 
    15 inductive ns_public
    16   intrs 
    17          (*Initial trace is empty*)
    18     Nil  "[]: ns_public"
    19 
    20          (*The spy MAY say anything he CAN say.  We do not expect him to
    21            invent new nonces here, but he can also use NS1.  Common to
    22            all similar protocols.*)
    23     Fake "[| evs: ns_public;  B ~= Spy;  
    24              X: synth (analz (sees lost Spy evs)) |]
    25           ==> Says Spy B X  # evs : ns_public"
    26 
    27          (*Alice initiates a protocol run, sending a nonce to Bob*)
    28     NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
    29           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    30                  # evs  :  ns_public"
    31 
    32          (*Bob responds to Alice's message with a further nonce*)
    33     NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    34              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    35           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    36                 # evs  :  ns_public"
    37 
    38          (*Alice proves her existence by sending NB back to Bob.*)
    39     NS3  "[| evs: ns_public;  A ~= B;
    40              Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    41              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    42                : set evs |]
    43           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    44 
    45   (**Oops message??**)
    46 
    47 rules
    48   (*Spy has access to his own key for spoof messages*)
    49   Spy_in_lost "Spy: lost"
    50 
    51 end