Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
authorpaulson
Tue Sep 08 15:17:11 1998 +0200 (1998-09-08)
changeset 54349b4bed3f394c
parent 5433 b66a23a45377
child 5435 2487121d3bd1
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public.thy
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Public_Bad.thy
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Recur.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/WooLam.ML
src/HOL/Auth/WooLam.thy
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 08 14:54:21 1998 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Tue Sep 08 15:17:11 1998 +0200
     1.3 @@ -24,8 +24,7 @@
     1.4  
     1.5  
     1.6  (*A "possibility property": there are traces that reach the end.*)
     1.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
     1.8 -\     ==> EX Timestamp K. EX evs: kerberos_ban.    \
     1.9 +Goal "EX Timestamp K. EX evs: kerberos_ban.    \
    1.10  \            Says B A (Crypt K (Number Timestamp)) \
    1.11  \                 : set evs";
    1.12  by (cut_facts_tac [SesKeyLife_LB] 1);
    1.13 @@ -41,15 +40,6 @@
    1.14  
    1.15  (**** Inductive proofs about kerberos_ban ****)
    1.16  
    1.17 -(*Nobody sends themselves messages*)
    1.18 -Goal "evs : kerberos_ban ==> ALL X. Says A A X ~: set evs";
    1.19 -by (etac kerberos_ban.induct 1);
    1.20 -by Auto_tac;
    1.21 -qed_spec_mp "not_Says_to_self";
    1.22 -Addsimps [not_Says_to_self];
    1.23 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.24 -
    1.25 -
    1.26  (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
    1.27  Goal "Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
    1.28  \             ==> X : parts (spies evs)";
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 14:54:21 1998 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Tue Sep 08 15:17:11 1998 +0200
     2.3 @@ -48,18 +48,16 @@
     2.4  
     2.5      Nil  "[]: kerberos_ban"
     2.6  
     2.7 -
     2.8 -    Fake "[| evs: kerberos_ban;  B ~= Spy;  
     2.9 -             X: synth (analz (spies evs)) |]
    2.10 +    Fake "[| evs: kerberos_ban;  X: synth (analz (spies evs)) |]
    2.11            ==> Says Spy B X # evs : kerberos_ban"
    2.12  
    2.13  
    2.14 -    Kb1  "[| evs1: kerberos_ban;  A ~= Server |]
    2.15 +    Kb1  "[| evs1: kerberos_ban |]
    2.16            ==> Says A Server {|Agent A, Agent B|} # evs1
    2.17                  :  kerberos_ban"
    2.18  
    2.19  
    2.20 -    Kb2  "[| evs2: kerberos_ban;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    2.21 +    Kb2  "[| evs2: kerberos_ban;  Key KAB ~: used evs2;
    2.22               Says A' Server {|Agent A, Agent B|} : set evs2 |]
    2.23            ==> Says Server A 
    2.24                  (Crypt (shrK A)
    2.25 @@ -68,7 +66,7 @@
    2.26                  # evs2 : kerberos_ban"
    2.27  
    2.28  
    2.29 -    Kb3  "[| evs3: kerberos_ban;  A ~= B; 
    2.30 +    Kb3  "[| evs3: kerberos_ban;  
    2.31               Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) 
    2.32                 : set evs3;
    2.33               Says A Server {|Agent A, Agent B|} : set evs3;
    2.34 @@ -77,21 +75,19 @@
    2.35                 # evs3 : kerberos_ban"
    2.36  
    2.37  
    2.38 -    Kb4  "[| evs4: kerberos_ban;  A ~= B;  
    2.39 +    Kb4  "[| evs4: kerberos_ban;  
    2.40               Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), 
    2.41  		         (Crypt K {|Agent A, Number Ta|}) |}: set evs4;
    2.42 -             ~ Expired Ts evs4; 
    2.43 -             RecentAuth Ta evs4|]
    2.44 +             ~ Expired Ts evs4;  RecentAuth Ta evs4 |]
    2.45            ==> Says B A (Crypt K (Number Ta)) # evs4
    2.46                  : kerberos_ban"
    2.47  
    2.48 -
    2.49 -(*The session key has EXPIRED when it gets lost *)
    2.50 -    Oops "[| evso: kerberos_ban;  A ~= Spy;
    2.51 +         (*Old session keys may become compromised*)
    2.52 +    Oops "[| evso: kerberos_ban;  
    2.53               Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
    2.54                 : set evso;
    2.55               Expired Ts evso |]
    2.56 -          ==> Says A Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    2.57 +          ==> Notes Spy {|Number Ts, Key K|} # evso : kerberos_ban"
    2.58  
    2.59  
    2.60  end
     3.1 --- a/src/HOL/Auth/NS_Public.ML	Tue Sep 08 14:54:21 1998 +0200
     3.2 +++ b/src/HOL/Auth/NS_Public.ML	Tue Sep 08 15:17:11 1998 +0200
     3.3 @@ -14,8 +14,8 @@
     3.4  AddIffs [Spy_in_bad];
     3.5  
     3.6  (*A "possibility property": there are traces that reach the end*)
     3.7 -Goal "A ~= B ==> EX NB. EX evs: ns_public.               \
     3.8 -\                  Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
     3.9 +Goal
    3.10 +   "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    3.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    3.12  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    3.13  by possibility_tac;
    3.14 @@ -24,15 +24,6 @@
    3.15  
    3.16  (**** Inductive proofs about ns_public ****)
    3.17  
    3.18 -(*Nobody sends themselves messages*)
    3.19 -Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
    3.20 -by (etac ns_public.induct 1);
    3.21 -by Auto_tac;
    3.22 -qed_spec_mp "not_Says_to_self";
    3.23 -Addsimps [not_Says_to_self];
    3.24 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    3.25 -
    3.26 -
    3.27  (*Induction for regularity theorems.  If induction formula has the form
    3.28     X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    3.29     needless information about analz (insert X (spies evs))  *)
     4.1 --- a/src/HOL/Auth/NS_Public.thy	Tue Sep 08 14:54:21 1998 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.thy	Tue Sep 08 15:17:11 1998 +0200
     4.3 @@ -19,17 +19,16 @@
     4.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     4.5             invent new nonces here, but he can also use NS1.  Common to
     4.6             all similar protocols.*)
     4.7 -    Fake "[| evs: ns_public;  B ~= Spy;  
     4.8 -             X: synth (analz (spies evs)) |]
     4.9 +    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
    4.10            ==> Says Spy B X  # evs : ns_public"
    4.11  
    4.12           (*Alice initiates a protocol run, sending a nonce to Bob*)
    4.13 -    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
    4.14 +    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
    4.15            ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    4.16                   # evs1  :  ns_public"
    4.17  
    4.18           (*Bob responds to Alice's message with a further nonce*)
    4.19 -    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
    4.20 +    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
    4.21               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
    4.22            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
    4.23                  # evs2  :  ns_public"
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 08 14:54:21 1998 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Tue Sep 08 15:17:11 1998 +0200
     5.3 @@ -18,8 +18,8 @@
     5.4  AddIffs [Spy_in_bad];
     5.5  
     5.6  (*A "possibility property": there are traces that reach the end*)
     5.7 -Goal "A ~= B ==> EX NB. EX evs: ns_public.               \
     5.8 -\                  Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
     5.9 +Goal
    5.10 +  "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    5.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.12  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    5.13  by possibility_tac;
    5.14 @@ -28,15 +28,6 @@
    5.15  
    5.16  (**** Inductive proofs about ns_public ****)
    5.17  
    5.18 -(*Nobody sends themselves messages*)
    5.19 -Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs";
    5.20 -by (etac ns_public.induct 1);
    5.21 -by Auto_tac;
    5.22 -qed_spec_mp "not_Says_to_self";
    5.23 -Addsimps [not_Says_to_self];
    5.24 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    5.25 -
    5.26 -
    5.27  (*Induction for regularity theorems.  If induction formula has the form
    5.28     X ~: analz (spies evs) --> ... then it shortens the proof by discarding
    5.29     needless information about analz (insert X (spies evs))  *)
     6.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 08 14:54:21 1998 +0200
     6.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Tue Sep 08 15:17:11 1998 +0200
     6.3 @@ -23,17 +23,16 @@
     6.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     6.5             invent new nonces here, but he can also use NS1.  Common to
     6.6             all similar protocols.*)
     6.7 -    Fake "[| evs: ns_public;  B ~= Spy;  
     6.8 -             X: synth (analz (spies evs)) |]
     6.9 +    Fake "[| evs: ns_public;  X: synth (analz (spies evs)) |]
    6.10            ==> Says Spy B X  # evs : ns_public"
    6.11  
    6.12           (*Alice initiates a protocol run, sending a nonce to Bob*)
    6.13 -    NS1  "[| evs1: ns_public;  A ~= B;  Nonce NA ~: used evs1 |]
    6.14 +    NS1  "[| evs1: ns_public;  Nonce NA ~: used evs1 |]
    6.15            ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
    6.16                  # evs1  :  ns_public"
    6.17  
    6.18           (*Bob responds to Alice's message with a further nonce*)
    6.19 -    NS2  "[| evs2: ns_public;  A ~= B;  Nonce NB ~: used evs2;
    6.20 +    NS2  "[| evs2: ns_public;  Nonce NB ~: used evs2;
    6.21               Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs2 |]
    6.22            ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
    6.23                  # evs2  :  ns_public"
     7.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Sep 08 14:54:21 1998 +0200
     7.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Sep 08 15:17:11 1998 +0200
     7.3 @@ -16,7 +16,7 @@
     7.4  
     7.5  
     7.6  (*A "possibility property": there are traces that reach the end*)
     7.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]       \
     7.8 +Goal "[| A ~= Server |]       \
     7.9  \        ==> EX N K. EX evs: ns_shared.               \
    7.10  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    7.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    7.12 @@ -35,14 +35,6 @@
    7.13  
    7.14  (**** Inductive proofs about ns_shared ****)
    7.15  
    7.16 -(*Nobody sends themselves messages*)
    7.17 -Goal "evs : ns_shared ==> ALL X. Says A A X ~: set evs";
    7.18 -by (etac ns_shared.induct 1);
    7.19 -by Auto_tac;
    7.20 -qed_spec_mp "not_Says_to_self";
    7.21 -Addsimps [not_Says_to_self];
    7.22 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    7.23 -
    7.24  (*For reasoning about the encrypted portion of message NS3*)
    7.25  Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    7.26  \                ==> X : parts (spies evs)";
     8.1 --- a/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 14:54:21 1998 +0200
     8.2 +++ b/src/HOL/Auth/NS_Shared.thy	Tue Sep 08 15:17:11 1998 +0200
     8.3 @@ -21,12 +21,11 @@
     8.4           (*The spy MAY say anything he CAN say.  We do not expect him to
     8.5             invent new nonces here, but he can also use NS1.  Common to
     8.6             all similar protocols.*)
     8.7 -    Fake "[| evs: ns_shared;  B ~= Spy;  
     8.8 -             X: synth (analz (spies evs)) |]
     8.9 +    Fake "[| evs: ns_shared;  X: synth (analz (spies evs)) |]
    8.10            ==> Says Spy B X # evs : ns_shared"
    8.11  
    8.12           (*Alice initiates a protocol run, requesting to talk to any B*)
    8.13 -    NS1  "[| evs1: ns_shared;  A ~= Server;  Nonce NA ~: used evs1 |]
    8.14 +    NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
    8.15            ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    8.16                  :  ns_shared"
    8.17  
    8.18 @@ -34,7 +33,7 @@
    8.19             !! It may respond more than once to A's request !!
    8.20  	   Server doesn't know who the true sender is, hence the A' in
    8.21                 the sender field.*)
    8.22 -    NS2  "[| evs2: ns_shared;  A ~= B;  A ~= Server;  Key KAB ~: used evs2;
    8.23 +    NS2  "[| evs2: ns_shared;  Key KAB ~: used evs2;
    8.24               Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    8.25            ==> Says Server A 
    8.26                  (Crypt (shrK A)
    8.27 @@ -43,8 +42,8 @@
    8.28                  # evs2 : ns_shared"
    8.29  
    8.30            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    8.31 -            Can inductively show A ~= Server*)
    8.32 -    NS3  "[| evs3: ns_shared;  A ~= B;
    8.33 +            Need A ~= Server because we allow messages to self.*)
    8.34 +    NS3  "[| evs3: ns_shared;  A ~= Server;
    8.35               Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    8.36                 : set evs3;
    8.37               Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    8.38 @@ -52,7 +51,7 @@
    8.39  
    8.40           (*Bob's nonce exchange.  He does not know who the message came
    8.41             from, but responds to A because she is mentioned inside.*)
    8.42 -    NS4  "[| evs4: ns_shared;  A ~= B;  Nonce NB ~: used evs4;
    8.43 +    NS4  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
    8.44               Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    8.45            ==> Says B A (Crypt K (Nonce NB)) # evs4
    8.46                  : ns_shared"
    8.47 @@ -62,7 +61,7 @@
    8.48             We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    8.49             Letting the Spy add or subtract 1 lets him send ALL nonces.
    8.50             Instead we distinguish the messages by sending the nonce twice.*)
    8.51 -    NS5  "[| evs5: ns_shared;  A ~= B;  
    8.52 +    NS5  "[| evs5: ns_shared;  
    8.53               Says B' A (Crypt K (Nonce NB)) : set evs5;
    8.54               Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    8.55                 : set evs5 |]
     9.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 08 14:54:21 1998 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 08 15:17:11 1998 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4  
     9.5  
     9.6  (*A "possibility property": there are traces that reach the end*)
     9.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
     9.8 +Goal "[| B ~= Server |]   \
     9.9  \     ==> EX K. EX NA. EX evs: otway.          \
    9.10  \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    9.11  \              : set evs";
    9.12 @@ -30,15 +30,6 @@
    9.13  
    9.14  (**** Inductive proofs about otway ****)
    9.15  
    9.16 -(*Nobody sends themselves messages*)
    9.17 -Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
    9.18 -by (etac otway.induct 1);
    9.19 -by Auto_tac;
    9.20 -qed_spec_mp "not_Says_to_self";
    9.21 -Addsimps [not_Says_to_self];
    9.22 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    9.23 -
    9.24 -
    9.25  (** For reasoning about the encrypted portion of messages **)
    9.26  
    9.27  Goal "Says A' B {|N, Agent A, Agent B, X|} : set evs \
    10.1 --- a/src/HOL/Auth/OtwayRees.thy	Tue Sep 08 14:54:21 1998 +0200
    10.2 +++ b/src/HOL/Auth/OtwayRees.thy	Tue Sep 08 15:17:11 1998 +0200
    10.3 @@ -20,15 +20,16 @@
    10.4           (*Initial trace is empty*)
    10.5      Nil  "[]: otway"
    10.6  
    10.7 +         (** These rules allow agents to send messages to themselves **)
    10.8 +
    10.9           (*The spy MAY say anything he CAN say.  We do not expect him to
   10.10             invent new nonces here, but he can also use NS1.  Common to
   10.11             all similar protocols.*)
   10.12 -    Fake "[| evs: otway;  B ~= Spy;  
   10.13 -             X: synth (analz (spies evs)) |]
   10.14 +    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
   10.15            ==> Says Spy B X  # evs : otway"
   10.16  
   10.17           (*Alice initiates a protocol run*)
   10.18 -    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
   10.19 +    OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
   10.20            ==> Says A B {|Nonce NA, Agent A, Agent B, 
   10.21                           Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
   10.22                   # evs1 : otway"
   10.23 @@ -36,7 +37,7 @@
   10.24           (*Bob's response to Alice's message.  Bob doesn't know who 
   10.25  	   the sender is, hence the A' in the sender field.
   10.26             Note that NB is encrypted.*)
   10.27 -    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
   10.28 +    OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
   10.29               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
   10.30            ==> Says B Server 
   10.31                    {|Nonce NA, Agent A, Agent B, X, 
   10.32 @@ -47,7 +48,7 @@
   10.33           (*The Server receives Bob's message and checks that the three NAs
   10.34             match.  Then he sends a new session key to Bob with a packet for
   10.35             forwarding to Alice.*)
   10.36 -    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
   10.37 +    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
   10.38               Says B' Server 
   10.39                    {|Nonce NA, Agent A, Agent B, 
   10.40                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   10.41 @@ -60,8 +61,9 @@
   10.42                   # evs3 : otway"
   10.43  
   10.44           (*Bob receives the Server's (?) message and compares the Nonces with
   10.45 -	   those in the message he previously sent the Server.*)
   10.46 -    OR4  "[| evs4: otway;  A ~= B;  
   10.47 +	   those in the message he previously sent the Server.
   10.48 +           Need B ~= Server because we allow messages to self.*)
   10.49 +    OR4  "[| evs4: otway;  B ~= Server;
   10.50               Says B Server {|Nonce NA, Agent A, Agent B, X', 
   10.51                               Crypt (shrK B)
   10.52                                     {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
    11.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 08 14:54:21 1998 +0200
    11.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 08 15:17:11 1998 +0200
    11.3 @@ -18,10 +18,10 @@
    11.4  
    11.5  
    11.6  (*A "possibility property": there are traces that reach the end*)
    11.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]                            \
    11.8 -\  ==> EX K. EX NA. EX evs: otway.                                      \
    11.9 -\       Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
   11.10 -\       : set evs";
   11.11 +Goal "[| B ~= Server |]   \
   11.12 +\     ==> EX K. EX NA. EX evs: otway.                                      \
   11.13 +\          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
   11.14 +\            : set evs";
   11.15  by (REPEAT (resolve_tac [exI,bexI] 1));
   11.16  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
   11.17  by possibility_tac;
   11.18 @@ -30,15 +30,6 @@
   11.19  
   11.20  (**** Inductive proofs about otway ****)
   11.21  
   11.22 -(*Nobody sends themselves messages*)
   11.23 -Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
   11.24 -by (etac otway.induct 1);
   11.25 -by Auto_tac;
   11.26 -qed_spec_mp "not_Says_to_self";
   11.27 -Addsimps [not_Says_to_self];
   11.28 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   11.29 -
   11.30 -
   11.31  (** For reasoning about the encrypted portion of messages **)
   11.32  
   11.33  Goal "Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
   11.34 @@ -196,12 +187,12 @@
   11.35  (**** Authenticity properties relating to NA ****)
   11.36  
   11.37  (*If the encrypted message appears then it originated with the Server!*)
   11.38 -Goal "[| A ~: bad;  evs : otway |]                 \
   11.39 -\ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
   11.40 -\  --> (EX NB. Says Server B                                          \
   11.41 -\               {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   11.42 -\                 Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   11.43 -\               : set evs)";
   11.44 +Goal "[| A ~: bad;  A ~= B;  evs : otway |]                 \
   11.45 +\     ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
   11.46 +\      --> (EX NB. Says Server B                                          \
   11.47 +\                   {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   11.48 +\                     Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   11.49 +\                   : set evs)";
   11.50  by (parts_induct_tac 1);
   11.51  by (Blast_tac 1);
   11.52  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   11.53 @@ -214,7 +205,7 @@
   11.54    Freshness may be inferred from nonce NA.*)
   11.55  Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   11.56  \         : set evs;                                                 \
   11.57 -\        A ~: bad;  evs : otway |]                                  \
   11.58 +\        A ~: bad;  A ~= B;  evs : otway |]                          \
   11.59  \     ==> EX NB. Says Server B                                       \
   11.60  \                 {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
   11.61  \                   Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   11.62 @@ -266,8 +257,8 @@
   11.63    what it is.*)
   11.64  Goal "[| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   11.65  \         : set evs;                                                 \
   11.66 -\        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
   11.67 -\        A ~: bad;  B ~: bad;  evs : otway |]                    \
   11.68 +\        ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;             \
   11.69 +\        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]               \
   11.70  \     ==> Key K ~: analz (spies evs)";
   11.71  by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
   11.72  qed "A_gets_good_key";
   11.73 @@ -276,7 +267,7 @@
   11.74  (**** Authenticity properties relating to NB ****)
   11.75  
   11.76  (*If the encrypted message appears then it originated with the Server!*)
   11.77 -Goal "[| B ~: bad;  evs : otway |]                                 \
   11.78 +Goal "[| B ~: bad;  A ~= B;  evs : otway |]                              \
   11.79  \ ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
   11.80  \     --> (EX NA. Says Server B                                          \
   11.81  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   11.82 @@ -294,7 +285,7 @@
   11.83    has sent the correct message in round 3.*)
   11.84  Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   11.85  \          : set evs;                                                    \
   11.86 -\        B ~: bad;  evs : otway |]                                       \
   11.87 +\        B ~: bad;  A ~= B;  evs : otway |]                              \
   11.88  \     ==> EX NA. Says Server B                                           \
   11.89  \                  {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
   11.90  \                    Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
   11.91 @@ -305,9 +296,9 @@
   11.92  
   11.93  (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   11.94  Goal "[| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   11.95 -\         : set evs;                                            \
   11.96 -\        ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                \
   11.97 -\        A ~: bad;  B ~: bad;  evs : otway |]                   \
   11.98 +\         : set evs;                                                     \
   11.99 +\        ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
  11.100 +\        A ~: bad;  B ~: bad;  A ~= B;  evs : otway |]                   \
  11.101  \     ==> Key K ~: analz (spies evs)";
  11.102  by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
  11.103  qed "B_gets_good_key";
    12.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 08 14:54:21 1998 +0200
    12.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Tue Sep 08 15:17:11 1998 +0200
    12.3 @@ -28,24 +28,23 @@
    12.4           (*The spy MAY say anything he CAN say.  We do not expect him to
    12.5             invent new nonces here, but he can also use NS1.  Common to
    12.6             all similar protocols.*)
    12.7 -    Fake "[| evs: otway;  B ~= Spy;  
    12.8 -             X: synth (analz (spies evs)) |]
    12.9 +    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
   12.10            ==> Says Spy B X  # evs : otway"
   12.11  
   12.12           (*Alice initiates a protocol run*)
   12.13 -    OR1  "[| evs1: otway;  A ~= B;  B ~= Server |]
   12.14 +    OR1  "[| evs1: otway |]
   12.15            ==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
   12.16  
   12.17           (*Bob's response to Alice's message.  Bob doesn't know who 
   12.18  	   the sender is, hence the A' in the sender field.*)
   12.19 -    OR2  "[| evs2: otway;  B ~= Server;
   12.20 +    OR2  "[| evs2: otway;  
   12.21               Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
   12.22            ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.23                   # evs2 : otway"
   12.24  
   12.25           (*The Server receives Bob's message.  Then he sends a new
   12.26             session key to Bob with a packet for forwarding to Alice.*)
   12.27 -    OR3  "[| evs3: otway;  B ~= Server;  A ~= B;  Key KAB ~: used evs3;
   12.28 +    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
   12.29               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
   12.30                 : set evs3 |]
   12.31            ==> Says Server B 
   12.32 @@ -54,8 +53,9 @@
   12.33                # evs3 : otway"
   12.34  
   12.35           (*Bob receives the Server's (?) message and compares the Nonces with
   12.36 -	   those in the message he previously sent the Server.*)
   12.37 -    OR4  "[| evs4: otway;  A ~= B;
   12.38 +	   those in the message he previously sent the Server.
   12.39 +           Need B ~= Server because we allow messages to self.*)
   12.40 +    OR4  "[| evs4: otway;  B ~= Server; 
   12.41               Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
   12.42               Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
   12.43                 : set evs4 |]
    13.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 08 14:54:21 1998 +0200
    13.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 08 15:17:11 1998 +0200
    13.3 @@ -21,10 +21,10 @@
    13.4  
    13.5  
    13.6  (*A "possibility property": there are traces that reach the end*)
    13.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    13.8 -\  ==> EX K. EX NA. EX evs: otway.          \
    13.9 -\         Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
   13.10 -\           : set evs";
   13.11 +Goal "[| A ~= B; B ~= Server |]   \
   13.12 +\     ==> EX K. EX NA. EX evs: otway.          \
   13.13 +\           Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
   13.14 +\             : set evs";
   13.15  by (REPEAT (resolve_tac [exI,bexI] 1));
   13.16  by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
   13.17  by possibility_tac;
   13.18 @@ -33,14 +33,6 @@
   13.19  
   13.20  (**** Inductive proofs about otway ****)
   13.21  
   13.22 -(*Nobody sends themselves messages*)
   13.23 -Goal "evs : otway ==> ALL X. Says A A X ~: set evs";
   13.24 -by (etac otway.induct 1);
   13.25 -by Auto_tac;
   13.26 -qed_spec_mp "not_Says_to_self";
   13.27 -Addsimps [not_Says_to_self];
   13.28 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   13.29 -
   13.30  
   13.31  (** For reasoning about the encrypted portion of messages **)
   13.32  
   13.33 @@ -232,9 +224,8 @@
   13.34  (*** Attempting to prove stronger properties ***)
   13.35  
   13.36  (*Only OR1 can have caused such a part of a message to appear.
   13.37 -  I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
   13.38 -  Perhaps it's because OR2 has two similar-looking encrypted messages in
   13.39 -        this version.*)
   13.40 +  The premise A ~= B prevents OR2's similar-looking cryptogram from being
   13.41 +  picked up.  Original Otway-Rees doesn't need it.*)
   13.42  Goal "[| A ~: bad;  A ~= B;  evs : otway |]                \
   13.43  \     ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   13.44  \         Says A B {|NA, Agent A, Agent B,                  \
    14.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 08 14:54:21 1998 +0200
    14.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Tue Sep 08 15:17:11 1998 +0200
    14.3 @@ -22,11 +22,11 @@
    14.4           (*The spy MAY say anything he CAN say.  We do not expect him to
    14.5             invent new nonces here, but he can also use NS1.  Common to
    14.6             all similar protocols.*)
    14.7 -    Fake "[| evs: otway;  B ~= Spy;  X: synth (analz (spies evs)) |]
    14.8 +    Fake "[| evs: otway;  X: synth (analz (spies evs)) |]
    14.9            ==> Says Spy B X  # evs : otway"
   14.10  
   14.11           (*Alice initiates a protocol run*)
   14.12 -    OR1  "[| evs1: otway;  A ~= B;  B ~= Server;  Nonce NA ~: used evs1 |]
   14.13 +    OR1  "[| evs1: otway;  Nonce NA ~: used evs1 |]
   14.14            ==> Says A B {|Nonce NA, Agent A, Agent B, 
   14.15                           Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |} 
   14.16                   # evs1 : otway"
   14.17 @@ -34,7 +34,7 @@
   14.18           (*Bob's response to Alice's message.  Bob doesn't know who 
   14.19  	   the sender is, hence the A' in the sender field.
   14.20             We modify the published protocol by NOT encrypting NB.*)
   14.21 -    OR2  "[| evs2: otway;  B ~= Server;  Nonce NB ~: used evs2;
   14.22 +    OR2  "[| evs2: otway;  Nonce NB ~: used evs2;
   14.23               Says A' B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
   14.24            ==> Says B Server 
   14.25                    {|Nonce NA, Agent A, Agent B, X, Nonce NB,
   14.26 @@ -44,7 +44,7 @@
   14.27           (*The Server receives Bob's message and checks that the three NAs
   14.28             match.  Then he sends a new session key to Bob with a packet for
   14.29             forwarding to Alice.*)
   14.30 -    OR3  "[| evs3: otway;  B ~= Server;  Key KAB ~: used evs3;
   14.31 +    OR3  "[| evs3: otway;  Key KAB ~: used evs3;
   14.32               Says B' Server 
   14.33                    {|Nonce NA, Agent A, Agent B, 
   14.34                      Crypt (shrK A) {|Nonce NA, Agent A, Agent B|}, 
   14.35 @@ -58,8 +58,9 @@
   14.36                   # evs3 : otway"
   14.37  
   14.38           (*Bob receives the Server's (?) message and compares the Nonces with
   14.39 -	   those in the message he previously sent the Server.*)
   14.40 -    OR4  "[| evs4: otway;  A ~= B;
   14.41 +	   those in the message he previously sent the Server.
   14.42 +           Need B ~= Server because we allow messages to self.*)
   14.43 +    OR4  "[| evs4: otway;  A ~= B;  B ~= Server;
   14.44               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
   14.45                               Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
   14.46                 : set evs4;
    15.1 --- a/src/HOL/Auth/Recur.ML	Tue Sep 08 14:54:21 1998 +0200
    15.2 +++ b/src/HOL/Auth/Recur.ML	Tue Sep 08 15:17:11 1998 +0200
    15.3 @@ -8,7 +8,6 @@
    15.4  
    15.5  Pretty.setdepth 30;
    15.6  
    15.7 -
    15.8  AddEs spies_partsEs;
    15.9  AddDs [impOfSubs analz_subset_parts];
   15.10  AddDs [impOfSubs Fake_parts_insert];
   15.11 @@ -21,27 +20,24 @@
   15.12  
   15.13  
   15.14  (*Simplest case: Alice goes directly to the server*)
   15.15 -Goal "A ~= Server                                                      \
   15.16 -\ ==> EX K NA. EX evs: recur.                                           \
   15.17 -\  Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
   15.18 -\                  Agent Server|}  : set evs";
   15.19 +Goal "EX K NA. EX evs: recur.                                           \
   15.20 +\  Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},   \
   15.21 +\                  END|}  : set evs";
   15.22  by (REPEAT (resolve_tac [exI,bexI] 1));
   15.23 -by (rtac (recur.Nil RS recur.RA1 RS 
   15.24 -          (respond.One RSN (4,recur.RA3))) 2);
   15.25 +by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2);
   15.26  by possibility_tac;
   15.27  result();
   15.28  
   15.29  
   15.30  (*Case two: Alice, Bob and the server*)
   15.31 -Goal "[| A ~= B; A ~= Server; B ~= Server |]                 \
   15.32 -\ ==> EX K. EX NA. EX evs: recur.                               \
   15.33 -\    Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   15.34 -\               Agent Server|}  : set evs";
   15.35 +Goal "EX K. EX NA. EX evs: recur.                               \
   15.36 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   15.37 +\                  END|}  : set evs";
   15.38  by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
   15.39  by (REPEAT (eresolve_tac [exE, conjE] 1));
   15.40  by (REPEAT (resolve_tac [exI,bexI] 1));
   15.41  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS 
   15.42 -          (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
   15.43 +          (respond.One RS respond.Cons RSN (3,recur.RA3)) RS
   15.44            recur.RA4) 2);
   15.45  by basic_possibility_tac;
   15.46  by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
   15.47 @@ -50,17 +46,16 @@
   15.48  
   15.49  (*Case three: Alice, Bob, Charlie and the server
   15.50    TOO SLOW to run every time!
   15.51 -Goal "[| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
   15.52 -\ ==> EX K. EX NA. EX evs: recur.                                      \
   15.53 -\    Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
   15.54 -\               Agent Server|}  : set evs";
   15.55 +Goal "EX K. EX NA. EX evs: recur.                                      \
   15.56 +\       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
   15.57 +\                  END|}  : set evs";
   15.58  by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
   15.59  by (REPEAT (eresolve_tac [exE, conjE] 1));
   15.60  by (REPEAT (resolve_tac [exI,bexI] 1));
   15.61  by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS 
   15.62            (respond.One RS respond.Cons RS respond.Cons RSN
   15.63 -           (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
   15.64 -(*SLOW: 70 seconds*)
   15.65 +           (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
   15.66 +(*SLOW: 33 seconds*)
   15.67  by basic_possibility_tac;
   15.68  by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 
   15.69  		 ORELSE
   15.70 @@ -70,15 +65,6 @@
   15.71  
   15.72  (**** Inductive proofs about recur ****)
   15.73  
   15.74 -(*Nobody sends themselves messages*)
   15.75 -Goal "evs : recur ==> ALL X. Says A A X ~: set evs";
   15.76 -by (etac recur.induct 1);
   15.77 -by Auto_tac;
   15.78 -qed_spec_mp "not_Says_to_self";
   15.79 -Addsimps [not_Says_to_self];
   15.80 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   15.81 -
   15.82 -
   15.83  
   15.84  Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
   15.85  by (etac respond.induct 1);
   15.86 @@ -253,7 +239,7 @@
   15.87  by (etac responses.induct 2);
   15.88  by (ALLGOALS Asm_simp_tac);
   15.89  (*Fake*)
   15.90 -by (Fake_parts_insert_tac 1);
   15.91 +by (blast_tac (claset() addIs [parts_insertI]) 1);
   15.92  qed "Hash_imp_body";
   15.93  
   15.94  
   15.95 @@ -323,17 +309,6 @@
   15.96              (2, resp_analz_insert_lemma) RSN(2, rev_mp));
   15.97  
   15.98  
   15.99 -(*The Server does not send such messages.  This theorem lets us avoid
  15.100 -  assuming B~=Server in RA4.*)
  15.101 -Goal "evs : recur \
  15.102 -\     ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
  15.103 -by (etac recur.induct 1);
  15.104 -by (etac (respond.induct) 5);
  15.105 -by Auto_tac;
  15.106 -qed_spec_mp "Says_Server_not";
  15.107 -AddSEs [Says_Server_not RSN (2,rev_notE)];
  15.108 -
  15.109 -
  15.110  (*The last key returned by respond indeed appears in a certificate*)
  15.111  Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
  15.112  \   ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
    16.1 --- a/src/HOL/Auth/Recur.thy	Tue Sep 08 14:54:21 1998 +0200
    16.2 +++ b/src/HOL/Auth/Recur.thy	Tue Sep 08 15:17:11 1998 +0200
    16.3 @@ -8,6 +8,10 @@
    16.4  
    16.5  Recur = Shared +
    16.6  
    16.7 +(*End marker for message bundles*)
    16.8 +syntax        END :: msg
    16.9 +translations "END" == "Number 0"
   16.10 +
   16.11  (*Two session keys are distributed to each agent except for the initiator,
   16.12          who receives one.
   16.13    Perhaps the two session keys could be bundled into a single message.
   16.14 @@ -15,17 +19,15 @@
   16.15  consts     respond :: "event list => (msg*msg*key)set"
   16.16  inductive "respond evs" (*Server's response to the nested message*)
   16.17    intrs
   16.18 -    (*The message "Agent Server" marks the end of a list.*)
   16.19 -    One  "[| A ~= Server;  Key KAB ~: used evs |]
   16.20 -          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, 
   16.21 -               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
   16.22 +    One  "[| Key KAB ~: used evs |]
   16.23 +          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, 
   16.24 +               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
   16.25                 KAB)   : respond evs"
   16.26  
   16.27      (*The most recent session key is passed up to the caller*)
   16.28      Cons "[| (PA, RA, KAB) : respond evs;  
   16.29               Key KBC ~: used evs;  Key KBC ~: parts {RA};
   16.30 -             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
   16.31 -             B ~= Server |]
   16.32 +             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
   16.33            ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
   16.34                 {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
   16.35                   Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
   16.36 @@ -41,7 +43,7 @@
   16.37  inductive "responses evs"       
   16.38    intrs
   16.39      (*Server terminates lists*)
   16.40 -    Nil  "Agent Server : responses evs"
   16.41 +    Nil  "END : responses evs"
   16.42  
   16.43      Cons "[| RA : responses evs;  Key KAB ~: used evs |]
   16.44            ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
   16.45 @@ -56,35 +58,31 @@
   16.46  
   16.47           (*The spy MAY say anything he CAN say.  Common to
   16.48             all similar protocols.*)
   16.49 -    Fake "[| evs: recur;  B ~= Spy;  
   16.50 -             X: synth (analz (spies evs)) |]
   16.51 +    Fake "[| evs: recur;  X: synth (analz (spies evs)) |]
   16.52            ==> Says Spy B X  # evs : recur"
   16.53  
   16.54           (*Alice initiates a protocol run.
   16.55 -           "Agent Server" is just a placeholder, to terminate the nesting.*)
   16.56 -    RA1  "[| evs1: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs1 |]
   16.57 -          ==> Says A B 
   16.58 -                (Hash[Key(shrK A)] 
   16.59 -                 {|Agent A, Agent B, Nonce NA, Agent Server|})
   16.60 +           END is a placeholder to terminate the nesting.*)
   16.61 +    RA1  "[| evs1: recur;  Nonce NA ~: used evs1 |]
   16.62 +          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
   16.63                # evs1 : recur"
   16.64  
   16.65           (*Bob's response to Alice's message.  C might be the Server.
   16.66             We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
   16.67             it complicates proofs, so B may respond to any message at all!*)
   16.68 -    RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
   16.69 +    RA2  "[| evs2: recur;  Nonce NB ~: used evs2;
   16.70               Says A' B PA : set evs2 |]
   16.71            ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
   16.72                # evs2 : recur"
   16.73  
   16.74           (*The Server receives Bob's message and prepares a response.*)
   16.75 -    RA3  "[| evs3: recur;  B ~= Server;
   16.76 -             Says B' Server PB : set evs3;
   16.77 +    RA3  "[| evs3: recur;  Says B' Server PB : set evs3;
   16.78               (PB,RB,K) : respond evs3 |]
   16.79            ==> Says Server B RB # evs3 : recur"
   16.80  
   16.81           (*Bob receives the returned message and compares the Nonces with
   16.82             those in the message he previously sent the Server.*)
   16.83 -    RA4  "[| evs4: recur;  A ~= B;  
   16.84 +    RA4  "[| evs4: recur;  
   16.85               Says B  C {|XH, Agent B, Agent C, Nonce NB, 
   16.86                           XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
   16.87               Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
    17.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 08 14:54:21 1998 +0200
    17.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 08 15:17:11 1998 +0200
    17.3 @@ -82,8 +82,7 @@
    17.4           "[]: tls"
    17.5  
    17.6      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    17.7 -         "[| evs: tls;  B ~= Spy;  
    17.8 -             X: synth (analz (spies evs)) |]
    17.9 +         "[| evs: tls;  X: synth (analz (spies evs)) |]
   17.10            ==> Says Spy B X # evs : tls"
   17.11  
   17.12      SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
   17.13 @@ -100,7 +99,7 @@
   17.14             UNIX TIME is omitted because the protocol doesn't use it.
   17.15             May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
   17.16  	   while MASTER SECRET is 48 bytes*)
   17.17 -         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
   17.18 +         "[| evsCH: tls;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
   17.19            ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
   17.20  	        # evsCH  :  tls"
   17.21  
   17.22 @@ -109,14 +108,14 @@
   17.23  	   PB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   17.24             SERVER CERTIFICATE (7.4.2) is always present.
   17.25             CERTIFICATE_REQUEST (7.4.4) is implied.*)
   17.26 -         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   17.27 +         "[| evsSH: tls;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   17.28               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   17.29  	       : set evsSH |]
   17.30            ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
   17.31  
   17.32      Certificate
   17.33           (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
   17.34 -         "[| evsC: tls;  A ~= B |]
   17.35 +         "[| evsC: tls |]
   17.36            ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
   17.37  
   17.38      ClientKeyExch
   17.39 @@ -128,7 +127,7 @@
   17.40  	   both items have the same length, 48 bytes).
   17.41             The Note event records in the trace that she knows PMS
   17.42                 (see REMARK at top). *)
   17.43 -         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   17.44 +         "[| evsCX: tls;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   17.45               Says B' A (certificate B KB) : set evsCX |]
   17.46            ==> Says A B (Crypt KB (Nonce PMS))
   17.47  	      # Notes A {|Agent B, Nonce PMS|}
   17.48 @@ -140,7 +139,7 @@
   17.49            It adds the pre-master-secret, which is also essential!
   17.50            Checking the signature, which is the only use of A's certificate,
   17.51            assures B of A's presence*)
   17.52 -         "[| evsCV: tls;  A ~= B;  
   17.53 +         "[| evsCV: tls;  
   17.54               Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
   17.55  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   17.56            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
   17.57 @@ -206,6 +205,7 @@
   17.58            needed to resume this session.  The "Says A'' B ..." premise is
   17.59            used to prove Notes_master_imp_Crypt_PMS.*)
   17.60           "[| evsSA: tls;
   17.61 +	     A ~= B;
   17.62               Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
   17.63  	     M = PRF(PMS,NA,NB);  
   17.64  	     X = Hash{|Number SID, Nonce M,
   17.65 @@ -245,8 +245,9 @@
   17.66      Oops 
   17.67           (*The most plausible compromise is of an old session key.  Losing
   17.68             the MASTER SECRET or PREMASTER SECRET is more serious but
   17.69 -           rather unlikely.*)
   17.70 -         "[| evso: tls;  A ~= Spy;  
   17.71 +           rather unlikely.  The assumption A ~= Spy is essential: otherwise
   17.72 +           the Spy could learn session keys merely by replaying messages!*)
   17.73 +         "[| evso: tls;  A ~= Spy;
   17.74  	     Says A B (Crypt (sessionK((NA,NB,M),b)) X) : set evso |]
   17.75            ==> Says A Spy (Key (sessionK((NA,NB,M),b))) # evso  :  tls"
   17.76  
    18.1 --- a/src/HOL/Auth/WooLam.ML	Tue Sep 08 14:54:21 1998 +0200
    18.2 +++ b/src/HOL/Auth/WooLam.ML	Tue Sep 08 15:17:11 1998 +0200
    18.3 @@ -16,8 +16,7 @@
    18.4  
    18.5  
    18.6  (*A "possibility property": there are traces that reach the end*)
    18.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    18.8 -\     ==> EX NB. EX evs: woolam.               \
    18.9 +Goal "EX NB. EX evs: woolam.  \
   18.10  \           Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
   18.11  by (REPEAT (resolve_tac [exI,bexI] 1));
   18.12  by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
   18.13 @@ -28,15 +27,6 @@
   18.14  
   18.15  (**** Inductive proofs about woolam ****)
   18.16  
   18.17 -(*Nobody sends themselves messages*)
   18.18 -Goal "evs : woolam ==> ALL X. Says A A X ~: set evs";
   18.19 -by (etac woolam.induct 1);
   18.20 -by Auto_tac;
   18.21 -qed_spec_mp "not_Says_to_self";
   18.22 -Addsimps [not_Says_to_self];
   18.23 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   18.24 -
   18.25 -
   18.26  (** For reasoning about the encrypted portion of messages **)
   18.27  
   18.28  Goal "Says A' B X : set evs ==> X : analz (spies evs)";
    19.1 --- a/src/HOL/Auth/WooLam.thy	Tue Sep 08 14:54:21 1998 +0200
    19.2 +++ b/src/HOL/Auth/WooLam.thy	Tue Sep 08 15:17:11 1998 +0200
    19.3 @@ -22,20 +22,20 @@
    19.4           (*Initial trace is empty*)
    19.5      Nil  "[]: woolam"
    19.6  
    19.7 +         (** These rules allow agents to send messages to themselves **)
    19.8 +
    19.9           (*The spy MAY say anything he CAN say.  We do not expect him to
   19.10             invent new nonces here, but he can also use NS1.  Common to
   19.11             all similar protocols.*)
   19.12 -    Fake "[| evs: woolam;  B ~= Spy;  
   19.13 -             X: synth (analz (spies evs)) |]
   19.14 +    Fake "[| evs: woolam;  X: synth (analz (spies evs)) |]
   19.15            ==> Says Spy B X  # evs : woolam"
   19.16  
   19.17           (*Alice initiates a protocol run*)
   19.18 -    WL1  "[| evs1: woolam;  A ~= B |]
   19.19 +    WL1  "[| evs1: woolam |]
   19.20            ==> Says A B (Agent A) # evs1 : woolam"
   19.21  
   19.22           (*Bob responds to Alice's message with a challenge.*)
   19.23 -    WL2  "[| evs2: woolam;  A ~= B;  
   19.24 -             Says A' B (Agent A) : set evs2 |]
   19.25 +    WL2  "[| evs2: woolam;  Says A' B (Agent A) : set evs2 |]
   19.26            ==> Says B A (Nonce NB) # evs2 : woolam"
   19.27  
   19.28           (*Alice responds to Bob's challenge by encrypting NB with her key.
   19.29 @@ -50,13 +50,13 @@
   19.30             the messages are shown in chronological order, for clarity.
   19.31             But here, exchanging the two events would cause the lemma
   19.32             WL4_analz_spies to pick up the wrong assumption!*)
   19.33 -    WL4  "[| evs4: woolam;  B ~= Server;  
   19.34 +    WL4  "[| evs4: woolam;  
   19.35               Says A'  B X         : set evs4;
   19.36               Says A'' B (Agent A) : set evs4 |]
   19.37            ==> Says B Server {|Agent A, Agent B, X|} # evs4 : woolam"
   19.38  
   19.39           (*Server decrypts Alice's response for Bob.*)
   19.40 -    WL5  "[| evs5: woolam;  B ~= Server;
   19.41 +    WL5  "[| evs5: woolam;  
   19.42               Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|}
   19.43                 : set evs5 |]
   19.44            ==> Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|})
    20.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Sep 08 14:54:21 1998 +0200
    20.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 08 15:17:11 1998 +0200
    20.3 @@ -14,7 +14,7 @@
    20.4  
    20.5  
    20.6  (*A "possibility property": there are traces that reach the end*)
    20.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    20.8 +Goal "A ~= Server \
    20.9  \     ==> EX X NB K. EX evs: yahalom.          \
   20.10  \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   20.11  by (REPEAT (resolve_tac [exI,bexI] 1));
   20.12 @@ -26,14 +26,6 @@
   20.13  
   20.14  (**** Inductive proofs about yahalom ****)
   20.15  
   20.16 -(*Nobody sends themselves messages*)
   20.17 -Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
   20.18 -by (etac yahalom.induct 1);
   20.19 -by Auto_tac;
   20.20 -qed_spec_mp "not_Says_to_self";
   20.21 -Addsimps [not_Says_to_self];
   20.22 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   20.23 -
   20.24  
   20.25  (** For reasoning about the encrypted portion of messages **)
   20.26  
   20.27 @@ -109,8 +101,7 @@
   20.28  (*Describes the form of K when the Server sends this message.  Useful for
   20.29    Oops as well as main secrecy property.*)
   20.30  Goal "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
   20.31 -\          : set evs;                                                   \
   20.32 -\        evs : yahalom |]                                          \
   20.33 +\          : set evs;   evs : yahalom |]                                \
   20.34  \     ==> K ~: range shrK";
   20.35  by (etac rev_mp 1);
   20.36  by (etac yahalom.induct 1);
    21.1 --- a/src/HOL/Auth/Yahalom.thy	Tue Sep 08 14:54:21 1998 +0200
    21.2 +++ b/src/HOL/Auth/Yahalom.thy	Tue Sep 08 15:17:11 1998 +0200
    21.3 @@ -21,17 +21,16 @@
    21.4           (*The spy MAY say anything he CAN say.  We do not expect him to
    21.5             invent new nonces here, but he can also use NS1.  Common to
    21.6             all similar protocols.*)
    21.7 -    Fake "[| evs: yahalom;  B ~= Spy;  
    21.8 -             X: synth (analz (spies evs)) |]
    21.9 +    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
   21.10            ==> Says Spy B X  # evs : yahalom"
   21.11  
   21.12           (*Alice initiates a protocol run*)
   21.13 -    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
   21.14 +    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
   21.15            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
   21.16  
   21.17           (*Bob's response to Alice's message.  Bob doesn't know who 
   21.18  	   the sender is, hence the A' in the sender field.*)
   21.19 -    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
   21.20 +    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
   21.21               Says A' B {|Agent A, Nonce NA|} : set evs2 |]
   21.22            ==> Says B Server 
   21.23                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   21.24 @@ -39,7 +38,7 @@
   21.25  
   21.26           (*The Server receives Bob's message.  He responds by sending a
   21.27              new session key to Alice, with a packet for forwarding to Bob.*)
   21.28 -    YM3  "[| evs3: yahalom;  A ~= Server;  Key KAB ~: used evs3;
   21.29 +    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
   21.30               Says B' Server 
   21.31                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
   21.32                 : set evs3 |]
   21.33 @@ -50,8 +49,8 @@
   21.34  
   21.35           (*Alice receives the Server's (?) message, checks her Nonce, and
   21.36             uses the new session key to send Bob his Nonce.  The premise
   21.37 -           A ~= Server is needed to prove Says_Server_message_form.*)
   21.38 -    YM4  "[| evs4: yahalom;  A ~= Server;  
   21.39 +           A ~= Server is needed to prove Says_Server_not_range.*)
   21.40 +    YM4  "[| evs4: yahalom;  A ~= Server;
   21.41               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
   21.42                          X|}  : set evs4;
   21.43               Says A B {|Agent A, Nonce NA|} : set evs4 |]
    22.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 08 14:54:21 1998 +0200
    22.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 08 15:17:11 1998 +0200
    22.3 @@ -18,8 +18,7 @@
    22.4  
    22.5  
    22.6  (*A "possibility property": there are traces that reach the end*)
    22.7 -Goal "[| A ~= B; A ~= Server; B ~= Server |]   \
    22.8 -\     ==> EX X NB K. EX evs: yahalom.          \
    22.9 +Goal "EX X NB K. EX evs: yahalom.          \
   22.10  \            Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   22.11  by (REPEAT (resolve_tac [exI,bexI] 1));
   22.12  by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
   22.13 @@ -30,15 +29,6 @@
   22.14  
   22.15  (**** Inductive proofs about yahalom ****)
   22.16  
   22.17 -(*Nobody sends themselves messages*)
   22.18 -Goal "evs: yahalom ==> ALL X. Says A A X ~: set evs";
   22.19 -by (etac yahalom.induct 1);
   22.20 -by Auto_tac;
   22.21 -qed_spec_mp "not_Says_to_self";
   22.22 -Addsimps [not_Says_to_self];
   22.23 -AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   22.24 -
   22.25 -
   22.26  (** For reasoning about the encrypted portion of messages **)
   22.27  
   22.28  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   22.29 @@ -114,7 +104,7 @@
   22.30  Goal "[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
   22.31  \         : set evs;                                            \
   22.32  \        evs : yahalom |]                                       \
   22.33 -\     ==> K ~: range shrK & A ~= B";
   22.34 +\     ==> K ~: range shrK";
   22.35  by (etac rev_mp 1);
   22.36  by (etac yahalom.induct 1);
   22.37  by (ALLGOALS Asm_simp_tac);
   22.38 @@ -191,8 +181,7 @@
   22.39  
   22.40  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   22.41  
   22.42 -Goal "[| A ~: bad;  B ~: bad;  A ~= B;                       \
   22.43 -\        evs : yahalom |]                                    \
   22.44 +Goal "[| A ~: bad;  B ~: bad;  evs : yahalom |]              \
   22.45  \     ==> Says Server A                                      \
   22.46  \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|},     \
   22.47  \                 Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|} \
    23.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 14:54:21 1998 +0200
    23.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Sep 08 15:17:11 1998 +0200
    23.3 @@ -24,17 +24,16 @@
    23.4           (*The spy MAY say anything he CAN say.  We do not expect him to
    23.5             invent new nonces here, but he can also use NS1.  Common to
    23.6             all similar protocols.*)
    23.7 -    Fake "[| evs: yahalom;  B ~= Spy;  
    23.8 -             X: synth (analz (spies evs)) |]
    23.9 +    Fake "[| evs: yahalom;  X: synth (analz (spies evs)) |]
   23.10            ==> Says Spy B X  # evs : yahalom"
   23.11  
   23.12           (*Alice initiates a protocol run*)
   23.13 -    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
   23.14 +    YM1  "[| evs1: yahalom;  Nonce NA ~: used evs1 |]
   23.15            ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
   23.16  
   23.17           (*Bob's response to Alice's message.  Bob doesn't know who 
   23.18  	   the sender is, hence the A' in the sender field.*)
   23.19 -    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
   23.20 +    YM2  "[| evs2: yahalom;  Nonce NB ~: used evs2;
   23.21               Says A' B {|Agent A, Nonce NA|} : set evs2 |]
   23.22            ==> Says B Server 
   23.23                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
   23.24 @@ -43,7 +42,7 @@
   23.25           (*The Server receives Bob's message.  He responds by sending a
   23.26             new session key to Alice, with a certificate for forwarding to Bob.
   23.27             Both agents are quoted in the 2nd certificate to prevent attacks!*)
   23.28 -    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
   23.29 +    YM3  "[| evs3: yahalom;  Key KAB ~: used evs3;
   23.30               Says B' Server {|Agent B, Nonce NB,
   23.31  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
   23.32                 : set evs3 |]
   23.33 @@ -55,7 +54,7 @@
   23.34  
   23.35           (*Alice receives the Server's (?) message, checks her Nonce, and
   23.36             uses the new session key to send Bob his Nonce.*)
   23.37 -    YM4  "[| evs4: yahalom;  A ~= Server;  
   23.38 +    YM4  "[| evs4: yahalom;  
   23.39               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
   23.40                          X|}  : set evs4;
   23.41               Says A B {|Agent A, Nonce NA|} : set evs4 |]