--- a/src/HOL/Auth/Recur.ML Tue Jan 07 10:18:20 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Tue Jan 07 10:19:43 1997 +0100
@@ -19,7 +19,7 @@
**)
(*Simplest case: Alice goes directly to the server*)
-goal thy
+goal thy
"!!A. A ~= Server \
\ ==> EX K NA. EX evs: recur lost. \
\ Says Server A {|Agent A, \
@@ -29,13 +29,15 @@
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
(respond.One RSN (4,recur.RA3))) 2);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
-by (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI]));
+by (REPEAT
+ (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
+ THEN
+ REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
result();
(*Case two: Alice, Bob and the server*)
-goal thy
+goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
@@ -45,6 +47,7 @@
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
(respond.One RS respond.Cons RSN (4,recur.RA3)) RS
recur.RA4) 2);
+bw HPair_def;
by (REPEAT
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
THEN
@@ -53,7 +56,7 @@
(*Case three: Alice, Bob, Charlie and the server*)
-goal thy
+goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
@@ -63,6 +66,7 @@
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
(respond.One RS respond.Cons RS respond.Cons RSN
(4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+bw HPair_def;
by (REPEAT (*SLOW: 37 seconds*)
(REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
THEN
@@ -313,6 +317,8 @@
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
+Delsimps [image_insert];
+
(** Session keys are not used to encrypt other session keys **)
(*Version for "responses" relation. Handles case RA3 in the theorem below.
@@ -339,8 +345,8 @@
\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
\ (K : newK``I | Key K : analz (sees lost Spy evs))";
by (etac recur.induct 1);
+be subst 4; (*RA2: DELETE needless definition of PA!*)
by analz_Fake_tac;
-be ssubst 4; (*RA2: DELETE needless definition of PA!*)
by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
(*Base*)
@@ -381,7 +387,7 @@
\ (Nonce (newN i) : parts {X} --> \
\ Hash X ~: parts (sees lost Spy evs))";
be recur.induct 1;
-be ssubst 4; (*RA2: DELETE needless definition of PA!*)
+be subst 4; (*RA2: DELETE needless definition of PA!*)
by parts_Fake_tac;
(*RA3 requires a further induction*)
be responses.induct 5;
@@ -416,7 +422,7 @@
\ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs) --> B=B' & P=P'";
be recur.induct 1;
-be ssubst 4; (*RA2: DELETE needless definition of PA!*)
+be subst 4; (*RA2: DELETE needless definition of PA!*)
(*For better simplification of RA2*)
by (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 4);
by parts_Fake_tac;
@@ -431,9 +437,8 @@
addDs [impOfSubs analz_subset_parts,
impOfSubs Fake_parts_insert]
addss (!simpset)) 2);
-(*Base*)
+(*Base*) (** LEVEL 9 **)
by (fast_tac (!claset addss (!simpset)) 1);
-
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
(*RA1: creation of new Nonce. Move assertion into global context*)
by (expand_case_tac "NA = ?y" 1);
@@ -450,13 +455,14 @@
by (best_tac (!claset addss (!simpset)) 1);
val lemma = result();
-goal thy
- "!!evs.[| Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
+goalw thy [HPair_def]
+ "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs); \
-\ Hash {|Key(shrK A), Agent A, Agent B', Nonce NA, P'|} \
+\ HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
\ : parts (sees lost Spy evs); \
\ evs : recur lost; A ~: lost |] \
\ ==> B=B' & P=P'";
+by (REPEAT (eresolve_tac partsEs 1));
by (prove_unique_tac lemma 1);
qed "unique_NA";
@@ -465,17 +471,6 @@
(relations "respond" and "responses")
***)
-(*The response never contains Hashes*)
-(*NEEDED????????????????*)
-goal thy
- "!!evs. (j,PB,RB) : respond i \
-\ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
-\ Hash {|Key (shrK B), M|} : parts H";
-be (respond_imp_responses RS responses.induct) 1;
-by (Auto_tac());
-bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
-
-
goal thy
"!!evs. [| RB : responses i; evs : recur lost |] \
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
@@ -556,7 +551,7 @@
\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
\ (j,PB,RB) : respond i |] \
\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1); (*33 seconds, due to the disjunctions*)
+by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
qed "unique_session_keys";
@@ -565,7 +560,7 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!j. (j, {|Hash {|Key(shrK A), Agent A, B, NA, P|}, X|}, RA) : respond i \
+ "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
be respond.elim 1;
by (ALLGOALS Asm_full_simp_tac);
@@ -579,7 +574,7 @@
\ Key K ~: analz (insert RB (sees lost Spy evs))";
be respond.induct 1;
by (forward_tac [respond_imp_responses] 2);
-by (ALLGOALS
+by (ALLGOALS (*4 MINUTES???*)
(asm_simp_tac
(!simpset addsimps
([analz_image_newK, not_parts_not_analz,
@@ -615,8 +610,8 @@
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
\ Key K ~: analz (sees lost Spy evs)";
by (etac recur.induct 1);
+be subst 4; (*RA2: DELETE needless definition of PA!*)
by analz_Fake_tac;
-be ssubst 4; (*RA2: DELETE needless definition of PA!*)
by (ALLGOALS
(asm_simp_tac
(!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
@@ -654,14 +649,23 @@
(**** Authenticity properties for Agents ****)
+(*The response never contains Hashes*)
+(*NEEDED????????????????*)
+goal thy
+ "!!evs. (j,PB,RB) : respond i \
+\ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
+\ Hash {|Key (shrK B), M|} : parts H";
+be (respond_imp_responses RS responses.induct) 1;
+by (Auto_tac());
+bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
+
(*NEEDED????????????????*)
(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
-goal thy
+goalw thy [HPair_def]
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : recur lost |] \
-\ ==> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \
-\ Agent A, Agent B, NA, P|} \
+\ ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|}) \
\ : set_of_list evs";
be rev_mp 1;
by (parts_induct_tac 1);
@@ -676,14 +680,6 @@
qed_spec_mp "Hash_auth_sender";
-(*NEEDED????????????????*)
-goal thy "!!i. {|Hash {|Key (shrK Server), M|}, M|} : responses i ==> R";
-be setup_induction 1;
-be responses.induct 1;
-by (ALLGOALS Asm_simp_tac);
-qed "responses_no_Hash_Server";
-
-
val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
--- a/src/HOL/Auth/Recur.thy Tue Jan 07 10:18:20 1997 +0100
+++ b/src/HOL/Auth/Recur.thy Tue Jan 07 10:19:43 1997 +0100
@@ -6,7 +6,7 @@
Inductive relation "recur" for the Recursive Authentication protocol.
*)
-Recur = Shared +
+Recur = HPair + Shared +
syntax
newK2 :: "nat*nat => key"
@@ -23,9 +23,9 @@
intrs
(*The message "Agent Server" marks the end of a list.*)
- One "[| A ~= Server;
- MA = {|Agent A, Agent B, Nonce NA, Agent Server|} |]
- ==> (j, {|Hash{|Key(shrK A), MA|}, MA|},
+ One "A ~= Server
+ ==> (j, HPair (Key(shrK A))
+ {|Agent A, Agent B, Nonce NA, Agent Server|},
{|Agent A,
Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|},
Agent Server|})
@@ -33,11 +33,9 @@
(*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
Cons "[| (Suc j, PA, RA) : respond i;
- B ~= Server;
- MB = {|Agent B, Agent C, Nonce NB, PA|};
- PA = {|Hash{|Key(shrK A), MA|}, MA|};
- MA = {|Agent A, Agent B, Nonce NA, P|} |]
- ==> (j, {|Hash{|Key(shrK B), MB|}, MB|},
+ PA = HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|};
+ B ~= Server |]
+ ==> (j, HPair (Key(shrK B)) {|Agent B, Agent C, Nonce NB, PA|},
{|Agent B,
Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
Agent B,
@@ -46,7 +44,7 @@
: respond i"
-(*Induction over "respond" can be difficult, due to the complexity of the
+(*Induction over "respond" can be difficult due to the complexity of the
subgoals. The "responses" relation formalizes the general form of its
third component.
*)
@@ -77,9 +75,11 @@
(*Alice initiates a protocol run.
"Agent Server" is just a placeholder, to terminate the nesting.*)
- RA1 "[| evs: recur lost; A ~= B; A ~= Server;
- MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
- ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
+ RA1 "[| evs: recur lost; A ~= B; A ~= Server |]
+ ==> Says A B
+ (HPair (Key(shrK A))
+ {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|})
+ # evs : recur lost"
(*Bob's response to Alice's message. C might be the Server.
XA should be the Hash of the remaining components with KA, but
@@ -87,9 +87,11 @@
P is the previous recur message from Alice's caller.*)
RA2 "[| evs: recur lost; B ~= C; B ~= Server;
Says A' B PA : set_of_list evs;
- PA = {|XA, Agent A, Agent B, Nonce NA, P|};
- MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
- ==> Says B C {|Hash{|Key(shrK B),MB|}, MB|} # evs : recur lost"
+ PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
+ ==> Says B C
+ (HPair (Key(shrK B))
+ {|Agent B, Agent C, Nonce (newN(length evs)), PA|})
+ # evs : recur lost"
(*The Server receives and decodes Bob's message. Then he generates
a new session key and a response.*)