src/HOL/Auth/OtwayRees.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6333 b1dec44d0018
child 11185 1b737b4c2108
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@6308
     1
(*  
paulson@6308
     2
Inductive relation "otway" for the Otway-Rees protocol
paulson@6308
     3
extended by Gets primitive.
paulson@1941
     4
paulson@2014
     5
Version that encrypts Nonce NB
paulson@2014
     6
paulson@1941
     7
*)
paulson@1941
     8
paulson@1941
     9
OtwayRees = Shared + 
paulson@1941
    10
paulson@6308
    11
paulson@3519
    12
consts  otway   :: event list set
paulson@3519
    13
inductive "otway"
paulson@1941
    14
  intrs 
paulson@1941
    15
         (*Initial trace is empty*)
paulson@3519
    16
    Nil  "[]: otway"
paulson@1941
    17
paulson@5434
    18
         (** These rules allow agents to send messages to themselves **)
paulson@5434
    19
paulson@2032
    20
         (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@1941
    21
           invent new nonces here, but he can also use NS1.  Common to
paulson@1941
    22
           all similar protocols.*)
paulson@6308
    23
    Fake "[| evsa: otway;  X: synth (analz (knows Spy evsa)) |]
paulson@6308
    24
          ==> Says Spy B X  # evsa : otway"
paulson@6308
    25
paulson@6308
    26
         (*A message that has been sent can be received by the
paulson@6308
    27
           intended recipient.*)
paulson@6308
    28
    Reception "[| evsr: otway;  Says A B X : set evsr |]
paulson@6308
    29
               ==> Gets B X # evsr : otway"
paulson@1941
    30
paulson@1941
    31
         (*Alice initiates a protocol run*)
paulson@5434
    32
    OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
paulson@2516
    33
          ==> Says A B {|Nonce NA, Agent A, Agent B, 
paulson@2516
    34
                         Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
paulson@3659
    35
                 # evs1 : otway"
paulson@1941
    36
paulson@6333
    37
         (*Bob's response to Alice's message.  Note that NB is encrypted.*)
paulson@5434
    38
    OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
paulson@6308
    39
             Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
paulson@1976
    40
          ==> Says B Server 
paulson@2014
    41
                  {|Nonce NA, Agent A, Agent B, X, 
paulson@2451
    42
                    Crypt (shrK B)
paulson@2516
    43
                      {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
paulson@3659
    44
                 # evs2 : otway"
paulson@1941
    45
paulson@1941
    46
         (*The Server receives Bob's message and checks that the three NAs
paulson@1941
    47
           match.  Then he sends a new session key to Bob with a packet for
paulson@1941
    48
           forwarding to Alice.*)
paulson@5434
    49
    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
paulson@6308
    50
             Gets Server 
paulson@1941
    51
                  {|Nonce NA, Agent A, Agent B, 
paulson@2284
    52
                    Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
paulson@2284
    53
                    Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
paulson@3659
    54
               : set evs3 |]
paulson@1976
    55
          ==> Says Server B 
paulson@1941
    56
                  {|Nonce NA, 
paulson@2516
    57
                    Crypt (shrK A) {|Nonce NA, Key KAB|},
paulson@2516
    58
                    Crypt (shrK B) {|Nonce NB, Key KAB|}|}
paulson@3659
    59
                 # evs3 : otway"
paulson@1941
    60
paulson@1941
    61
         (*Bob receives the Server's (?) message and compares the Nonces with
paulson@5434
    62
	   those in the message he previously sent the Server.
paulson@5434
    63
           Need B ~= Server because we allow messages to self.*)
paulson@5434
    64
    OR4  "[| evs4: otway;  B ~= Server;
paulson@2014
    65
             Says B Server {|Nonce NA, Agent A, Agent B, X', 
paulson@2284
    66
                             Crypt (shrK B)
paulson@2284
    67
                                   {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
paulson@3659
    68
               : set evs4;
paulson@6308
    69
             Gets B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
paulson@3659
    70
               : set evs4 |]
paulson@3659
    71
          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
paulson@1941
    72
paulson@2135
    73
         (*This message models possible leaks of session keys.  The nonces
paulson@2135
    74
           identify the protocol run.*)
paulson@5359
    75
    Oops "[| evso: otway;  
paulson@2284
    76
             Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
paulson@3659
    77
               : set evso |]
paulson@4537
    78
          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
paulson@1941
    79
paulson@1941
    80
end