src/HOL/Auth/NS_Public.thy
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3683 aafe719dff14
child 5434 9b4bed3f394c
permissions -rw-r--r--
First working version with Oops event for session keys
     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  ns_public  :: event list set
    13 
    14 inductive ns_public
    15   intrs 
    16          (*Initial trace is empty*)
    17     Nil  "[]: ns_public"
    18 
    19          (*The spy MAY say anything he CAN say.  We do not expect him to
    20            invent new nonces here, but he can also use NS1.  Common to
    21            all similar protocols.*)
    22     Fake "[| evs: ns_public;  B ~= Spy;  
    23              X: synth (analz (spies evs)) |]
    24           ==> Says Spy B X  # evs : ns_public"
    25 
    26          (*Alice initiates a protocol run, sending a nonce to Bob*)
    27     NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
    28           ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    29                  # evs1  :  ns_public"
    30 
    31          (*Bob responds to Alice's message with a further nonce*)
    32     NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
    33              Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
    34           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    35                 # evs2  :  ns_public"
    36 
    37          (*Alice proves her existence by sending NB back to Bob.*)
    38     NS3  "[| evs3: ns_public;
    39              Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
    40              Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    41                : set evs3 |]
    42           ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
    43 
    44   (**Oops message??**)
    45 
    46 end