src/HOL/Auth/NS_Public.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5434 9b4bed3f394c
child 11104 f2024fed9f0c
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@2318
     1
(*  Title:      HOL/Auth/NS_Public
paulson@2318
     2
    ID:         $Id$
paulson@2318
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2318
     4
    Copyright   1996  University of Cambridge
paulson@2318
     5
paulson@2318
     6
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
paulson@2538
     7
Version incorporating Lowe's fix (inclusion of B's identity in round 2).
paulson@2318
     8
*)
paulson@2318
     9
paulson@2318
    10
NS_Public = Public + 
paulson@2318
    11
paulson@3519
    12
consts  ns_public  :: event list set
paulson@2549
    13
paulson@2318
    14
inductive ns_public
paulson@2318
    15
  intrs 
paulson@2318
    16
         (*Initial trace is empty*)
paulson@2318
    17
    Nil  "[]: ns_public"
paulson@2318
    18
paulson@2318
    19
         (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@2318
    20
           invent new nonces here, but he can also use NS1.  Common to
paulson@2318
    21
           all similar protocols.*)
paulson@5434
    22
    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
paulson@2318
    23
          ==> Says Spy B X  # evs : ns_public"
paulson@2318
    24
paulson@2318
    25
         (*Alice initiates a protocol run, sending a nonce to Bob*)
paulson@5434
    26
    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
paulson@2497
    27
          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
paulson@3659
    28
                 # evs1  :  ns_public"
paulson@2318
    29
paulson@2318
    30
         (*Bob responds to Alice's message with a further nonce*)
paulson@5434
    31
    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
paulson@3659
    32
             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
paulson@2497
    33
          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
paulson@3659
    34
                # evs2  :  ns_public"
paulson@2318
    35
paulson@2318
    36
         (*Alice proves her existence by sending NB back to Bob.*)
paulson@3659
    37
    NS3  "[| evs3: ns_public;
paulson@3659
    38
             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
paulson@2516
    39
             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
paulson@3659
    40
               : set evs3 |]
paulson@3659
    41
          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
paulson@2318
    42
paulson@2318
    43
  (**Oops message??**)
paulson@2318
    44
paulson@2318
    45
end