src/HOL/Auth/OtwayRees.thy
changeset 1976 1cff1f4fdb8a
parent 1941 f97a6e5b6375
child 2014 5be4c8ca7b25
equal deleted inserted replaced
1975:eec67972b1bf 1976:1cff1f4fdb8a
    19     Nil  "[]: otway"
    19     Nil  "[]: otway"
    20 
    20 
    21          (*The enemy MAY say anything he CAN say.  We do not expect him to
    21          (*The enemy MAY say anything he CAN say.  We do not expect him to
    22            invent new nonces here, but he can also use NS1.  Common to
    22            invent new nonces here, but he can also use NS1.  Common to
    23            all similar protocols.*)
    23            all similar protocols.*)
    24     Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
    24     Fake "[| evs: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    25           |] ==> Says Enemy B X  # evs : otway"
    25           ==> Says Enemy B X  # evs : otway"
    26 
    26 
    27          (*Alice initiates a protocol run*)
    27          (*Alice initiates a protocol run*)
    28     OR1  "[| evs: otway;  A ~= B
    28     OR1  "[| evs: otway;  A ~= B |]
    29           |] ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    29           ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    30                             Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    30                             Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    31                                   (shrK A) |} 
    31                                   (shrK A) |} 
    32                  # evs : otway"
    32                  # evs : otway"
    33 
    33 
    34          (*Bob's response to Alice's message.  Bob doesn't know who 
    34          (*Bob's response to Alice's message.  Bob doesn't know who 
    35 	   the sender is, hence the A' in the sender field.
    35 	   the sender is, hence the A' in the sender field.
    36            We modify the published protocol by NOT encrypting NB.*)
    36            We modify the published protocol by NOT encrypting NB.*)
    37     OR2  "[| evs: otway;  B ~= Server;
    37     OR2  "[| evs: otway;  B ~= Server;
    38              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
    38              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    39           |] ==> Says B Server 
    39           ==> Says B Server 
    40                   {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    40                   {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    41                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    41                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    42                  # evs : otway"
    42                  # evs : otway"
    43 
    43 
    44          (*The Server receives Bob's message and checks that the three NAs
    44          (*The Server receives Bob's message and checks that the three NAs
    48              Says B' Server 
    48              Says B' Server 
    49                   {|Nonce NA, Agent A, Agent B, 
    49                   {|Nonce NA, Agent A, Agent B, 
    50                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    50                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    51                     Nonce NB, 
    51                     Nonce NB, 
    52                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    52                     Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    53                : set_of_list evs
    53                : set_of_list evs |]
    54           |] ==> Says Server B 
    54           ==> Says Server B 
    55                   {|Nonce NA, 
    55                   {|Nonce NA, 
    56                     Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    56                     Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    57                     Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    57                     Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    58                  # evs : otway"
    58                  # evs : otway"
    59 
    59 
    61 	   those in the message he previously sent the Server.*)
    61 	   those in the message he previously sent the Server.*)
    62     OR4  "[| evs: otway;  A ~= B;  
    62     OR4  "[| evs: otway;  A ~= B;  
    63              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    63              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    64                : set_of_list evs;
    64                : set_of_list evs;
    65              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    65              Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    66                : set_of_list evs
    66                : set_of_list evs |]
    67           |] ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    67           ==> (Says B A {|Nonce NA, X|}) # evs : otway"
    68 
    68 
    69          (*Alice checks her Nonce, then sends a dummy message to Bob,
    69          (*Alice checks her Nonce, then sends a dummy message to Bob,
    70            using the new session key.*)
    70            using the new session key.*)
    71     OR5  "[| evs: otway;  
    71     OR5  "[| evs: otway;  
    72              Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    72              Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    73                : set_of_list evs;
    73                : set_of_list evs;
    74              Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs
    74              Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    75           |] ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    75           ==> Says A B (Crypt (Agent A) K)  # evs : otway"
    76 
    76 
    77 end
    77 end