src/HOL/Auth/OtwayRees.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:
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/OtwayRees
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     2
    ID:         $Id$
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     5
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     6
Inductive relation "otway" for the Otway-Rees protocol.
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
     7
2014
5be4c8ca7b25 Correction of protocol; addition of Reveal message; proofs of
paulson
parents: 1976
diff changeset
     8
Version that encrypts Nonce NB
5be4c8ca7b25 Correction of protocol; addition of Reveal message; proofs of
paulson
parents: 1976
diff changeset
     9
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    10
From page 244 of
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    11
  Burrows, Abadi and Needham.  A Logic of Authentication.
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    12
  Proc. Royal Soc. 426 (1989)
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    13
*)
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    14
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    15
OtwayRees = Shared + 
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    16
2378
fc103154ad8f Removed needless quotation marks
paulson
parents: 2284
diff changeset
    17
consts  otway   :: agent set => event list set
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    18
inductive "otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    19
  intrs 
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    20
         (*Initial trace is empty*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    21
    Nil  "[]: otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    22
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    23
         (*The spy MAY say anything he CAN say.  We do not expect him to
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    24
           invent new nonces here, but he can also use NS1.  Common to
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    25
           all similar protocols.*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    26
    Fake "[| evs: otway lost;  B ~= Spy;  
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    27
             X: synth (analz (sees lost Spy evs)) |]
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    28
          ==> Says Spy B X  # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    29
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    30
         (*Alice initiates a protocol run*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    31
    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    32
          ==> Says A B {|Nonce NA, Agent A, Agent B, 
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    33
                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    34
                 # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    35
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    36
         (*Bob's response to Alice's message.  Bob doesn't know who 
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    37
	   the sender is, hence the A' in the sender field.
2105
782772e744dc Important correction to comment
paulson
parents: 2064
diff changeset
    38
           Note that NB is encrypted.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    39
    OR2  "[| evs: otway lost;  B ~= Server;  Nonce NB ~: used evs;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    40
             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
1976
1cff1f4fdb8a Reformatting
paulson
parents: 1941
diff changeset
    41
          ==> Says B Server 
2014
5be4c8ca7b25 Correction of protocol; addition of Reveal message; proofs of
paulson
parents: 1976
diff changeset
    42
                  {|Nonce NA, Agent A, Agent B, X, 
2451
ce85a2aafc7a Extensive tidying and simplification, largely stemming from
paulson
parents: 2378
diff changeset
    43
                    Crypt (shrK B)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    44
                      {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    45
                 # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    46
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    47
         (*The Server receives Bob's message and checks that the three NAs
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    48
           match.  Then he sends a new session key to Bob with a packet for
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    49
           forwarding to Alice.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    50
    OR3  "[| evs: otway lost;  B ~= Server;  Key KAB ~: used evs;
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    51
             Says B' Server 
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    52
                  {|Nonce NA, Agent A, Agent B, 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2135
diff changeset
    53
                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2135
diff changeset
    54
                    Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    55
               : set evs |]
1976
1cff1f4fdb8a Reformatting
paulson
parents: 1941
diff changeset
    56
          ==> Says Server B 
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    57
                  {|Nonce NA, 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    58
                    Crypt (shrK A) {|Nonce NA, Key KAB|},
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    59
                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    60
                 # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    61
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    62
         (*Bob receives the Server's (?) message and compares the Nonces with
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    63
	   those in the message he previously sent the Server.*)
2135
80477862ab33 Minor corrections
paulson
parents: 2105
diff changeset
    64
    OR4  "[| evs: otway lost;  A ~= B;  
2014
5be4c8ca7b25 Correction of protocol; addition of Reveal message; proofs of
paulson
parents: 1976
diff changeset
    65
             Says B Server {|Nonce NA, Agent A, Agent B, X', 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2135
diff changeset
    66
                             Crypt (shrK B)
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2135
diff changeset
    67
                                   {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    68
               : set evs;
2837
dee1c7f1f576 Trivial renamings (for consistency with CSFW papers)
paulson
parents: 2516
diff changeset
    69
             Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    70
               : set evs |]
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2014
diff changeset
    71
          ==> Says B A {|Nonce NA, X|} # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    72
2135
80477862ab33 Minor corrections
paulson
parents: 2105
diff changeset
    73
         (*This message models possible leaks of session keys.  The nonces
80477862ab33 Minor corrections
paulson
parents: 2105
diff changeset
    74
           identify the protocol run.*)
80477862ab33 Minor corrections
paulson
parents: 2105
diff changeset
    75
    Oops "[| evs: otway lost;  B ~= Spy;
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2135
diff changeset
    76
             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    77
               : set evs |]
2135
80477862ab33 Minor corrections
paulson
parents: 2105
diff changeset
    78
          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
1941
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    79
f97a6e5b6375 Initial working proof of Otway-Rees protocol
paulson
parents:
diff changeset
    80
end