--- a/src/HOL/Auth/Yahalom.ML Fri Sep 13 13:15:48 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML Fri Sep 13 13:16:57 1996 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Auth/OtwayRees
+(* Title: HOL/Auth/Yahalom
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -10,11 +10,25 @@
Proc. Royal Soc. 426 (1989)
*)
-open OtwayRees;
+open Yahalom;
proof_timing:=true;
HOL_quantifiers := false;
+
+(** Weak liveness: there are traces that reach the end **)
+
+goal thy
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+\ ==> EX X NB K. EX evs: yahalom. \
+\ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2;
+by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
+by (ALLGOALS Fast_tac);
+qed "weak_liveness";
+
+
(**** Inductive proofs about yahalom ****)
(*The Enemy can see more than anybody else, except for their initial state*)
@@ -45,30 +59,19 @@
(** For reasoning about the encrypted portion of messages **)
-goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
-\ X : analz (sees Enemy evs)";
-by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
-qed "YM2_analz_sees_Enemy";
-
-goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
+(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \
\ X : analz (sees Enemy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
qed "YM4_analz_sees_Enemy";
-goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
+goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \
+\ : set_of_list evs ==> \
\ K : parts (sees Enemy evs)";
by (fast_tac (!claset addSEs partsEs
addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
-qed "YM5_parts_sees_Enemy";
+qed "YM4_parts_sees_Enemy";
-(*YM2_analz... and YM4_analz... let us treat those cases using the same
- argument as for the Fake case. This is possible for most, but not all,
- proofs: Fake does not invent new nonces (as in YM2), and of course Fake
- messages originate from the Enemy. *)
-
-val YM2_YM4_tac =
- dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
- dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
(*** Shared keys are not betrayed ***)
@@ -78,11 +81,13 @@
"!!evs. [| evs : yahalom; A ~: bad |] ==> \
\ Key (shrK A) ~: parts (sees Enemy evs)";
be yahalom.induct 1;
-by YM2_YM4_tac;
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+by (ALLGOALS Asm_simp_tac);
+by (stac insert_commute 3);
by (Auto_tac());
-(*Deals with Fake message*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]) 1);
+(*Fake and YM4 are similar*)
+by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
+ impOfSubs Fake_parts_insert])));
qed "Enemy_not_see_shrK";
bind_thm ("Enemy_not_analz_shrK",
@@ -94,7 +99,7 @@
As usual fast_tac cannot be used because it uses the equalities too soon*)
val major::prems =
goal thy "[| Key (shrK A) : parts (sees Enemy evs); \
-\ evs : yahalom; \
+\ evs : yahalom; \
\ A:bad ==> R \
\ |] ==> R";
br ccontr 1;
@@ -121,13 +126,11 @@
\ length evs <= length evs' --> \
\ Key (newK evs') ~: (UN C. parts (sees C evs))";
be yahalom.induct 1;
-by YM2_YM4_tac;
-(*auto_tac does not work here, as it performs safe_tac first*)
-by (ALLGOALS Asm_simp_tac);
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
+ impOfSubs parts_insert_subset_Un,
+ Suc_leD]
+ addss (!simpset))));
val lemma = result();
(*Variant needed for the main theorem below*)
@@ -156,27 +159,24 @@
\ length evs <= length evs' --> \
\ newK evs' ~: keysFor (UN C. parts (sees C evs))";
be yahalom.induct 1;
-by YM2_YM4_tac;
-bd YM5_parts_sees_Enemy 7;
-by (ALLGOALS Asm_simp_tac);
-(*YM1 and YM3*)
-by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
-(*Fake, YM2, YM4: these messages send unknown (X) components*)
-by (EVERY
- (map
+by (forward_tac [YM4_parts_sees_Enemy] 6);
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
+by (ALLGOALS Asm_full_simp_tac);
+(*YM1, YM2 and YM3*)
+by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
+(*Fake and YM4: these messages send unknown (X) components*)
+by (stac insert_commute 2);
+by (Simp_tac 2);
+(*YM4: the only way K could have been used is if it had been seen,
+ contradicting new_keys_not_seen*)
+by (ALLGOALS
(best_tac
- (!claset addSDs [newK_invKey]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
impOfSubs (parts_insert_subset_Un RS keysFor_mono),
Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)))
- [3,2,1]));
-(*YM5: dummy message*)
-by (best_tac (!claset addSDs [newK_invKey]
- addEs [new_keys_not_seen RSN(2,rev_notE)]
- addIs [less_SucI, impOfSubs keysFor_mono]
- addss (!simpset addsimps [le_def])) 1);
+ addDs [impOfSubs analz_subset_parts]
+ addEs [new_keys_not_seen RSN(2,rev_notE)]
+ addss (!simpset))));
val lemma = result();
goal thy
@@ -214,14 +214,16 @@
\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \
\ Key K : parts {X} --> Key K : parts (sees Enemy evs)";
be yahalom.induct 1;
-by YM2_YM4_tac;
+bd (YM4_analz_sees_Enemy RS synth.Inj) 6;
by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
(*Deals with Faked messages*)
-by (best_tac (!claset addSEs partsEs
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 2);
-(*Base case and YM5*)
+by (EVERY
+ (map (best_tac (!claset addSEs partsEs
+ addDs [impOfSubs analz_subset_parts,
+ impOfSubs parts_insert_subset_Un]
+ addss (!simpset)))
+ [3,2]));
+(*Base case*)
by (Auto_tac());
result();
@@ -259,19 +261,6 @@
(** Session keys are not used to encrypt other session keys **)
-(*Could generalize this so that the X component doesn't have to be first
- in the message?*)
-val enemy_analz_tac =
- SELECT_GOAL
- (EVERY [REPEAT (resolve_tac [impI,notI] 1),
- dtac (impOfSubs Fake_analz_insert) 1,
- eresolve_tac [asm_rl, synth.Inj] 1,
- Fast_tac 1,
- Asm_full_simp_tac 1,
- IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
- ]);
-
-
(*Lemma for the trivial direction of the if-and-only-if*)
goal thy
"!!evs. (Key K : analz (Key``nE Un sEe)) --> \
@@ -286,34 +275,23 @@
\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
\ (K : newK``E | Key K : analz (sees Enemy evs))";
be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
bd YM4_analz_sees_Enemy 6;
by (REPEAT_FIRST (resolve_tac [allI, lemma]));
-by (ALLGOALS (*Takes 35 secs*)
+by (ALLGOALS
(asm_simp_tac
(!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
@ pushes)
setloop split_tac [expand_if])));
(*YM4*)
-by (enemy_analz_tac 5);
+by (enemy_analz_tac 4);
(*YM3*)
-by (Fast_tac 4);
-(*YM2*) (** LEVEL 7 **)
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
- (insert_commute RS ssubst) 3);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
- (insert_commute RS ssubst) 3);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
-by (enemy_analz_tac 3);
-(*Fake case*) (** LEVEL 11 **)
-by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")]
- (insert_commute RS ssubst) 2);
+by (Fast_tac 3);
+(*Fake case*)
by (enemy_analz_tac 2);
(*Base case*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
qed_spec_mp "analz_image_newK";
-
goal thy
"!!evs. evs : yahalom ==> \
\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
@@ -326,29 +304,28 @@
(*Describes the form *and age* of K when the following message is sent*)
goal thy
- "!!evs. [| Says Server B \
-\ {|NA, Crypt {|NA, K|} (shrK A), \
-\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \
+ "!!evs. [| Says Server A \
+\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
+\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
\ evs : yahalom |] \
-\ ==> (EX evt:yahalom. K = Key(newK evt) & \
-\ length evt < length evs) & \
-\ (EX i. NA = Nonce i)";
+\ ==> (EX evt:yahalom. K = Key(newK evt) & \
+\ length evt < length evs)";
be rev_mp 1;
be yahalom.induct 1;
by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
qed "Says_Server_message_form";
-(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
+(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3
+ As with Otway-Rees, proof does not need uniqueness of session keys.*)
goal thy
"!!evs. [| Says Server A \
-\ {|NA, Crypt {|NA, K|} (shrK B), \
-\ Crypt {|NB, K|} (shrK A)|} : set_of_list evs; \
-\ A ~: bad; B ~: bad; evs : yahalom |] ==> \
+\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \
+\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \
+\ A ~: bad; B ~: bad; evs : yahalom |] ==> \
\ K ~: analz (sees Enemy evs)";
be rev_mp 1;
be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
bd YM4_analz_sees_Enemy 6;
by (ALLGOALS Asm_simp_tac);
(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
@@ -360,87 +337,10 @@
(!simpset addsimps ([analz_subset_parts RS contra_subsetD,
analz_insert_Key_newK] @ pushes)
setloop split_tac [expand_if])));
+(*YM4*)
+by (enemy_analz_tac 3);
(*YM3*)
-by (fast_tac (!claset addSEs [less_irrefl]) 3);
+by (fast_tac (!claset addSEs [less_irrefl]) 2);
(*Fake*) (** LEVEL 10 **)
-by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
-by (enemy_analz_tac 1);
-(*YM4*)
-by (mp_tac 2);
-by (enemy_analz_tac 2);
-(*YM2*)
-by (mp_tac 1);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
- (insert_commute RS ssubst) 1);
-by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (enemy_analz_tac 1);
qed "Enemy_not_see_encrypted_key";
-
-
-
-(*** Session keys are issued at most once, and identify the principals ***)
-
-(** First, two lemmas for the Fake, YM2 and YM4 cases **)
-
-goal thy
- "!!evs. [| X : synth (analz (sees Enemy evs)); \
-\ Crypt X' (shrK C) : parts{X}; \
-\ C ~: bad; evs : yahalom |] \
-\ ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
-by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
- addDs [impOfSubs parts_insert_subset_Un]
- addss (!simpset)) 1);
-qed "Crypt_Fake_parts";
-
-goal thy
- "!!evs. [| Crypt X' K : parts (sees A evs); evs : yahalom |] \
-\ ==> EX S S' Y. Says S S' Y : set_of_list evs & \
-\ Crypt X' K : parts {Y}";
-bd parts_singleton 1;
-by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
-qed "Crypt_parts_singleton";
-
-fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
-
-(*The Key K uniquely identifies a pair of senders in the message encrypted by
- C, but if C=Enemy then he could send all sorts of nonsense.*)
-goal thy
- "!!evs. evs : yahalom ==> \
-\ EX A B. ALL C. \
-\ C ~: bad --> \
-\ (ALL S S' X. Says S S' X : set_of_list evs --> \
-\ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
-by (Simp_tac 1);
-be yahalom.induct 1;
-bd YM2_analz_sees_Enemy 4;
-bd YM4_analz_sees_Enemy 6;
-by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
-by (REPEAT_FIRST (etac exE));
-(*YM4*)
-by (ex_strip_tac 4);
-by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts,
- Crypt_parts_singleton]) 4);
-(*YM3: Case split propagates some context to other subgoal...*)
- (** LEVEL 8 **)
-by (excluded_middle_tac "K = newK evsa" 3);
-by (Asm_simp_tac 3);
-by (REPEAT (ares_tac [exI] 3));
-(*...we prove this case by contradiction: the key is too new!*)
-by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
- addSEs partsEs
- addEs [Says_imp_old_keys RS less_irrefl]
- addss (!simpset)) 3);
-(*YM2*) (** LEVEL 12 **)
-by (ex_strip_tac 2);
-by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
- (insert_commute RS ssubst) 2);
-by (Simp_tac 2);
-by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts,
- Crypt_parts_singleton]) 2);
-(*Fake*) (** LEVEL 16 **)
-by (ex_strip_tac 1);
-by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
-qed "unique_session_keys";
-
-(*It seems strange but this theorem is NOT needed to prove the main result!*)
--- a/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:15:48 1996 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:16:57 1996 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Auth/OtwayRees
+(* Title: HOL/Auth/Yahalom
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -10,7 +10,7 @@
Proc. Royal Soc. 426 (1989)
*)
-OtwayRees = Shared +
+Yahalom = Shared +
consts yahalom :: "event list set"
inductive yahalom
@@ -26,13 +26,12 @@
(*Alice initiates a protocol run*)
YM1 "[| evs: yahalom; A ~= B |]
- ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
+ ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom"
(*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.
- We modify the published protocol by NOT encrypting NB.*)
+ the sender is, hence the A' in the sender field.*)
YM2 "[| evs: yahalom; B ~= Server;
- Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
+ Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says B Server
{|Agent B,
Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
@@ -40,34 +39,23 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3 "[| evs: yahalom; B ~= Server;
+ YM3 "[| evs: yahalom; A ~= Server;
Says B' Server
- {|Nonce NA, Agent A, Agent B,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK A),
- Nonce NB,
- Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
+ {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}
: set_of_list evs |]
- ==> Says Server B
- {|Nonce NA,
- Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
- Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
+ ==> Says Server A
+ {|Crypt {|Agent B, Key (newK evs),
+ Nonce NA, Nonce NB|} (shrK A),
+ Crypt {|Agent A, Key (newK evs)|} (shrK B)|}
# evs : yahalom"
- (*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.*)
+ (*Alice receives the Server's (?) message, checks her Nonce, and
+ uses the new session key to send Bob his Nonce.*)
YM4 "[| evs: yahalom; A ~= B;
- Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
+ Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+ X|}
: set_of_list evs;
- Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
- : set_of_list evs |]
- ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
-
- (*Alice checks her Nonce, then sends a dummy message to Bob,
- using the new session key.*)
- YM5 "[| evs: yahalom;
- 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, X|} : set_of_list evs |]
- ==> Says A B (Crypt (Agent A) K) # evs : yahalom"
+ Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
+ ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom"
end