--- a/src/HOL/Auth/Recur.thy Wed Apr 23 18:09:48 2003 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Apr 25 11:18:14 2003 +0200
@@ -8,7 +8,7 @@
theory Recur = Shared:
-(*End marker for message bundles*)
+text{*End marker for message bundles*}
syntax END :: "msg"
translations "END" == "Number 0"
@@ -116,17 +116,17 @@
**)
-(*Simplest case: Alice goes directly to the server*)
+text{*Simplest case: Alice goes directly to the server*}
lemma "\<exists>K NA. \<exists>evs \<in> recur.
Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|},
END|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] recur.Nil [THEN recur.RA1,
- THEN recur.RA3 [OF _ _ respond.One]], possibility)
+ THEN recur.RA3 [OF _ _ respond.One]], possibility)
done
-(*Case two: Alice, Bob and the server*)
+text{*Case two: Alice, Bob and the server*}
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
@@ -174,7 +174,7 @@
apply (auto dest: Key_not_used respond_imp_not_used)
done
-(*Simple inductive reasoning about responses*)
+text{*Simple inductive reasoning about responses*}
lemma respond_imp_responses:
"(PA,RB,KAB) \<in> respond evs ==> RB \<in> responses evs"
apply (erule respond.induct)
@@ -208,7 +208,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
apply (erule recur.induct, auto)
-(*RA3. It's ugly to call auto twice, but it seems necessary.*)
+txt{*RA3. It's ugly to call auto twice, but it seems necessary.*}
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
done
@@ -241,7 +241,7 @@
add: analz_image_freshK_simps)
-(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
+text{*Version for the protocol. Proof is almost trivial, thanks to the lemma.*}
lemma raw_analz_image_freshK:
"evs \<in> recur ==>
\<forall>K KK. KK \<subseteq> - (range shrK) -->
@@ -251,7 +251,7 @@
apply (drule_tac [4] RA2_analz_spies,
drule_tac [5] respond_imp_responses,
drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
-(*RA3*)
+txt{*RA3*}
apply (simp_all add: resp_analz_image_freshK_lemma)
done
@@ -273,7 +273,7 @@
add: analz_image_freshK_simps raw_analz_image_freshK)
-(*Everything that's hashed is already in past traffic. *)
+text{*Everything that's hashed is already in past traffic. *}
lemma Hash_imp_body:
"[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
evs \<in> recur; A \<notin> bad |] ==> X \<in> parts (spies evs)"
@@ -282,11 +282,9 @@
drule_tac [6] RA4_parts_spies,
drule_tac [5] respond_imp_responses,
drule_tac [4] RA2_parts_spies)
-(*RA3 requires a further induction*)
+txt{*RA3 requires a further induction*}
apply (erule_tac [5] responses.induct, simp_all)
-(*Nil*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply (blast intro: parts_insertI)
done
@@ -306,10 +304,10 @@
apply (erule recur.induct,
drule_tac [5] respond_imp_responses)
apply (force, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
apply (erule_tac [3] responses.induct)
-(*RA1,2: creation of new Nonce*)
+txt{*RA1,2: creation of new Nonce*}
apply simp_all
apply (blast dest!: Hash_imp_body)+
done
@@ -337,14 +335,14 @@
apply (erule rev_mp, erule responses.induct)
apply (simp_all del: image_insert
add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
-(*Simplification using two distinct treatments of "image"*)
+txt{*Simplification using two distinct treatments of "image"*}
apply (simp add: parts_insert2, blast)
done
lemmas resp_analz_insert =
resp_analz_insert_lemma [OF _ raw_analz_image_freshK]
-(*The last key returned by respond indeed appears in a certificate*)
+text{*The last key returned by respond indeed appears in a certificate*}
lemma respond_certificate:
"(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
@@ -390,13 +388,11 @@
apply (simp_all del: image_insert
add: analz_image_freshK_simps split_ifs shrK_in_analz_respond
resp_analz_image_freshK parts_insert2)
-apply (simp_all add: ex_disj_distrib)
-(** LEVEL 5 **)
-(*Base case of respond*)
+txt{*Base case of respond*}
apply blast
-(*Inductive step of respond*)
+txt{*Inductive step of respond*}
apply (intro allI conjI impI, simp_all)
-(*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
+txt{*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*}
apply (blast dest: unique_session_keys [OF _ respond_certificate])
apply (blast dest!: respond_certificate)
apply (blast dest!: resp_analz_insert)
@@ -413,28 +409,26 @@
frule_tac [5] respond_imp_responses,
drule_tac [6] RA4_analz_spies,
simp_all add: split_ifs analz_insert_eq analz_insert_freshK)
-(*Base*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*RA2*)
+txt{*RA2*}
apply blast
-(*RA3 remains*)
+txt{*RA3 remains*}
apply (simp add: parts_insert_spies)
-(*Now we split into two cases. A single blast could do it, but it would take
- a CPU minute.*)
+txt{*Now we split into two cases. A single blast could do it, but it would take
+ a CPU minute.*}
apply (safe del: impCE)
-(*RA3, case 1: use lemma previously proved by induction*)
+txt{*RA3, case 1: use lemma previously proved by induction*}
apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key])
-(*RA3, case 2: K is an old key*)
+txt{*RA3, case 2: K is an old key*}
apply (blast dest: resp_analz_insert dest: Key_in_parts_respond)
-(*RA4*)
+txt{*RA4*}
apply blast
done
(**** Authenticity properties for Agents ****)
-(*The response never contains Hashes*)
+text{*The response never contains Hashes*}
lemma Hash_in_parts_respond:
"[| Hash {|Key (shrK B), M|} \<in> parts (insert RB H);
(PB,RB,K) \<in> respond evs |]
@@ -443,10 +437,10 @@
apply (erule respond_imp_responses [THEN responses.induct], auto)
done
-(*Only RA1 or RA2 can have caused such a part of a message to appear.
+text{*Only RA1 or RA2 can have caused such a part of a message to appear.
This result is of no use to B, who cannot verify the Hash. Moreover,
it can say nothing about how recent A's message is. It might later be
- used to prove B's presence to A at the run's conclusion.*)
+ used to prove B's presence to A at the run's conclusion.*}
lemma Hash_auth_sender [rule_format]:
"[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \<in> parts(spies evs);
A \<notin> bad; evs \<in> recur |]
@@ -457,9 +451,9 @@
drule_tac [6] RA4_parts_spies,
drule_tac [4] RA2_parts_spies,
simp_all)
-(*Nil*)
+txt{*Nil*}
apply force
-(*Fake, RA3*)
+txt{*Fake, RA3*}
apply (blast dest: Hash_in_parts_respond)+
done
@@ -468,25 +462,23 @@
**)
-(*Certificates can only originate with the Server.*)
+text{*Certificates can only originate with the Server.*}
lemma Cert_imp_Server_msg:
"[| Crypt (shrK A) Y \<in> parts (spies evs);
A \<notin> bad; evs \<in> recur |]
==> \<exists>C RC. Says Server C RC \<in> set evs &
Crypt (shrK A) Y \<in> parts {RC}"
apply (erule rev_mp, erule recur.induct, simp_all)
-(*Nil*)
-apply force
-(*Fake*)
+txt{*Fake*}
apply blast
-(*RA1*)
+txt{*RA1*}
apply blast
-(*RA2: it cannot be a new Nonce, contradiction.*)
+txt{*RA2: it cannot be a new Nonce, contradiction.*}
apply blast
-(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
- which however would break all other steps.*)
+txt{*RA3. Pity that the proof is so brittle: this step requires the rewriting,
+ which however would break all other steps.*}
apply (simp add: parts_insert_spies, blast)
-(*RA4*)
+txt{*RA4*}
apply blast
done