src/HOL/Auth/NS_Public_Bad.thy
changeset 3659 eddedfe2f3f8
parent 3541 2f5ac0f047a6
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Sep 04 17:57:56 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Sep 05 12:24:13 1997 +0200
     1.3 @@ -28,21 +28,21 @@
     1.4            ==> Says Spy B X  # evs : ns_public"
     1.5  
     1.6           (*Alice initiates a protocol run, sending a nonce to Bob*)
     1.7 -    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
     1.8 +    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
     1.9            ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    1.10 -                # evs  :  ns_public"
    1.11 +                # evs1  :  ns_public"
    1.12  
    1.13           (*Bob responds to Alice's message with a further nonce*)
    1.14 -    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    1.15 -             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    1.16 +    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
    1.17 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
    1.18            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    1.19 -                # evs  :  ns_public"
    1.20 +                # evs2  :  ns_public"
    1.21  
    1.22           (*Alice proves her existence by sending NB back to Bob.*)
    1.23 -    NS3  "[| evs: ns_public;
    1.24 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    1.25 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
    1.26 -          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    1.27 +    NS3  "[| evs3: ns_public;
    1.28 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
    1.29 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
    1.30 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
    1.31  
    1.32    (**Oops message??**)
    1.33