src/HOL/Auth/NS_Public_Bad.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3465 e85c24717cad
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/NS_Public_Bad
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     2
    ID:         $Id$
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     5
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     6
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     7
Flawed version, vulnerable to Lowe's attack.
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     8
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     9
From page 260 of
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    10
  Burrows, Abadi and Needham.  A Logic of Authentication.
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    11
  Proc. Royal Soc. 426 (1989)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    12
*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    13
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    14
NS_Public_Bad = Public + 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    15
2549
0c723635b9e6 Cosmetic improvements
paulson
parents: 2516
diff changeset
    16
consts  lost       :: agent set        (*No need for it to be a variable*)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    17
	ns_public  :: event list set
2549
0c723635b9e6 Cosmetic improvements
paulson
parents: 2516
diff changeset
    18
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    19
inductive ns_public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    20
  intrs 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    21
         (*Initial trace is empty*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    22
    Nil  "[]: ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    23
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    24
         (*The spy MAY say anything he CAN say.  We do not expect him to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
           invent new nonces here, but he can also use NS1.  Common to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    26
           all similar protocols.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
    Fake "[| evs: ns_public;  B ~= Spy;  
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    28
             X: synth (analz (sees lost Spy evs)) |]
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    29
          ==> Says Spy B X  # evs : ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    30
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    31
         (*Alice initiates a protocol run, sending a nonce to Bob*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    32
    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    33
          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    34
                # evs  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    35
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    36
         (*Bob responds to Alice's message with a further nonce*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    37
    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2549
diff changeset
    38
             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    39
          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    40
                # evs  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    41
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    42
         (*Alice proves her existence by sending NB back to Bob.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    43
    NS3  "[| evs: ns_public;  A ~= B;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2549
diff changeset
    44
             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
e85c24717cad set_of_list -> set
nipkow
parents: 2549
diff changeset
    45
             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    46
          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    47
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    48
  (**Oops message??**)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    49
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    50
rules
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    51
  (*Spy has access to his own key for spoof messages*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    52
  Spy_in_lost "Spy: lost"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    53
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    54
end