src/HOL/Auth/NS_Public_Bad.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5434 9b4bed3f394c
child 11104 f2024fed9f0c
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3465
diff changeset
    16
consts  ns_public  :: event list set
2549
0c723635b9e6 Cosmetic improvements
paulson
parents: 2516
diff changeset
    17
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    18
inductive ns_public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    19
  intrs 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    20
         (*Initial trace is empty*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    21
    Nil  "[]: ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    22
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    23
         (*The spy MAY say anything he CAN say.  We do not expect him to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    24
           invent new nonces here, but he can also use NS1.  Common to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
           all similar protocols.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    26
    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
          ==> Says Spy B X  # evs : ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    28
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    29
         (*Alice initiates a protocol run, sending a nonce to Bob*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    30
    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    31
          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    32
                # evs1  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    33
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    34
         (*Bob responds to Alice's message with a further nonce*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 3683
diff changeset
    35
    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    36
             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    37
          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    38
                # evs2  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    39
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    40
         (*Alice proves her existence by sending NB back to Bob.*)
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    41
    NS3  "[| evs3: ns_public;
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    42
             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    43
             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3541
diff changeset
    44
          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    45
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    46
  (**Oops message??**)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    47
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    48
end