Removal of monotonicity reasoning involving "lost" and the theorem
authorpaulson
Fri Jul 11 13:32:39 1997 +0200 (1997-07-11)
changeset 3516470626799511
parent 3515 d8a71f6eaf40
child 3517 2547f33fa33a
Removal of monotonicity reasoning involving "lost" and the theorem
Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder
to prove when Notes is available.
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Fri Jul 11 13:30:01 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Jul 11 13:32:39 1997 +0200
     1.3 @@ -5,6 +5,8 @@
     1.4  
     1.5  Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
     1.6  Version incorporating Lowe's fix (inclusion of B's identify in round 2).
     1.7 +
     1.8 +PROOFS BELOW MIGHT BE SIMPLIFIED using Yahalom's analz_mono_parts_induct_tac 
     1.9  *)
    1.10  
    1.11  open NS_Public;
    1.12 @@ -118,8 +120,8 @@
    1.13  by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.14  by (ex_strip_tac 1);
    1.15  by (blast_tac (!claset delrules [conjI]
    1.16 -                      addSDs [impOfSubs Fake_parts_insert]
    1.17 -                      addDs  [impOfSubs analz_subset_parts]) 1);
    1.18 +                       addSDs [impOfSubs Fake_parts_insert]
    1.19 +                       addDs  [impOfSubs analz_subset_parts]) 1);
    1.20  val lemma = result();
    1.21  
    1.22  goal thy 
     2.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Jul 11 13:30:01 1997 +0200
     2.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Jul 11 13:32:39 1997 +0200
     2.3 @@ -33,16 +33,6 @@
     2.4  
     2.5  (**** Inductive proofs about ns_shared ****)
     2.6  
     2.7 -(*Monotonicity*)
     2.8 -goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
     2.9 -by (rtac subsetI 1);
    2.10 -by (etac ns_shared.induct 1);
    2.11 -by (REPEAT_FIRST
    2.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    2.13 -                              :: ns_shared.intrs))));
    2.14 -qed "ns_shared_mono";
    2.15 -
    2.16 -
    2.17  (*Nobody sends themselves messages*)
    2.18  goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
    2.19  by (etac ns_shared.induct 1);
    2.20 @@ -317,21 +307,6 @@
    2.21  qed "Spy_not_see_encrypted_key";
    2.22  
    2.23  
    2.24 -goal thy 
    2.25 - "!!evs. [| C ~: {A,B,Server};                                          \
    2.26 -\           Says Server A                                               \
    2.27 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
    2.28 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
    2.29 -\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
    2.30 -\        ==> Key K ~: analz (sees lost C evs)";
    2.31 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    2.32 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    2.33 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    2.34 -by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
    2.35 -qed "Agent_not_see_encrypted_key";
    2.36 -
    2.37 -
    2.38 -
    2.39  (**** Guarantees available at various stages of protocol ***)
    2.40  
    2.41  A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
     3.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Jul 11 13:30:01 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Jul 11 13:32:39 1997 +0200
     3.3 @@ -35,15 +35,6 @@
     3.4  
     3.5  (**** Inductive proofs about otway ****)
     3.6  
     3.7 -(*Monotonicity*)
     3.8 -goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
     3.9 -by (rtac subsetI 1);
    3.10 -by (etac otway.induct 1);
    3.11 -by (ALLGOALS
    3.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    3.13 -                              :: otway.intrs))));
    3.14 -qed "otway_mono";
    3.15 -
    3.16  (*Nobody sends themselves messages*)
    3.17  goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    3.18  by (etac otway.induct 1);
    3.19 @@ -391,21 +382,6 @@
    3.20  qed "Spy_not_see_encrypted_key";
    3.21  
    3.22  
    3.23 -goal thy 
    3.24 - "!!evs. [| C ~: {A,B,Server};                                           \
    3.25 -\           Says Server B                                                \
    3.26 -\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
    3.27 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
    3.28 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
    3.29 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
    3.30 -\        ==> Key K ~: analz (sees lost C evs)";
    3.31 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    3.32 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    3.33 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    3.34 -by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
    3.35 -qed "Agent_not_see_encrypted_key";
    3.36 -
    3.37 -
    3.38  (**** Authenticity properties relating to NB ****)
    3.39  
    3.40  (*Only OR2 can have caused such a part of a message to appear.  We do not
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 11 13:30:01 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jul 11 13:32:39 1997 +0200
     4.3 @@ -32,15 +32,6 @@
     4.4  
     4.5  (**** Inductive proofs about otway ****)
     4.6  
     4.7 -(*Monotonicity*)
     4.8 -goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
     4.9 -by (rtac subsetI 1);
    4.10 -by (etac otway.induct 1);
    4.11 -by (REPEAT_FIRST
    4.12 -    (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    4.13 -                              :: otway.intrs))));
    4.14 -qed "otway_mono";
    4.15 -
    4.16  (*Nobody sends themselves messages*)
    4.17  goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
    4.18  by (etac otway.induct 1);
    4.19 @@ -311,22 +302,6 @@
    4.20  qed "Spy_not_see_encrypted_key";
    4.21  
    4.22  
    4.23 -goal thy 
    4.24 - "!!evs. [| C ~: {A,B,Server};                                      \
    4.25 -\           Says Server B                                           \
    4.26 -\              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    4.27 -\                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    4.28 -\             : set evs;                                            \
    4.29 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
    4.30 -\           A ~: lost;  B ~: lost;  evs : otway lost |]             \
    4.31 -\        ==> Key K ~: analz (sees lost C evs)";
    4.32 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    4.33 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    4.34 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    4.35 -by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
    4.36 -qed "Agent_not_see_encrypted_key";
    4.37 -
    4.38 -
    4.39  (**** Authenticity properties relating to NB ****)
    4.40  
    4.41  (*If the encrypted message appears then it originated with the Server!*)
     5.1 --- a/src/HOL/Auth/Recur.ML	Fri Jul 11 13:30:01 1997 +0200
     5.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jul 11 13:32:39 1997 +0200
     5.3 @@ -74,15 +74,6 @@
     5.4  
     5.5  (**** Inductive proofs about recur ****)
     5.6  
     5.7 -(*Monotonicity*)
     5.8 -goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost";
     5.9 -by (rtac subsetI 1);
    5.10 -by (etac recur.induct 1);
    5.11 -by (REPEAT_FIRST
    5.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    5.13 -                              :: recur.intrs))));
    5.14 -qed "recur_mono";
    5.15 -
    5.16  (*Nobody sends themselves messages*)
    5.17  goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
    5.18  by (etac recur.induct 1);
    5.19 @@ -490,21 +481,6 @@
    5.20  qed "Spy_not_see_session_key";
    5.21  
    5.22  
    5.23 -goal thy 
    5.24 - "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}         \
    5.25 -\              : parts(sees lost Spy evs);                \
    5.26 -\           C ~: {A,A',Server};                           \
    5.27 -\           A ~: lost;  A' ~: lost;  evs : recur lost |]  \
    5.28 -\        ==> Key K ~: analz (sees lost C evs)";
    5.29 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    5.30 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    5.31 -by (FIRSTGOAL (rtac Spy_not_see_session_key));
    5.32 -by (REPEAT_FIRST
    5.33 -    (blast_tac
    5.34 -     (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
    5.35 -qed "Agent_not_see_session_key";
    5.36 -
    5.37 -
    5.38  (**** Authenticity properties for Agents ****)
    5.39  
    5.40  (*The response never contains Hashes*)
     6.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jul 11 13:30:01 1997 +0200
     6.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jul 11 13:32:39 1997 +0200
     6.3 @@ -34,16 +34,6 @@
     6.4  
     6.5  (**** Inductive proofs about yahalom ****)
     6.6  
     6.7 -(*Monotonicity*)
     6.8 -goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
     6.9 -by (rtac subsetI 1);
    6.10 -by (etac yahalom.induct 1);
    6.11 -by (REPEAT_FIRST
    6.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    6.13 -                              :: yahalom.intrs))));
    6.14 -qed "yahalom_mono";
    6.15 -
    6.16 -
    6.17  (*Nobody sends themselves messages*)
    6.18  goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    6.19  by (etac yahalom.induct 1);
    6.20 @@ -267,34 +257,14 @@
    6.21  qed "Spy_not_see_encrypted_key";
    6.22  
    6.23  
    6.24 -(*And other agents don't see the key either.*)
    6.25 -goal thy 
    6.26 - "!!evs. [| C ~: {A,B,Server};                                    \
    6.27 -\           Says Server A                                         \
    6.28 -\              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
    6.29 -\                Crypt (shrK B) {|Agent A, Key K|}|}              \
    6.30 -\             : set evs;                                          \
    6.31 -\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
    6.32 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    6.33 -\        ==> Key K ~: analz (sees lost C evs)";
    6.34 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    6.35 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    6.36 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    6.37 -by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
    6.38 -qed "Agent_not_see_encrypted_key";
    6.39 -
    6.40 -
    6.41  (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
    6.42    It simplifies the proof by discarding needless information about
    6.43  	analz (insert X (sees lost Spy evs)) 
    6.44  *)
    6.45 -val analz_mono_parts_induct_tac = 
    6.46 -    etac yahalom.induct 1 
    6.47 +fun analz_mono_parts_induct_tac i = 
    6.48 +    etac yahalom.induct i
    6.49      THEN 
    6.50 -    REPEAT_FIRST  
    6.51 -      (rtac impI THEN' 
    6.52 -       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    6.53 -       mp_tac)  
    6.54 +    REPEAT_FIRST analz_mono_contra_tac
    6.55      THEN  parts_sees_tac;
    6.56  
    6.57  
    6.58 @@ -346,7 +316,7 @@
    6.59  \                                  Nonce NA, Nonce NB|},                \
    6.60  \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
    6.61  \                       : set evs)";
    6.62 -by analz_mono_parts_induct_tac;
    6.63 +by (analz_mono_parts_induct_tac 1);
    6.64  (*YM3 & Fake*)
    6.65  by (Blast_tac 2);
    6.66  by (Fake_parts_insert_tac 1);
    6.67 @@ -517,7 +487,7 @@
    6.68  \       : parts(sees lost Spy evs)                   \
    6.69  \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
    6.70  \       ~: parts(sees lost Spy evs)";
    6.71 -by analz_mono_parts_induct_tac;
    6.72 +by (analz_mono_parts_induct_tac 1);
    6.73  by (Fake_parts_insert_tac 1);
    6.74  by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
    6.75                         addSIs [parts_insertI]
    6.76 @@ -672,19 +642,6 @@
    6.77  
    6.78  (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
    6.79  
    6.80 -(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
    6.81 -  It simplifies the proof by discarding needless information about
    6.82 -	analz (insert X (sees lost Spy evs)) 
    6.83 -*)
    6.84 -val analz_mono_parts_induct_tac = 
    6.85 -    etac yahalom.induct 1 
    6.86 -    THEN 
    6.87 -    REPEAT_FIRST  
    6.88 -      (rtac impI THEN' 
    6.89 -       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    6.90 -       mp_tac)  
    6.91 -    THEN  parts_sees_tac;
    6.92 -
    6.93  (*Assuming the session key is secure, if both certificates are present then
    6.94    A has said NB.  We can't be sure about the rest of A's message, but only
    6.95    NB matters for freshness.*)  
    6.96 @@ -696,7 +653,7 @@
    6.97  \              : parts (sees lost Spy evs) -->                          \
    6.98  \            B ~: lost -->                                              \
    6.99  \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   6.100 -by analz_mono_parts_induct_tac;
   6.101 +by (analz_mono_parts_induct_tac 1);
   6.102  (*Fake*)
   6.103  by (Fake_parts_insert_tac 1);
   6.104  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
     7.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Jul 11 13:30:01 1997 +0200
     7.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jul 11 13:32:39 1997 +0200
     7.3 @@ -35,16 +35,6 @@
     7.4  
     7.5  (**** Inductive proofs about yahalom ****)
     7.6  
     7.7 -(*Monotonicity*)
     7.8 -goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
     7.9 -by (rtac subsetI 1);
    7.10 -by (etac yahalom.induct 1);
    7.11 -by (REPEAT_FIRST
    7.12 -    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    7.13 -			       :: yahalom.intrs))));
    7.14 -qed "yahalom_mono";
    7.15 -
    7.16 -
    7.17  (*Nobody sends themselves messages*)
    7.18  goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
    7.19  by (etac yahalom.induct 1);
    7.20 @@ -268,23 +258,6 @@
    7.21  qed "Spy_not_see_encrypted_key";
    7.22  
    7.23  
    7.24 -(*And other agents don't see the key either.*)
    7.25 -goal thy 
    7.26 - "!!evs. [| C ~: {A,B,Server};                                    \
    7.27 -\           Says Server A                                         \
    7.28 -\              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
    7.29 -\                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
    7.30 -\           : set evs;                                            \
    7.31 -\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
    7.32 -\           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
    7.33 -\        ==> Key K ~: analz (sees lost C evs)";
    7.34 -by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    7.35 -by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    7.36 -by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    7.37 -by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
    7.38 -qed "Agent_not_see_encrypted_key";
    7.39 -
    7.40 -
    7.41  (** Security Guarantee for A upon receiving YM3 **)
    7.42  
    7.43  (*If the encrypted message appears then it originated with the Server.
    7.44 @@ -399,15 +372,13 @@
    7.45    It simplifies the proof by discarding needless information about
    7.46  	analz (insert X (sees lost Spy evs)) 
    7.47  *)
    7.48 -val analz_mono_parts_induct_tac = 
    7.49 -    etac yahalom.induct 1 
    7.50 +fun analz_mono_parts_induct_tac i = 
    7.51 +    etac yahalom.induct i
    7.52      THEN 
    7.53 -    REPEAT_FIRST  
    7.54 -      (rtac impI THEN' 
    7.55 -       dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
    7.56 -       mp_tac)  
    7.57 +    REPEAT_FIRST analz_mono_contra_tac
    7.58      THEN  parts_sees_tac;
    7.59  
    7.60 +
    7.61  (*Assuming the session key is secure, if both certificates are present then
    7.62    A has said NB.  We can't be sure about the rest of A's message, but only
    7.63    NB matters for freshness.*)  
    7.64 @@ -419,7 +390,7 @@
    7.65  \              : parts (sees lost Spy evs) -->                          \
    7.66  \            B ~: lost -->                                              \
    7.67  \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
    7.68 -by analz_mono_parts_induct_tac;
    7.69 +by (analz_mono_parts_induct_tac 1);
    7.70  (*Fake*)
    7.71  by (Fake_parts_insert_tac 1);
    7.72  (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)