Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
authorpaulson
Fri Sep 05 12:24:13 1997 +0200 (1997-09-05)
changeset 3659eddedfe2f3f8
parent 3658 f87dd7b68d8c
child 3660 5c9d3a63e9ff
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/NS_Public.thy	Thu Sep 04 17:57:56 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.thy	Fri Sep 05 12:24:13 1997 +0200
     1.3 @@ -24,22 +24,22 @@
     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, Agent B|})
    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 +    NS3  "[| evs3: ns_public;
    1.26 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
    1.27               Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    1.28 -               : set evs |]
    1.29 -          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    1.30 +               : set evs3 |]
    1.31 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
    1.32  
    1.33    (**Oops message??**)
    1.34  
     2.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Sep 04 17:57:56 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Fri Sep 05 12:24:13 1997 +0200
     2.3 @@ -28,21 +28,21 @@
     2.4            ==> Says Spy B X  # evs : ns_public"
     2.5  
     2.6           (*Alice initiates a protocol run, sending a nonce to Bob*)
     2.7 -    NS1  "[| evs: ns_public;  A ~= B;  Nonce NA ~: used evs |]
     2.8 +    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
     2.9            ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    2.10 -                # evs  :  ns_public"
    2.11 +                # evs1  :  ns_public"
    2.12  
    2.13           (*Bob responds to Alice's message with a further nonce*)
    2.14 -    NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
    2.15 -             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
    2.16 +    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
    2.17 +             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
    2.18            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    2.19 -                # evs  :  ns_public"
    2.20 +                # evs2  :  ns_public"
    2.21  
    2.22           (*Alice proves her existence by sending NB back to Bob.*)
    2.23 -    NS3  "[| evs: ns_public;
    2.24 -             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;
    2.25 -             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs |]
    2.26 -          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"
    2.27 +    NS3  "[| evs3: ns_public;
    2.28 +             Says A  B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs3;
    2.29 +             Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs3 |]
    2.30 +          ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 : ns_public"
    2.31  
    2.32    (**Oops message??**)
    2.33  
     3.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Sep 04 17:57:56 1997 +0200
     3.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Sep 05 12:24:13 1997 +0200
     3.3 @@ -26,35 +26,35 @@
     3.4            ==> Says Spy B X # evs : ns_shared"
     3.5  
     3.6           (*Alice initiates a protocol run, requesting to talk to any B*)
     3.7 -    NS1  "[| evs: ns_shared;  A ~= Server;  Nonce NA ~: used evs |]
     3.8 -          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs
     3.9 +    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
    3.10 +          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    3.11                  :  ns_shared"
    3.12  
    3.13           (*Server's response to Alice's message.
    3.14             !! It may respond more than once to A's request !!
    3.15  	   Server doesn't know who the true sender is, hence the A' in
    3.16                 the sender field.*)
    3.17 -    NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    3.18 -             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs |]
    3.19 +    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    3.20 +             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    3.21            ==> Says Server A 
    3.22                  (Crypt (shrK A)
    3.23                     {|Nonce NA, Agent B, Key KAB,
    3.24                       (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    3.25 -                # evs : ns_shared"
    3.26 +                # evs2 : ns_shared"
    3.27  
    3.28            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    3.29              Can inductively show A ~= Server*)
    3.30 -    NS3  "[| evs: ns_shared;  A ~= B;
    3.31 +    NS3  "[| evs3: ns_shared;  A ~= B;
    3.32               Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    3.33 -               : set evs;
    3.34 -             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs |]
    3.35 -          ==> Says A B X # evs : ns_shared"
    3.36 +               : set evs3;
    3.37 +             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    3.38 +          ==> Says A B X # evs3 : ns_shared"
    3.39  
    3.40           (*Bob's nonce exchange.  He does not know who the message came
    3.41             from, but responds to A because she is mentioned inside.*)
    3.42 -    NS4  "[| evs: ns_shared;  A ~= B;  Nonce NB ~: used evs;
    3.43 -             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs |]
    3.44 -          ==> Says B A (Crypt K (Nonce NB)) # evs
    3.45 +    NS4  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
    3.46 +             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    3.47 +          ==> Says B A (Crypt K (Nonce NB)) # evs4
    3.48                  : ns_shared"
    3.49  
    3.50           (*Alice responds with Nonce NB if she has seen the key before.
    3.51 @@ -62,19 +62,19 @@
    3.52             We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    3.53             Letting the Spy add or subtract 1 lets him send ALL nonces.
    3.54             Instead we distinguish the messages by sending the nonce twice.*)
    3.55 -    NS5  "[| evs: ns_shared;  A ~= B;  
    3.56 -             Says B' A (Crypt K (Nonce NB)) : set evs;
    3.57 +    NS5  "[| evs5: ns_shared;  A ~= B;  
    3.58 +             Says B' A (Crypt K (Nonce NB)) : set evs5;
    3.59               Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    3.60 -               : set evs |]
    3.61 -          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs : ns_shared"
    3.62 +               : set evs5 |]
    3.63 +          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
    3.64    
    3.65           (*This message models possible leaks of session keys.
    3.66             The two Nonces identify the protocol run: the rule insists upon
    3.67             the true senders in order to make them accurate.*)
    3.68 -    Oops "[| evs: ns_shared;  A ~= Spy;
    3.69 -             Says B A (Crypt K (Nonce NB)) : set evs;
    3.70 +    Oops "[| evso: ns_shared;  A ~= Spy;
    3.71 +             Says B A (Crypt K (Nonce NB)) : set evso;
    3.72               Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    3.73 -               : set evs |]
    3.74 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared"
    3.75 +               : set evso |]
    3.76 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
    3.77  
    3.78  end
     4.1 --- a/src/HOL/Auth/OtwayRees.thy	Thu Sep 04 17:57:56 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Sep 05 12:24:13 1997 +0200
     4.3 @@ -28,53 +28,53 @@
     4.4            ==> Says Spy B X  # evs : otway"
     4.5  
     4.6           (*Alice initiates a protocol run*)
     4.7 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
     4.8 +    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
     4.9            ==> Says A B {|Nonce NA, Agent A, Agent B, 
    4.10                           Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
    4.11 -                 # evs : otway"
    4.12 +                 # evs1 : otway"
    4.13  
    4.14           (*Bob's response to Alice's message.  Bob doesn't know who 
    4.15  	   the sender is, hence the A' in the sender field.
    4.16             Note that NB is encrypted.*)
    4.17 -    OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
    4.18 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
    4.19 +    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
    4.20 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    4.21            ==> Says B Server 
    4.22                    {|Nonce NA, Agent A, Agent B, X, 
    4.23                      Crypt (shrK B)
    4.24                        {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    4.25 -                 # evs : otway"
    4.26 +                 # evs2 : otway"
    4.27  
    4.28           (*The Server receives Bob's message and checks that the three NAs
    4.29             match.  Then he sends a new session key to Bob with a packet for
    4.30             forwarding to Alice.*)
    4.31 -    OR3  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
    4.32 +    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
    4.33               Says B' Server 
    4.34                    {|Nonce NA, Agent A, Agent B, 
    4.35                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    4.36                      Crypt (shrK B) {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    4.37 -               : set evs |]
    4.38 +               : set evs3 |]
    4.39            ==> Says Server B 
    4.40                    {|Nonce NA, 
    4.41                      Crypt (shrK A) {|Nonce NA, Key KAB|},
    4.42                      Crypt (shrK B) {|Nonce NB, Key KAB|}|}
    4.43 -                 # evs : otway"
    4.44 +                 # evs3 : otway"
    4.45  
    4.46           (*Bob receives the Server's (?) message and compares the Nonces with
    4.47  	   those in the message he previously sent the Server.*)
    4.48 -    OR4  "[| evs: otway;  A ~= B;  
    4.49 +    OR4  "[| evs4: otway;  A ~= B;  
    4.50               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    4.51                               Crypt (shrK B)
    4.52                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    4.53 -               : set evs;
    4.54 +               : set evs4;
    4.55               Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    4.56 -               : set evs |]
    4.57 -          ==> Says B A {|Nonce NA, X|} # evs : otway"
    4.58 +               : set evs4 |]
    4.59 +          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
    4.60  
    4.61           (*This message models possible leaks of session keys.  The nonces
    4.62             identify the protocol run.*)
    4.63 -    Oops "[| evs: otway;  B ~= Spy;
    4.64 +    Oops "[| evso: otway;  B ~= Spy;
    4.65               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    4.66 -               : set evs |]
    4.67 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
    4.68 +               : set evso |]
    4.69 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
    4.70  
    4.71  end
     5.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Sep 04 17:57:56 1997 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Sep 05 12:24:13 1997 +0200
     5.3 @@ -33,41 +33,41 @@
     5.4            ==> Says Spy B X  # evs : otway"
     5.5  
     5.6           (*Alice initiates a protocol run*)
     5.7 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
     5.8 -          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs : otway"
     5.9 +    OR1  "[| evs1: otway;  A ~= B;  B ~= Server |]
    5.10 +          ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
    5.11  
    5.12           (*Bob's response to Alice's message.  Bob doesn't know who 
    5.13  	   the sender is, hence the A' in the sender field.*)
    5.14 -    OR2  "[| evs: otway;  B ~= Server;
    5.15 -             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs |]
    5.16 +    OR2  "[| evs2: otway;  B ~= Server;
    5.17 +             Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    5.18            ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    5.19 -                 # evs : otway"
    5.20 +                 # evs2 : otway"
    5.21  
    5.22           (*The Server receives Bob's message.  Then he sends a new
    5.23             session key to Bob with a packet for forwarding to Alice.*)
    5.24 -    OR3  "[| evs: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs;
    5.25 +    OR3  "[| evs3: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs3;
    5.26               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    5.27 -               : set evs |]
    5.28 +               : set evs3 |]
    5.29            ==> Says Server B 
    5.30                 {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
    5.31                   Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key KAB|}|}
    5.32 -              # evs : otway"
    5.33 +              # evs3 : otway"
    5.34  
    5.35           (*Bob receives the Server's (?) message and compares the Nonces with
    5.36  	   those in the message he previously sent the Server.*)
    5.37 -    OR4  "[| evs: otway;  A ~= B;
    5.38 -             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
    5.39 +    OR4  "[| evs4: otway;  A ~= B;
    5.40 +             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
    5.41               Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
    5.42 -               : set evs |]
    5.43 -          ==> Says B A X # evs : otway"
    5.44 +               : set evs4 |]
    5.45 +          ==> Says B A X # evs4 : otway"
    5.46  
    5.47           (*This message models possible leaks of session keys.  The nonces
    5.48             identify the protocol run.  B is not assumed to know shrK A.*)
    5.49 -    Oops "[| evs: otway;  B ~= Spy;
    5.50 +    Oops "[| evso: otway;  B ~= Spy;
    5.51               Says Server B 
    5.52                        {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
    5.53                          Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}
    5.54 -               : set evs |]
    5.55 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
    5.56 +               : set evso |]
    5.57 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
    5.58  
    5.59  end
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Sep 04 17:57:56 1997 +0200
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Sep 05 12:24:13 1997 +0200
     6.3 @@ -26,51 +26,51 @@
     6.4            ==> Says Spy B X  # evs : otway"
     6.5  
     6.6           (*Alice initiates a protocol run*)
     6.7 -    OR1  "[| evs: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs |]
     6.8 +    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
     6.9            ==> Says A B {|Nonce NA, Agent A, Agent B, 
    6.10                           Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
    6.11 -                 # evs : otway"
    6.12 +                 # evs1 : otway"
    6.13  
    6.14           (*Bob's response to Alice's message.  Bob doesn't know who 
    6.15  	   the sender is, hence the A' in the sender field.
    6.16             We modify the published protocol by NOT encrypting NB.*)
    6.17 -    OR2  "[| evs: otway;  B ~= Server;  Nonce NB ~: used evs;
    6.18 -             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs |]
    6.19 +    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
    6.20 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
    6.21            ==> Says B Server 
    6.22                    {|Nonce NA, Agent A, Agent B, X, Nonce NB,
    6.23                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    6.24 -                 # evs : otway"
    6.25 +                 # evs2 : otway"
    6.26  
    6.27           (*The Server receives Bob's message and checks that the three NAs
    6.28             match.  Then he sends a new session key to Bob with a packet for
    6.29             forwarding to Alice.*)
    6.30 -    OR3  "[| evs: otway;  B ~= Server;  Key KAB ~: used evs;
    6.31 +    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
    6.32               Says B' Server 
    6.33                    {|Nonce NA, Agent A, Agent B, 
    6.34                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
    6.35                      Nonce NB, 
    6.36                      Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
    6.37 -               : set evs |]
    6.38 +               : set evs3 |]
    6.39            ==> Says Server B 
    6.40                    {|Nonce NA, 
    6.41                      Crypt (shrK A) {|Nonce NA, Key KAB|},
    6.42                      Crypt (shrK B) {|Nonce NB, Key KAB|}|}
    6.43 -                 # evs : otway"
    6.44 +                 # evs3 : otway"
    6.45  
    6.46           (*Bob receives the Server's (?) message and compares the Nonces with
    6.47  	   those in the message he previously sent the Server.*)
    6.48 -    OR4  "[| evs: otway;  A ~= B;
    6.49 +    OR4  "[| evs4: otway;  A ~= B;
    6.50               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    6.51 -               : set evs;
    6.52 +               : set evs4;
    6.53               Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    6.54 -               : set evs |]
    6.55 -          ==> Says B A {|Nonce NA, X|} # evs : otway"
    6.56 +               : set evs4 |]
    6.57 +          ==> Says B A {|Nonce NA, X|} # evs4 : otway"
    6.58  
    6.59           (*This message models possible leaks of session keys.  The nonces
    6.60             identify the protocol run.*)
    6.61 -    Oops "[| evs: otway;  B ~= Spy;
    6.62 +    Oops "[| evso: otway;  B ~= Spy;
    6.63               Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
    6.64 -               : set evs |]
    6.65 -          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
    6.66 +               : set evso |]
    6.67 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
    6.68  
    6.69  end
     7.1 --- a/src/HOL/Auth/Recur.thy	Thu Sep 04 17:57:56 1997 +0200
     7.2 +++ b/src/HOL/Auth/Recur.thy	Fri Sep 05 12:24:13 1997 +0200
     7.3 @@ -62,11 +62,11 @@
     7.4  
     7.5           (*Alice initiates a protocol run.
     7.6             "Agent Server" is just a placeholder, to terminate the nesting.*)
     7.7 -    RA1  "[| evs: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
     7.8 +    RA1  "[| evs1: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs1 |]
     7.9            ==> Says A B 
    7.10                  (Hash[Key(shrK A)] 
    7.11                   {|Agent A, Agent B, Nonce NA, Agent Server|})
    7.12 -              # evs : recur"
    7.13 +              # evs1 : recur"
    7.14  
    7.15           (*Bob's response to Alice's message.  C might be the Server.
    7.16             XA should be the Hash of the remaining components with KA, but
    7.17 @@ -74,27 +74,27 @@
    7.18             P is the previous recur message from Alice's caller.
    7.19             NOTE: existing proofs don't need PA and are complicated by its
    7.20                  presence!  See parts_Fake_tac.*)
    7.21 -    RA2  "[| evs: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
    7.22 -             Says A' B PA : set evs;  
    7.23 +    RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
    7.24 +             Says A' B PA : set evs2;  
    7.25               PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
    7.26            ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
    7.27 -              # evs : recur"
    7.28 +              # evs2 : recur"
    7.29  
    7.30           (*The Server receives Bob's message and prepares a response.*)
    7.31 -    RA3  "[| evs: recur;  B ~= Server;
    7.32 -             Says B' Server PB : set evs;
    7.33 -             (PB,RB,K) : respond evs |]
    7.34 -          ==> Says Server B RB # evs : recur"
    7.35 +    RA3  "[| evs3: recur;  B ~= Server;
    7.36 +             Says B' Server PB : set evs3;
    7.37 +             (PB,RB,K) : respond evs3 |]
    7.38 +          ==> Says Server B RB # evs3 : recur"
    7.39  
    7.40           (*Bob receives the returned message and compares the Nonces with
    7.41             those in the message he previously sent the Server.*)
    7.42 -    RA4  "[| evs: recur;  A ~= B;  
    7.43 +    RA4  "[| evs4: recur;  A ~= B;  
    7.44               Says B  C {|XH, Agent B, Agent C, Nonce NB, 
    7.45 -                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
    7.46 +                         XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
    7.47               Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
    7.48                           Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
    7.49 -                         RA|} : set evs |]
    7.50 -          ==> Says B A RA # evs : recur"
    7.51 +                         RA|} : set evs4 |]
    7.52 +          ==> Says B A RA # evs4 : recur"
    7.53  
    7.54  (**No "oops" message can easily be expressed.  Each session key is
    7.55     associated--in two separate messages--with two nonces.
     8.1 --- a/src/HOL/Auth/WooLam.thy	Thu Sep 04 17:57:56 1997 +0200
     8.2 +++ b/src/HOL/Auth/WooLam.thy	Fri Sep 05 12:24:13 1997 +0200
     8.3 @@ -30,36 +30,36 @@
     8.4            ==> Says Spy B X  # evs : woolam"
     8.5  
     8.6           (*Alice initiates a protocol run*)
     8.7 -    WL1  "[| evs: woolam;  A ~= B |]
     8.8 -          ==> Says A B (Agent A) # evs : woolam"
     8.9 +    WL1  "[| evs1: woolam;  A ~= B |]
    8.10 +          ==> Says A B (Agent A) # evs1 : woolam"
    8.11  
    8.12           (*Bob responds to Alice's message with a challenge.*)
    8.13 -    WL2  "[| evs: woolam;  A ~= B;  
    8.14 -             Says A' B (Agent A) : set evs |]
    8.15 -          ==> Says B A (Nonce NB) # evs : woolam"
    8.16 +    WL2  "[| evs2: woolam;  A ~= B;  
    8.17 +             Says A' B (Agent A) : set evs2 |]
    8.18 +          ==> Says B A (Nonce NB) # evs2 : woolam"
    8.19  
    8.20           (*Alice responds to Bob's challenge by encrypting NB with her key.
    8.21             B is *not* properly determined -- Alice essentially broadcasts
    8.22             her reply.*)
    8.23 -    WL3  "[| evs: woolam;
    8.24 -             Says A  B (Agent A)  : set evs;
    8.25 -             Says B' A (Nonce NB) : set evs |]
    8.26 -          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs : woolam"
    8.27 +    WL3  "[| evs3: woolam;
    8.28 +             Says A  B (Agent A)  : set evs3;
    8.29 +             Says B' A (Nonce NB) : set evs3 |]
    8.30 +          ==> Says A B (Crypt (shrK A) (Nonce NB)) # evs3 : woolam"
    8.31  
    8.32           (*Bob forwards Alice's response to the Server.  NOTE: usually
    8.33             the messages are shown in chronological order, for clarity.
    8.34             But here, exchanging the two events would cause the lemma
    8.35             WL4_analz_sees_Spy to pick up the wrong assumption!*)
    8.36 -    WL4  "[| evs: woolam;  B ~= Server;  
    8.37 -             Says A'  B X         : set evs;
    8.38 -             Says A'' B (Agent A) : set evs |]
    8.39 -          ==> Says B Server {|Agent A, Agent B, X|} # evs : woolam"
    8.40 +    WL4  "[| evs4: woolam;  B ~= Server;  
    8.41 +             Says A'  B X         : set evs4;
    8.42 +             Says A'' B (Agent A) : set evs4 |]
    8.43 +          ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
    8.44  
    8.45           (*Server decrypts Alice's response for Bob.*)
    8.46 -    WL5  "[| evs: woolam;  B ~= Server;
    8.47 +    WL5  "[| evs5: woolam;  B ~= Server;
    8.48               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
    8.49 -               : set evs |]
    8.50 +               : set evs5 |]
    8.51            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    8.52 -                 # evs : woolam"
    8.53 +                 # evs5 : woolam"
    8.54  
    8.55  end
     9.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Sep 04 17:57:56 1997 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 05 12:24:13 1997 +0200
     9.3 @@ -26,44 +26,44 @@
     9.4            ==> Says Spy B X  # evs : yahalom"
     9.5  
     9.6           (*Alice initiates a protocol run*)
     9.7 -    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
     9.8 -          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
     9.9 +    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
    9.10 +          ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    9.11  
    9.12           (*Bob's response to Alice's message.  Bob doesn't know who 
    9.13  	   the sender is, hence the A' in the sender field.*)
    9.14 -    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
    9.15 -             Says A' B {|Agent A, Nonce NA|} : set evs |]
    9.16 +    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
    9.17 +             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    9.18            ==> Says B Server 
    9.19                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    9.20 -                # evs : yahalom"
    9.21 +                # evs2 : yahalom"
    9.22  
    9.23           (*The Server receives Bob's message.  He responds by sending a
    9.24              new session key to Alice, with a packet for forwarding to Bob.*)
    9.25 -    YM3  "[| evs: yahalom;  A ~= Server;  Key KAB ~: used evs;
    9.26 +    YM3  "[| evs3: yahalom;  A ~= Server;  Key KAB ~: used evs3;
    9.27               Says B' Server 
    9.28                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    9.29 -               : set evs |]
    9.30 +               : set evs3 |]
    9.31            ==> Says Server A
    9.32                     {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    9.33                       Crypt (shrK B) {|Agent A, Key KAB|}|}
    9.34 -                # evs : yahalom"
    9.35 +                # evs3 : yahalom"
    9.36  
    9.37           (*Alice receives the Server's (?) message, checks her Nonce, and
    9.38             uses the new session key to send Bob his Nonce.*)
    9.39 -    YM4  "[| evs: yahalom;  A ~= Server;  
    9.40 +    YM4  "[| evs4: yahalom;  A ~= Server;  
    9.41               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    9.42 -                        X|}  : set evs;
    9.43 -             Says A B {|Agent A, Nonce NA|} : set evs |]
    9.44 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
    9.45 +                        X|}  : set evs4;
    9.46 +             Says A B {|Agent A, Nonce NA|} : set evs4 |]
    9.47 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    9.48  
    9.49           (*This message models possible leaks of session keys.  The Nonces
    9.50             identify the protocol run.  Quoting Server here ensures they are
    9.51             correct.*)
    9.52 -    Oops "[| evs: yahalom;  A ~= Spy;
    9.53 +    Oops "[| evso: yahalom;  A ~= Spy;
    9.54               Says Server A {|Crypt (shrK A)
    9.55                                     {|Agent B, Key K, Nonce NA, Nonce NB|},
    9.56 -                             X|}  : set evs |]
    9.57 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
    9.58 +                             X|}  : set evso |]
    9.59 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    9.60  
    9.61  
    9.62  constdefs 
    10.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Sep 04 17:57:56 1997 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Sep 05 12:24:13 1997 +0200
    10.3 @@ -29,45 +29,45 @@
    10.4            ==> Says Spy B X  # evs : yahalom"
    10.5  
    10.6           (*Alice initiates a protocol run*)
    10.7 -    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
    10.8 -          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
    10.9 +    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
   10.10 +          ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
   10.11  
   10.12           (*Bob's response to Alice's message.  Bob doesn't know who 
   10.13  	   the sender is, hence the A' in the sender field.*)
   10.14 -    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
   10.15 -             Says A' B {|Agent A, Nonce NA|} : set evs |]
   10.16 +    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
   10.17 +             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
   10.18            ==> Says B Server 
   10.19                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   10.20 -                # evs : yahalom"
   10.21 +                # evs2 : yahalom"
   10.22  
   10.23           (*The Server receives Bob's message.  He responds by sending a
   10.24 -           new session key to Alice, with a packet for forwarding to Bob.
   10.25 -           !! Fields are reversed in the 2nd packet to prevent attacks!! *)
   10.26 -    YM3  "[| evs: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
   10.27 +           new session key to Alice, with a certificate for forwarding to Bob.
   10.28 +           Fields are reversed in the 2nd certificate to prevent attacks!! *)
   10.29 +    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
   10.30               Says B' Server {|Agent B, Nonce NB,
   10.31  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
   10.32 -               : set evs |]
   10.33 +               : set evs3 |]
   10.34            ==> Says Server A
   10.35                 {|Nonce NB, 
   10.36                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
   10.37                   Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
   10.38 -                 # evs : yahalom"
   10.39 +                 # evs3 : yahalom"
   10.40  
   10.41           (*Alice receives the Server's (?) message, checks her Nonce, and
   10.42             uses the new session key to send Bob his Nonce.*)
   10.43 -    YM4  "[| evs: yahalom;  A ~= Server;  
   10.44 +    YM4  "[| evs4: yahalom;  A ~= Server;  
   10.45               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   10.46 -                        X|}  : set evs;
   10.47 -             Says A B {|Agent A, Nonce NA|} : set evs |]
   10.48 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
   10.49 +                        X|}  : set evs4;
   10.50 +             Says A B {|Agent A, Nonce NA|} : set evs4 |]
   10.51 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
   10.52  
   10.53           (*This message models possible leaks of session keys.  The nonces
   10.54             identify the protocol run.  Quoting Server here ensures they are
   10.55             correct. *)
   10.56 -    Oops "[| evs: yahalom;  A ~= Spy;
   10.57 +    Oops "[| evso: yahalom;  A ~= Spy;
   10.58               Says Server A {|Nonce NB, 
   10.59                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   10.60 -                             X|}  : set evs |]
   10.61 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
   10.62 +                             X|}  : set evso |]
   10.63 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
   10.64  
   10.65  end