src/HOL/Auth/NS_Public_Bad.thy
changeset 2516 4d68fbe6378b
parent 2497 47de509bdd55
child 2549 0c723635b9e6
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -41,9 +41,9 @@
     1.4  
     1.5           (*Alice proves her existence by sending NB back to Bob.*)
     1.6      NS3  "[| evs: ns_public;  A ~= B;
     1.7 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
     1.8 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
     1.9                 : set_of_list evs;
    1.10 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    1.11 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    1.12                 : set_of_list evs |]
    1.13            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    1.14