src/HOL/Auth/OtwayRees.thy
changeset 2105 782772e744dc
parent 2064 5a5e508e2a2b
child 2135 80477862ab33
equal deleted inserted replaced
2104:f5c9a91e4b50 2105:782772e744dc
    34                                (shrK A) |} 
    34                                (shrK A) |} 
    35                  # evs : otway lost"
    35                  # evs : otway lost"
    36 
    36 
    37          (*Bob's response to Alice's message.  Bob doesn't know who 
    37          (*Bob's response to Alice's message.  Bob doesn't know who 
    38 	   the sender is, hence the A' in the sender field.
    38 	   the sender is, hence the A' in the sender field.
    39            We modify the published protocol by NOT encrypting NB.*)
    39            Note that NB is encrypted.*)
    40     OR2  "[| evs: otway lost;  B ~= Server;
    40     OR2  "[| evs: otway lost;  B ~= Server;
    41              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    41              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    42           ==> Says B Server 
    42           ==> Says B Server 
    43                   {|Nonce NA, Agent A, Agent B, X, 
    43                   {|Nonce NA, Agent A, Agent B, X, 
    44                     Crypt {|Nonce NA, Nonce (newN evs), 
    44                     Crypt {|Nonce NA, Nonce (newN evs),