--- a/src/HOL/Auth/OtwayRees.thy Thu Sep 15 17:16:54 2005 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Sep 15 17:16:55 2005 +0200
@@ -238,7 +238,7 @@
text{*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
- over-simplified version of this protocol: see OtwayRees_Bad.*}
+ over-simplified version of this protocol: see @{text OtwayRees_Bad}.*}
lemma no_nonce_OR1_OR2:
"[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> otway |]
@@ -270,7 +270,7 @@
text{*Corollary: 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
bad form of this protocol, even though we can prove
- Spy_not_see_encrypted_key*}
+ @{text Spy_not_see_encrypted_key} *}
lemma A_trusts_OR4:
"[| Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
--- a/src/HOL/Auth/Yahalom.thy Thu Sep 15 17:16:54 2005 +0200
+++ b/src/HOL/Auth/Yahalom.thy Thu Sep 15 17:16:55 2005 +0200
@@ -297,10 +297,12 @@
apply blast+
done
-text{*B knows, by the second part of A's message, that the Server distributed
- the key quoting nonce NB. This part says nothing about agent names.
- Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must
- be the FIRST antecedent of the induction formula.*}
+text{*B knows, by the second part of A's message, that the Server
+ distributed the key quoting nonce NB. This part says nothing about
+ agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB
+ \<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the
+ induction formula.*}
+
lemma B_trusts_YM4_newK [rule_format]:
"[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
@@ -392,9 +394,10 @@
analz_image_freshK fresh_not_KeyWithNonce
imp_disj_not1 (*Moves NBa\<noteq>NB to the front*)
Says_Server_KeyWithNonce)
-txt{*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce,
- we get (~ KeyWithNonce K NB evs); then simplification can apply the
- induction hypothesis with KK = {K}.*}
+txt{*For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By
+ @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
+ evs"}; then simplification can apply the induction hypothesis with
+ @{term "KK = {K}"}.*}
txt{*Fake*}
apply spy_analz
txt{*YM2*}
@@ -403,8 +406,9 @@
apply blast
txt{*YM4*}
apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
-txt{*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps
- make the next step faster.*}
+txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
+ @{prop "NBa \<noteq> NB"}. Previous two steps make the next step
+ faster.*}
apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
dest: analz.Inj
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
@@ -501,7 +505,7 @@
apply (clarify, simp add: all_conj_distrib)
txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*}
txt{*Case analysis on Aa:bad; PROOF FAILED problems
- use Says_unique_NB to identify message components: Aa=A, Ba=B*}
+ use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*}
apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
@@ -513,7 +517,7 @@
apply (case_tac "NB = NBa")
txt{*If NB=NBa then all other components of the Oops message agree*}
apply (blast dest: Says_unique_NB)
-txt{*case NB \<noteq> NBa*}
+txt{*case @{prop "NB \<noteq> NBa"}*}
apply (simp add: single_Nonce_secrecy)
apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
done
@@ -521,7 +525,7 @@
text{*B's session key guarantee from YM4. The two certificates contribute to a
single conclusion about the Server's message. Note that the "Notes Spy"
- assumption must quantify over \<forall>POSSIBLE keys instead of our particular K.
+ assumption must quantify over @{text \<forall>} POSSIBLE keys instead of our particular K.
If this run is broken and the spy substitutes a certificate containing an
old key, B has no means of telling.*}
lemma B_trusts_YM4: