src/HOL/Auth/OtwayRees_AN.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:
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/OtwayRees
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     2
    ID:         $Id$
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     5
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     6
Inductive relation "otway" for the Otway-Rees protocol.
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     7
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     8
Simplified version with minimal encryption but explicit messages
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
     9
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    10
Note that the formalization does not even assume that nonces are fresh.
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    11
This is because the protocol does not rely on uniqueness of nonces for
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    12
security, only for freshness, and the proof script does not prove freshness
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    13
properties.
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    14
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    15
From page 11 of
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    16
  Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    17
  IEEE Trans. SE 22 (1), 1996
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    18
*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    19
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    20
OtwayRees_AN = Shared + 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    21
2378
fc103154ad8f Removed needless quotation marks
paulson
parents: 2284
diff changeset
    22
consts  otway   :: agent set => event list set
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    23
inductive "otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    24
  intrs 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    25
         (*Initial trace is empty*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    26
    Nil  "[]: otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    27
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    28
         (*The spy MAY say anything he CAN say.  We do not expect him to
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    29
           invent new nonces here, but he can also use NS1.  Common to
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    30
           all similar protocols.*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    31
    Fake "[| evs: otway lost;  B ~= Spy;  
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    32
             X: synth (analz (sees lost Spy evs)) |]
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    33
          ==> Says Spy B X  # evs : otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    34
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    35
         (*Alice initiates a protocol run*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    36
    OR1  "[| evs: otway lost;  A ~= B;  B ~= Server |]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    37
          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway lost"
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    38
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    39
         (*Bob's response to Alice's message.  Bob doesn't know who 
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    40
	   the sender is, hence the A' in the sender field.*)
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    41
    OR2  "[| evs: otway lost;  B ~= Server;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    42
             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    43
          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    44
                 # evs : otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    45
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    46
         (*The Server receives Bob's message.  Then he sends a new
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    47
           session key to Bob with a packet for forwarding to Alice.*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    48
    OR3  "[| evs: otway lost;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    49
             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    50
               : set evs |]
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    51
          ==> Says Server B 
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    52
               {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2451
diff changeset
    53
                 Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    54
              # evs : otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    55
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    56
         (*Bob receives the Server's (?) message and compares the Nonces with
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    57
	   those in the message he previously sent the Server.*)
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    58
    OR4  "[| evs: otway lost;  A ~= B;
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    59
             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
2837
dee1c7f1f576 Trivial renamings (for consistency with CSFW papers)
paulson
parents: 2516
diff changeset
    60
             Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    61
               : set evs |]
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    62
          ==> Says B A X # evs : otway lost"
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    63
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    64
         (*This message models possible leaks of session keys.  The nonces
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    65
           identify the protocol run.  B is not assumed to know shrK A.*)
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    66
    Oops "[| evs: otway lost;  B ~= Spy;
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    67
             Says Server B 
2284
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    68
                      {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
80ebd1a213fd Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents: 2131
diff changeset
    69
                        Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2837
diff changeset
    70
               : set evs |]
2131
3106a99d30a5 Changing from the Reveal to the Oops rule
paulson
parents: 2090
diff changeset
    71
          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
2090
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    72
307ebbbec862 Abadi and Needham's variant of Otway-Rees
paulson
parents:
diff changeset
    73
end