src/HOL/Auth/OtwayRees_AN.thy
changeset 4537 4e835bd9fada
parent 3683 aafe719dff14
child 5359 bd539b72d484
equal deleted inserted replaced
4536:74f7c556fd90 4537:4e835bd9fada
    66     Oops "[| evso: otway;  B ~= Spy;
    66     Oops "[| evso: otway;  B ~= Spy;
    67              Says Server B 
    67              Says Server B 
    68                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
    68                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
    69                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    69                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    70                : set evso |]
    70                : set evso |]
    71           ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
    71           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
    72 
    72 
    73 end
    73 end