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.
--- a/src/HOL/Auth/NS_Public.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML Fri Jul 11 13:32:39 1997 +0200
@@ -5,6 +5,8 @@
Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
Version incorporating Lowe's fix (inclusion of B's identify in round 2).
+
+PROOFS BELOW MIGHT BE SIMPLIFIED using Yahalom's analz_mono_parts_induct_tac
*)
open NS_Public;
@@ -118,8 +120,8 @@
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (blast_tac (!claset delrules [conjI]
- addSDs [impOfSubs Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
+ addSDs [impOfSubs Fake_parts_insert]
+ addDs [impOfSubs analz_subset_parts]) 1);
val lemma = result();
goal thy
--- a/src/HOL/Auth/NS_Shared.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML Fri Jul 11 13:32:39 1997 +0200
@@ -33,16 +33,6 @@
(**** Inductive proofs about ns_shared ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> ns_shared lost' <= ns_shared lost";
-by (rtac subsetI 1);
-by (etac ns_shared.induct 1);
-by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
- :: ns_shared.intrs))));
-qed "ns_shared_mono";
-
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : ns_shared lost ==> ALL A X. Says A A X ~: set evs";
by (etac ns_shared.induct 1);
@@ -317,21 +307,6 @@
qed "Spy_not_see_encrypted_key";
-goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
-\ A ~: lost; B ~: lost; evs : ns_shared lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD])));
-qed "Agent_not_see_encrypted_key";
-
-
-
(**** Guarantees available at various stages of protocol ***)
A_trusts_NS2 RS conjunct2 RS Spy_not_see_encrypted_key;
--- a/src/HOL/Auth/OtwayRees.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML Fri Jul 11 13:32:39 1997 +0200
@@ -35,15 +35,6 @@
(**** Inductive proofs about otway ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
-by (rtac subsetI 1);
-by (etac otway.induct 1);
-by (ALLGOALS
- (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
- :: otway.intrs))));
-qed "otway_mono";
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
@@ -391,21 +382,6 @@
qed "Spy_not_see_encrypted_key";
-goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server B \
-\ {|NA, Crypt (shrK A) {|NA, Key K|}, \
-\ Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
-qed "Agent_not_see_encrypted_key";
-
-
(**** Authenticity properties relating to NB ****)
(*Only OR2 can have caused such a part of a message to appear. We do not
--- a/src/HOL/Auth/OtwayRees_AN.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jul 11 13:32:39 1997 +0200
@@ -32,15 +32,6 @@
(**** Inductive proofs about otway ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
-by (rtac subsetI 1);
-by (etac otway.induct 1);
-by (REPEAT_FIRST
- (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
- :: otway.intrs))));
-qed "otway_mono";
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
@@ -311,22 +302,6 @@
qed "Spy_not_see_encrypted_key";
-goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server B \
-\ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \
-\ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\ : set evs; \
-\ Says B Spy {|NA, NB, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : otway lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
-qed "Agent_not_see_encrypted_key";
-
-
(**** Authenticity properties relating to NB ****)
(*If the encrypted message appears then it originated with the Server!*)
--- a/src/HOL/Auth/Recur.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/Recur.ML Fri Jul 11 13:32:39 1997 +0200
@@ -74,15 +74,6 @@
(**** Inductive proofs about recur ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> recur lost' <= recur lost";
-by (rtac subsetI 1);
-by (etac recur.induct 1);
-by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
- :: recur.intrs))));
-qed "recur_mono";
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : recur lost ==> ALL A X. Says A A X ~: set evs";
by (etac recur.induct 1);
@@ -490,21 +481,6 @@
qed "Spy_not_see_session_key";
-goal thy
- "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} \
-\ : parts(sees lost Spy evs); \
-\ C ~: {A,A',Server}; \
-\ A ~: lost; A' ~: lost; evs : recur lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_session_key));
-by (REPEAT_FIRST
- (blast_tac
- (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono]))));
-qed "Agent_not_see_session_key";
-
-
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
--- a/src/HOL/Auth/Yahalom.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML Fri Jul 11 13:32:39 1997 +0200
@@ -34,16 +34,6 @@
(**** Inductive proofs about yahalom ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
-by (rtac subsetI 1);
-by (etac yahalom.induct 1);
-by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
- :: yahalom.intrs))));
-qed "yahalom_mono";
-
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
@@ -267,34 +257,14 @@
qed "Spy_not_see_encrypted_key";
-(*And other agents don't see the key either.*)
-goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server A \
-\ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, \
-\ Crypt (shrK B) {|Agent A, Key K|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
-qed "Agent_not_see_encrypted_key";
-
-
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
It simplifies the proof by discarding needless information about
analz (insert X (sees lost Spy evs))
*)
-val analz_mono_parts_induct_tac =
- etac yahalom.induct 1
+fun analz_mono_parts_induct_tac i =
+ etac yahalom.induct i
THEN
- REPEAT_FIRST
- (rtac impI THEN'
- dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
- mp_tac)
+ REPEAT_FIRST analz_mono_contra_tac
THEN parts_sees_tac;
@@ -346,7 +316,7 @@
\ Nonce NA, Nonce NB|}, \
\ Crypt (shrK B) {|Agent A, Key K|}|} \
\ : set evs)";
-by analz_mono_parts_induct_tac;
+by (analz_mono_parts_induct_tac 1);
(*YM3 & Fake*)
by (Blast_tac 2);
by (Fake_parts_insert_tac 1);
@@ -517,7 +487,7 @@
\ : parts(sees lost Spy evs) \
\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
\ ~: parts(sees lost Spy evs)";
-by analz_mono_parts_induct_tac;
+by (analz_mono_parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
addSIs [parts_insertI]
@@ -672,19 +642,6 @@
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
- It simplifies the proof by discarding needless information about
- analz (insert X (sees lost Spy evs))
-*)
-val analz_mono_parts_induct_tac =
- etac yahalom.induct 1
- THEN
- REPEAT_FIRST
- (rtac impI THEN'
- dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
- mp_tac)
- THEN parts_sees_tac;
-
(*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
NB matters for freshness.*)
@@ -696,7 +653,7 @@
\ : parts (sees lost Spy evs) --> \
\ B ~: lost --> \
\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
-by analz_mono_parts_induct_tac;
+by (analz_mono_parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
--- a/src/HOL/Auth/Yahalom2.ML Fri Jul 11 13:30:01 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML Fri Jul 11 13:32:39 1997 +0200
@@ -35,16 +35,6 @@
(**** Inductive proofs about yahalom ****)
-(*Monotonicity*)
-goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
-by (rtac subsetI 1);
-by (etac yahalom.induct 1);
-by (REPEAT_FIRST
- (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
- :: yahalom.intrs))));
-qed "yahalom_mono";
-
-
(*Nobody sends themselves messages*)
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
@@ -268,23 +258,6 @@
qed "Spy_not_see_encrypted_key";
-(*And other agents don't see the key either.*)
-goal thy
- "!!evs. [| C ~: {A,B,Server}; \
-\ Says Server A \
-\ {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, \
-\ Crypt (shrK B) {|nb, Key K, Agent A|}|} \
-\ : set evs; \
-\ Says A Spy {|na, nb, Key K|} ~: set evs; \
-\ A ~: lost; B ~: lost; evs : yahalom lost |] \
-\ ==> Key K ~: analz (sees lost C evs)";
-by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
-by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
-by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
-by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
-qed "Agent_not_see_encrypted_key";
-
-
(** Security Guarantee for A upon receiving YM3 **)
(*If the encrypted message appears then it originated with the Server.
@@ -399,15 +372,13 @@
It simplifies the proof by discarding needless information about
analz (insert X (sees lost Spy evs))
*)
-val analz_mono_parts_induct_tac =
- etac yahalom.induct 1
+fun analz_mono_parts_induct_tac i =
+ etac yahalom.induct i
THEN
- REPEAT_FIRST
- (rtac impI THEN'
- dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
- mp_tac)
+ REPEAT_FIRST analz_mono_contra_tac
THEN parts_sees_tac;
+
(*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
NB matters for freshness.*)
@@ -419,7 +390,7 @@
\ : parts (sees lost Spy evs) --> \
\ B ~: lost --> \
\ (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
-by analz_mono_parts_induct_tac;
+by (analz_mono_parts_induct_tac 1);
(*Fake*)
by (Fake_parts_insert_tac 1);
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)