src/HOL/Auth/NS_Public_Bad.thy
changeset 3465 e85c24717cad
parent 2549 0c723635b9e6
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -35,17 +35,14 @@
     1.4  
     1.5           (*Bob responds to Alice's message with a further nonce*)
     1.6      NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
     1.7 -             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
     1.8 -               : set_of_list evs |]
     1.9 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    1.10            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    1.11                  # evs  :  ns_public"
    1.12  
    1.13           (*Alice proves her existence by sending NB back to Bob.*)
    1.14      NS3  "[| evs: ns_public;  A ~= B;
    1.15 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|})
    1.16 -               : set_of_list evs;
    1.17 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    1.18 -               : set_of_list evs |]
    1.19 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    1.20 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
    1.21            ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    1.22  
    1.23    (**Oops message??**)