src/HOL/Auth/NS_Public.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3466 30791e5a69c4
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
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.
2538
c55f68761a8d Mended spelling error
paulson
parents: 2516
diff changeset
     7
Version incorporating Lowe's fix (inclusion of B's identity in round 2).
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     8
*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
     9
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    10
NS_Public = Public + 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    11
2549
0c723635b9e6 Cosmetic improvements
paulson
parents: 2538
diff changeset
    12
consts  lost       :: agent set        (*No need for it to be a variable*)
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    13
	ns_public  :: event list set
2549
0c723635b9e6 Cosmetic improvements
paulson
parents: 2538
diff changeset
    14
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    15
inductive ns_public
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    16
  intrs 
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    17
         (*Initial trace is empty*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    18
    Nil  "[]: ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    19
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    20
         (*The spy MAY say anything he CAN say.  We do not expect him to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    21
           invent new nonces here, but he can also use NS1.  Common to
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    22
           all similar protocols.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    23
    Fake "[| evs: ns_public;  B ~= Spy;  
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    24
             X: synth (analz (sees lost Spy evs)) |]
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    25
          ==> Says Spy B X  # evs : ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    26
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    27
         (*Alice initiates a protocol run, sending a nonce to Bob*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    28
    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    29
          ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    30
                 # evs  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    31
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    32
         (*Bob responds to Alice's message with a further nonce*)
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    33
    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    34
             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
2497
47de509bdd55 New treatment of nonce creation
paulson
parents: 2451
diff changeset
    35
          ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2318
diff changeset
    36
                # evs  :  ns_public"
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    37
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    38
         (*Alice proves her existence by sending NB back to Bob.*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    39
    NS3  "[| evs: ns_public;  A ~= B;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2549
diff changeset
    40
             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2497
diff changeset
    41
             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2549
diff changeset
    42
               : set evs |]
2318
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    43
          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    44
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    45
  (**Oops message??**)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    46
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    47
rules
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    48
  (*Spy has access to his own key for spoof messages*)
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    49
  Spy_in_lost "Spy: lost"
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    50
6d3f7c7f70b0 Public-key examples
paulson
parents:
diff changeset
    51
end