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