src/HOL/Auth/NS_Public_Bad.thy
author paulson
Tue Jul 22 11:21:17 1997 +0200 (1997-07-22)
changeset 3541 2f5ac0f047a6
parent 3519 ab0a9fbed4c0
child 3659 eddedfe2f3f8
permissions -rw-r--r--
Deleted the superfluous assumption A ~= B, which must hold anyway by induction
paulson@2318
     1
(*  Title:      HOL/Auth/NS_Public_Bad
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@2318
     7
Flawed version, vulnerable to Lowe's attack.
paulson@2318
     8
paulson@2318
     9
From page 260 of
paulson@2318
    10
  Burrows, Abadi and Needham.  A Logic of Authentication.
paulson@2318
    11
  Proc. Royal Soc. 426 (1989)
paulson@2318
    12
*)
paulson@2318
    13
paulson@2318
    14
NS_Public_Bad = Public + 
paulson@2318
    15
paulson@3519
    16
consts  ns_public  :: event list set
paulson@2549
    17
paulson@2318
    18
inductive ns_public
paulson@2318
    19
  intrs 
paulson@2318
    20
         (*Initial trace is empty*)
paulson@2318
    21
    Nil  "[]: ns_public"
paulson@2318
    22
paulson@2318
    23
         (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@2318
    24
           invent new nonces here, but he can also use NS1.  Common to
paulson@2318
    25
           all similar protocols.*)
paulson@2318
    26
    Fake "[| evs: ns_public;  B ~= Spy;  
paulson@3519
    27
             X: synth (analz (sees Spy evs)) |]
paulson@2318
    28
          ==> Says Spy B X  # evs : ns_public"
paulson@2318
    29
paulson@2318
    30
         (*Alice initiates a protocol run, sending a nonce to Bob*)
paulson@2497
    31
    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
paulson@2497
    32
          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
paulson@2451
    33
                # evs  :  ns_public"
paulson@2318
    34
paulson@2318
    35
         (*Bob responds to Alice's message with a further nonce*)
paulson@2497
    36
    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
nipkow@3465
    37
             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
paulson@2497
    38
          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
paulson@2451
    39
                # evs  :  ns_public"
paulson@2318
    40
paulson@2318
    41
         (*Alice proves her existence by sending NB back to Bob.*)
paulson@3541
    42
    NS3  "[| evs: ns_public;
nipkow@3465
    43
             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
nipkow@3465
    44
             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set 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
end