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