src/HOL/Auth/OtwayRees.thy
changeset 2064 5a5e508e2a2b
parent 2032 1bbf1bdcaf56
child 2105 782772e744dc
equal deleted inserted replaced
2063:2395bc55b3e6 2064:5a5e508e2a2b
    71                : set_of_list evs |]
    71                : set_of_list evs |]
    72           ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    72           ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    73 
    73 
    74          (*This message models possible leaks of session keys.  Alice's Nonce
    74          (*This message models possible leaks of session keys.  Alice's Nonce
    75            identifies the protocol run.*)
    75            identifies the protocol run.*)
    76     Reveal "[| evs: otway lost;  A ~= Spy;
    76     Revl "[| evs: otway lost;  A ~= Spy;
    77                Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    77              Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    78                  : set_of_list evs;
    78                : set_of_list evs;
    79                Says A  B {|Nonce NA, Agent A, Agent B, 
    79              Says A  B {|Nonce NA, Agent A, Agent B, 
    80                            Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    80                          Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    81                  : set_of_list evs |]
    81                : set_of_list evs |]
    82             ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
    82           ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
    83 
    83 
    84 end
    84 end