src/HOL/Auth/Yahalom.thy
changeset 2110 d01151e66cd4
parent 2032 1bbf1bdcaf56
child 2125 92a08ee6a9cb
equal deleted inserted replaced
2109:fabc35243cea 2110:d01151e66cd4
    57                         X|}
    57                         X|}
    58                : set_of_list evs;
    58                : set_of_list evs;
    59              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    59              Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    60           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
    60           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
    61 
    61 
       
    62          (*This message models possible leaks of session keys.  The Nonces
       
    63            identify the protocol run.*)
       
    64     Revl "[| evs: yahalom lost;  A ~= Spy;
       
    65              Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
       
    66                         X|}
       
    67                : set_of_list evs |]
       
    68           ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
       
    69 
    62 end
    70 end