src/HOL/Auth/OtwayRees.thy
changeset 2014 5be4c8ca7b25
parent 1976 1cff1f4fdb8a
child 2032 1bbf1bdcaf56
equal deleted inserted replaced
2013:4b7a432fb3ed 2014:5be4c8ca7b25
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     4     Copyright   1996  University of Cambridge
     5 
     5 
     6 Inductive relation "otway" for the Otway-Rees protocol.
     6 Inductive relation "otway" for the Otway-Rees protocol.
       
     7 
       
     8 Version that encrypts Nonce NB
     7 
     9 
     8 From page 244 of
    10 From page 244 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    11   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    12   Proc. Royal Soc. 426 (1989)
    11 *)
    13 *)
    23            all similar protocols.*)
    25            all similar protocols.*)
    24     Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    26     Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    25           ==> Says Enemy B X  # evs : otway"
    27           ==> Says Enemy B X  # evs : otway"
    26 
    28 
    27          (*Alice initiates a protocol run*)
    29          (*Alice initiates a protocol run*)
    28     OR1  "[| evs: otway;  A ~= B |]
    30     OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    29           ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    31           ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    30                             Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    32                          Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    31                                   (shrK A) |} 
    33                                (shrK A) |} 
    32                  # evs : otway"
    34                  # evs : otway"
    33 
    35 
    34          (*Bob's response to Alice's message.  Bob doesn't know who 
    36          (*Bob's response to Alice's message.  Bob doesn't know who 
    35 	   the sender is, hence the A' in the sender field.
    37 	   the sender is, hence the A' in the sender field.
    36            We modify the published protocol by NOT encrypting NB.*)
    38            We modify the published protocol by NOT encrypting NB.*)
    37     OR2  "[| evs: otway;  B ~= Server;
    39     OR2  "[| evs: otway;  B ~= Server;
    38              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    40              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    39           ==> Says B Server 
    41           ==> Says B Server 
    40                   {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    42                   {|Nonce NA, Agent A, Agent B, X, 
    41                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    43                     Crypt {|Nonce NA, Nonce (newN evs), 
       
    44                             Agent A, Agent B|} (shrK B)|}
    42                  # evs : otway"
    45                  # evs : otway"
    43 
    46 
    44          (*The Server receives Bob's message and checks that the three NAs
    47          (*The Server receives Bob's message and checks that the three NAs
    45            match.  Then he sends a new session key to Bob with a packet for
    48            match.  Then he sends a new session key to Bob with a packet for
    46            forwarding to Alice.*)
    49            forwarding to Alice.*)
    47     OR3  "[| evs: otway;  B ~= Server;
    50     OR3  "[| evs: otway;  B ~= Server;
    48              Says B' Server 
    51              Says B' Server 
    49                   {|Nonce NA, Agent A, Agent B, 
    52                   {|Nonce NA, Agent A, Agent B, 
    50                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    53                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    51                     Nonce NB, 
    54                     Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} (shrK B)|}
    52                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
       
    53                : set_of_list evs |]
    55                : set_of_list evs |]
    54           ==> Says Server B 
    56           ==> Says Server B 
    55                   {|Nonce NA, 
    57                   {|Nonce NA, 
    56                     Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    58                     Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    57                     Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    59                     Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    58                  # evs : otway"
    60                  # evs : otway"
    59 
    61 
    60          (*Bob receives the Server's (?) message and compares the Nonces with
    62          (*Bob receives the Server's (?) message and compares the Nonces with
    61 	   those in the message he previously sent the Server.*)
    63 	   those in the message he previously sent the Server.*)
    62     OR4  "[| evs: otway;  A ~= B;  
    64     OR4  "[| evs: otway;  A ~= B;  B ~= Server;
    63              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    65              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    64                : set_of_list evs;
    66                : set_of_list evs;
    65              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    67              Says B Server {|Nonce NA, Agent A, Agent B, X', 
       
    68                              Crypt {|Nonce NA, Nonce NB, Agent A, Agent B|} 
       
    69                                    (shrK B)|}
    66                : set_of_list evs |]
    70                : set_of_list evs |]
    67           ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    71           ==> Says B A {|Nonce NA, X|} # evs : otway"
    68 
    72 
    69          (*Alice checks her Nonce, then sends a dummy message to Bob,
    73          (*This message models possible leaks of session keys.  Alice's Nonce
    70            using the new session key.*)
    74            identifies the protocol run.*)
    71     OR5  "[| evs: otway;  
    75     Reveal "[| evs: otway;  A ~= Enemy;
    72              Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    76                Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    73                : set_of_list evs;
    77                  : set_of_list evs;
    74              Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    78                Says A  B {|Nonce NA, Agent A, Agent B, 
    75           ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    79                            Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
       
    80                  : set_of_list evs |]
       
    81             ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
    76 
    82 
    77 end
    83 end