Added new guarantees for A and B
authorpaulson
Tue, 01 Oct 1996 15:49:29 +0200
changeset 2048 bb54fbba0071
parent 2047 a3701c4343ea
child 2049 d3b93e1765bc
Added new guarantees for A and B
src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 10:43:58 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Oct 01 15:49:29 1996 +0200
@@ -43,25 +43,6 @@
                               :: otway.intrs))));
 qed "otway_mono";
 
-(*The Spy can see more than anybody else, except for their initial state*)
-goal thy 
- "!!evs. evs : otway lost ==> \
-\     sees lost A evs <= initState lost A Un sees lost Spy evs";
-by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
-                                addss (!simpset))));
-qed "sees_agent_subset_sees_Spy";
-
-(*The Spy can see more than anybody else who's lost their key!*)
-goal thy 
- "!!evs. evs : otway lost ==> \
-\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
-by (etac otway.induct 1);
-by (agent.induct_tac "A" 1);
-by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
-qed_spec_mp "sees_lost_agent_subset_sees_Spy";
-
-
 (*Nobody sends themselves messages*)
 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
 by (etac otway.induct 1);
@@ -418,7 +399,7 @@
 
 
 
-(**** Towards proving stronger authenticity properties ****)
+(**** Authenticity properties relating to NA ****)
 
 (*Only OR1 can have caused such a part of a message to appear.*)
 goal thy 
@@ -443,8 +424,8 @@
 goal thy 
  "!!evs. [| evs : otway lost; A ~: lost |]               \
 \ ==> EX B'. ALL B.    \
-\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) --> \
-\        B = B'";
+\        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \
+\        --> B = B'";
 by (etac otway.induct 1);
 by parts_Fake_tac;
 by (ALLGOALS Asm_simp_tac);
@@ -463,9 +444,9 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs); \ 
-\          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees lost Spy evs); \ 
-\          evs : otway lost;  A ~: lost |]                                         \
+ "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A): parts(sees lost Spy evs); \
+\          Crypt {|NA, Agent A, Agent C|} (shrK A): parts(sees lost Spy evs); \
+\          evs : otway lost;  A ~: lost |]                                    \
 \        ==> B = C";
 by (dtac lemma 1);
 by (assume_tac 1);
@@ -473,7 +454,7 @@
 (*Duplicate the assumption*)
 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
 by (fast_tac (!claset addSDs [spec]) 1);
-qed "unique_OR1_nonce";
+qed "unique_NA";
 
 
 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
@@ -503,19 +484,18 @@
 qed_spec_mp"no_nonce_OR1_OR2";
 
 
-
 (*If the encrypted message appears, and A has used Nonce NA to start a run,
   then it originated with the Server!*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                     \
-\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
-\            Says A B {|Nonce NA, Agent A, Agent B,                          \
-\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
-\             : set_of_list evs -->                                          \
-\            (EX NB. Says Server B                                           \
-\                 {|Nonce NA,                                                \
-\                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
-\                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
+\    ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs)      \
+\        --> Says A B {|NA, Agent A, Agent B,                          \
+\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}      \
+\             : set_of_list evs -->                                    \
+\            (EX NB. Says Server B                                     \
+\                 {|NA,                                                \
+\                   Crypt {|NA, Key K|} (shrK A),                      \
+\                   Crypt {|NB, Key K|} (shrK B)|}                     \
 \                   : set_of_list evs)";
 by (etac otway.induct 1);
 by parts_Fake_tac;
@@ -538,31 +518,31 @@
 (*OR3*)  (** LEVEL 8 **)
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
-                      addSEs [MPair_parts]
-                      addEs  [unique_OR1_nonce]) 1);
 by (fast_tac (!claset addSEs [MPair_parts]
                       addSDs [Says_imp_sees_Spy RS parts.Inj]
                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
-                      delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
-qed_spec_mp "Crypt_imp_Server_msg";
+                      delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+                      addSEs [MPair_parts]
+                      addEs  [unique_NA]) 1);
+qed_spec_mp "NA_Crypt_imp_Server_msg";
 
 
 (*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   then the key really did come from the Server!  CANNOT prove this of the
-  lost form of this protocol, even though we can prove
+  bad form of this protocol, even though we can prove
   Spy_not_see_encrypted_key*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
-\        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
-\             : set_of_list evs -->                                      \
-\            Says A B {|Nonce NA, Agent A, Agent B,                      \
-\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
-\             : set_of_list evs -->                                      \
-\            (EX NB. Says Server B                                       \
-\                     {|Nonce NA,                                        \
-\                       Crypt {|Nonce NA, Key K|} (shrK A),              \
-\                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]             \
+\        ==> Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}        \
+\             : set_of_list evs -->                                \
+\            Says A B {|NA, Agent A, Agent B,                      \
+\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
+\             : set_of_list evs -->                                \
+\            (EX NB. Says Server B                                 \
+\                     {|NA,                                        \
+\                       Crypt {|NA, Key K|} (shrK A),              \
+\                       Crypt {|NB, Key K|} (shrK B)|}             \
 \                       : set_of_list evs)";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
@@ -581,16 +561,15 @@
                       addDs [Says_imp_sees_Spy RS parts.Inj]) 3);
 (** LEVEL 8 **)
 (*Still subcases of Fake and OR4*)
-by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
+by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addDs  [impOfSubs analz_subset_parts]) 1);
-by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
+by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
                       addEs  partsEs
                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
-val OR4_imp_Says_Server_A = 
+val A_can_trust = 
     result() RSN (2, rev_mp) RS mp |> standard;
 
 
-
 (*Describes the form of K and NA when the Server sends this message.*)
 goal thy 
  "!!evs. [| Says Server B \
@@ -598,22 +577,25 @@
 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
 \           evs : otway lost |]                                        \
 \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
-\            (EX i. NA = Nonce i)";
+\            (EX i. NA = Nonce i) &                  \
+\            (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
-by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 qed "Says_Server_message_form";
 
 
-(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 **)
+(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
+    Does not in itself guarantee security: an attack could violate 
+    the premises, e.g. by having A=Spy **)
 
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
-\        ==> Says Server B                                             \
-\              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
-\                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
-\            Says A Spy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
-\            Key(newK evt) ~: analz (sees lost Spy evs)";
+\        ==> Says Server B                                                 \
+\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
+\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
+\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
+\            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by (dtac OR2_analz_sees_Spy 4);
 by (dtac OR4_analz_sees_Spy 6);
@@ -628,25 +610,25 @@
 (*OR3*)
 by (fast_tac (!claset addSIs [parts_insertI]
                       addEs [Says_imp_old_keys RS less_irrefl]
-                      addss (!simpset)) 3);
+                      addss (!simpset addsimps [parts_insert2])) 3);
 (*Reveal case 2, OR4, OR2, Fake*) 
 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
 (*Reveal case 1*) (** LEVEL 8 **)
 by (excluded_middle_tac "Aa : lost" 1);
-(*But this contradicts Key(newK evt) ~: analz (sees lost Spy evsa) *)
+(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
 by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
 (*So now we have  Aa ~: lost *)
-by (dtac OR4_imp_Says_Server_A 1);
+by (dtac A_can_trust 1);
 by (REPEAT (assume_tac 1));
 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 goal thy 
  "!!evs. [| Says Server B \
-\            {|NA, Crypt {|NA, K|} (shrK A),                      \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
-\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
+\            {|NA, Crypt {|NA, K|} (shrK A),                             \
+\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
+\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -655,11 +637,11 @@
 
 
 goal thy 
- "!!evs. [| C ~: {A,B,Server}; \
-\           Says Server B \
-\            {|NA, Crypt {|NA, K|} (shrK A),                      \
-\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
-\           Says A Spy {|NA, K|} ~: set_of_list evs;            \
+ "!!evs. [| C ~: {A,B,Server};                                           \
+\           Says Server B                                                \
+\            {|NA, Crypt {|NA, K|} (shrK A),                             \
+\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
+\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -669,8 +651,136 @@
 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
+  know anything about X'.*)
+goal thy 
+ "!!evs. [| B ~: lost;  evs : otway lost |]                    \
+\        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
+\             : parts (sees lost Spy evs) -->                  \
+\            (EX X'. Says B Server                             \
+\             {|NA, Agent A, Agent B, X',                      \
+\               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
+\             : set_of_list evs)";
+by (etac otway.induct 1);
+by parts_Fake_tac;
+by (ALLGOALS Asm_simp_tac);
+(*Fake*)
+by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
+                              impOfSubs Fake_parts_insert]) 2);
+by (Auto_tac());
+qed_spec_mp "Crypt_imp_OR2";
+
+
+(** The Nonce NB uniquely identifies B's  message. **)
+
+goal thy 
+ "!!evs. [| evs : otway lost; B ~: lost |]               \
+\ ==> EX NA' A'. ALL NA A.                              \
+\      Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \
+\      --> NA = NA' & A = A'";
+by (etac otway.induct 1);
+by parts_Fake_tac;
+by (ALLGOALS Asm_simp_tac);
+(*Fake*)
+by (best_tac (!claset delrules [conjI,conjE]
+		      addSDs [impOfSubs analz_subset_parts,
+                              impOfSubs Fake_parts_insert]) 2);
+(*Base case*)
+by (fast_tac (!claset addss (!simpset)) 1);
+by (Step_tac 1);
+(*OR2: creation of new Nonce.  Move assertion into global context*)
+by (excluded_middle_tac "NB = Nonce (newN evsa)" 1);
+by (Asm_simp_tac 1);
+by (fast_tac (!claset addSIs [exI]) 1);
+by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
+val lemma = result();
+
+goal thy 
+ "!!evs.[| Crypt {|NA, NB, Agent A, Agent B|} (shrK B) \
+\                  : parts(sees lost Spy evs);         \
+\          Crypt {|NC, NB, Agent C, Agent B|} (shrK B) \
+\                  : parts(sees lost Spy evs);         \
+\          evs : otway lost;  B ~: lost |]             \
+\        ==> NC = NA & C = A";
+by (dtac lemma 1);
+by (assume_tac 1);
+by (REPEAT (etac exE 1));
+(*Duplicate the assumption*)
+by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
+by (fast_tac (!claset addSDs [spec]) 1);
+qed "unique_NB";
+
+
+(*If the encrypted message appears, and B has used Nonce NB,
+  then it originated with the Server!*)
+goal thy 
+ "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
+\    ==> Crypt {|NB, Key K|} (shrK B) : parts (sees lost Spy evs)        \
+\        --> (ALL X'. Says B Server                                      \
+\                       {|NA, Agent A, Agent B, X',                      \
+\                         Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
+\             : set_of_list evs                                          \
+\             --> Says Server B                                          \
+\                  {|NA, Crypt {|NA, Key K|} (shrK A),                   \
+\                        Crypt {|NB, Key K|} (shrK B)|}                  \
+\                   : set_of_list evs)";
+by (etac otway.induct 1);
+by parts_Fake_tac;
+by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
+(*Fake*)
+by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
+                              impOfSubs Fake_parts_insert]) 1);
+(*OR1: it cannot be a new Nonce, contradiction.*)
+by (fast_tac (!claset addSIs [parts_insertI]
+                      addSEs partsEs
+                      addEs [Says_imp_old_nonces RS less_irrefl]
+                      addss (!simpset)) 1);
+(*OR3 and OR4*)  (** LEVEL 5 **)
+(*OR4*)
+by (REPEAT (Safe_step_tac 2));
+br (Crypt_imp_OR2 RS exE) 2;
+by (REPEAT (fast_tac (!claset addEs partsEs) 2));
+(*OR3*)  (** LEVEL 8 **)
+by (step_tac (!claset delrules [disjCI, impCE]) 1);
+by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
+                      addSEs [MPair_parts]
+                      addDs  [unique_NB]) 2);
+by (fast_tac (!claset addSEs [MPair_parts]
+                      addSDs [Says_imp_sees_Spy RS parts.Inj]
+                      addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
+                      delrules [conjI, impCE] (*stop split-up*)) 1);
+qed_spec_mp "NB_Crypt_imp_Server_msg";
+
+
+(*Guarantee for B: if it gets a message with matching NB then the Server
+  has sent the correct message.*)
+goal thy 
+ "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
+\           Says S B {|NA, X, Crypt {|NB, Key K|} (shrK B)|}       \
+\            : set_of_list evs;                                    \
+\           Says B Server {|NA, Agent A, Agent B, X',              \
+\                           Crypt {|NA, NB, Agent A, Agent B|}     \
+\                                 (shrK B)|}                       \
+\            : set_of_list evs |]                                  \
+\        ==> Says Server B                                         \
+\                 {|NA,                                            \
+\                   Crypt {|NA, Key K|} (shrK A),                  \
+\                   Crypt {|NB, Key K|} (shrK B)|}                 \
+\                   : set_of_list evs";
+by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
+                      addEs  partsEs
+                      addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
+qed "B_can_trust";
+
+
+B_can_trust RS Spy_not_see_encrypted_key;
+
+
 (** A session key uniquely identifies a pair of senders in the message
-    encrypted by a good agent C. **)
+    encrypted by a good agent C.  NEEDED?  INTERESTING?**)
 goal thy 
  "!!evs. evs : otway lost ==>                                           \
 \      EX A B. ALL C N.                                            \