--- a/src/HOL/Auth/Event.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/Event.thy Fri Oct 14 15:48:31 2022 +0100
@@ -280,8 +280,7 @@
Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt)))\<close>
"for proving theorems of the form X \<notin> analz (knows Spy evs) \<longrightarrow> P"
-subsubsection\<open>Useful for case analysis on whether a hash is a spoof or not\<close>
-
+text\<open>Useful for case analysis on whether a hash is a spoof or not\<close>
lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
ML
--- a/src/HOL/Auth/KerberosIV.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Fri Oct 14 15:48:31 2022 +0100
@@ -1574,7 +1574,7 @@
evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1628,7 +1628,7 @@
Key authK \<notin> analz (spies evs);
A \<notin> bad; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1668,7 +1668,7 @@
Key authK \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> Tgs Issues A with
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1698,7 +1698,7 @@
Key servK \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1765,7 +1765,7 @@
Key servK \<notin> analz (spies evs);
B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
--- a/src/HOL/Auth/KerberosV.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/KerberosV.thy Fri Oct 14 15:48:31 2022 +0100
@@ -588,7 +588,7 @@
\<Longrightarrow> \<not> expiredAK Ta evs"
by (metis order_le_less_trans)
-subsection\<open>Reliability: friendly agents send somthing if something else happened\<close>
+subsection\<open>Reliability: friendly agents send something if something else happened\<close>
lemma K3_imp_K2:
"\<lbrakk> Says A Tgs
@@ -1168,7 +1168,8 @@
-subsection\<open>Parties authentication: each party verifies "the identity of
+subsection\<open>Authentication\<close>
+text\<open>Each party verifies "the identity of
another party who generated some data" (quoted from Neuman and Ts'o).\<close>
text\<open>These guarantees don't assess whether two parties agree on
@@ -1243,8 +1244,8 @@
-subsection\<open>Parties' knowledge of session keys.
- An agent knows a session key if he used it to issue a cipher. These
+subsection\<open>Parties' knowledge of session keys\<close>
+text\<open>An agent knows a session key if he used it to issue a cipher. These
guarantees can be interpreted both in terms of key distribution
and of non-injective agreement on the session key.\<close>
@@ -1253,7 +1254,7 @@
evs \<in> kerbV \<rbrakk>
\<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta\<rbrace>)
on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1280,7 +1281,7 @@
Key authK \<notin> analz (spies evs); evs \<in> kerbV \<rbrakk>
\<Longrightarrow> Tgs Issues A with
(Crypt authK \<lbrace>Key servK, Agent B, Number Ts\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1310,7 +1311,7 @@
Key servK \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbV \<rbrakk>
\<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1384,7 +1385,7 @@
Key servK \<notin> analz (spies evs);
B \<noteq> Tgs; A \<notin> bad; B \<notin> bad; evs \<in> kerbV \<rbrakk>
\<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -1434,8 +1435,8 @@
-subsection\<open>
-Novel guarantees, never studied before. Because honest agents always say
+subsection\<open>Novel guarantees, never studied before\<close>
+text\<open> Because honest agents always say
the right timestamp in authenticators, we can prove unicity guarantees based
exactly on timestamps. Classical unicity guarantees are based on nonces.
Of course assuming the agent to be different from the Spy, rather than not in
--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Oct 14 15:48:31 2022 +0100
@@ -666,7 +666,7 @@
Key K \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk>
\<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -697,7 +697,7 @@
Key K \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk>
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
--- a/src/HOL/Auth/Message.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/Message.thy Fri Oct 14 15:48:31 2022 +0100
@@ -65,7 +65,7 @@
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
-subsubsection\<open>Inductive Definition of All Parts" of a Message\<close>
+subsection\<open>Inductive Definition of All Parts of a Message\<close>
inductive_set
parts :: "msg set \<Rightarrow> msg set"
@@ -96,13 +96,13 @@
by auto
-subsubsection\<open>Inverse of keys\<close>
+subsection\<open>Inverse of keys\<close>
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
by (metis invKey)
-subsection\<open>keysFor operator\<close>
+subsection\<open>The @{term keysFor} operator\<close>
lemma keysFor_empty [simp]: "keysFor {} = {}"
unfolding keysFor_def by blast
--- a/src/HOL/Auth/NS_Public.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/NS_Public.thy Fri Oct 14 15:48:31 2022 +0100
@@ -1,9 +1,9 @@
-(* Title: HOL/Auth/NS_PublicX.thy
+(* Title: HOL/Auth/NS_Public.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
-section\<open>Verifying the Needham-Schroeder Public-Key Protocol\<close>
+section\<open>The Needham-Schroeder Public-Key Protocol\<close>
text \<open>Flawed version, vulnerable to Lowe's attack.
From Burrows, Abadi and Needham. A Logic of Authentication.
--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Oct 14 15:48:31 2022 +0100
@@ -3,7 +3,7 @@
Copyright 1996 University of Cambridge
*)
-section\<open>Verifying the Needham-Schroeder Public-Key Protocol\<close>
+section\<open>The Needham-Schroeder Public-Key Protocol (Flawed)\<close>
text \<open>Flawed version, vulnerable to Lowe's attack.
From Burrows, Abadi and Needham. A Logic of Authentication.
--- a/src/HOL/Auth/NS_Shared.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/NS_Shared.thy Fri Oct 14 15:48:31 2022 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/Auth/NS_Shared.thy
- Author: Lawrence C Paulson and Giampaolo Bella
+ Author: Lawrence C Paulson and Giampaolo Bella
Copyright 1996 University of Cambridge
*)
-section\<open>Needham-Schroeder Shared-Key Protocol and the Issues Property\<close>
+section\<open>Needham-Schroeder Shared-Key Protocol\<close>
theory NS_Shared imports Public begin
@@ -231,7 +231,7 @@
apply (drule_tac [8] Says_Server_message_form)
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
txt\<open>NS2, NS3\<close>
-apply blast+
+apply blast+
done
@@ -429,7 +429,7 @@
Key K \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
\<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
@@ -489,7 +489,7 @@
Key K \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs"
-apply (simp (no_asm) add: Issues_def)
+unfolding Issues_def
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
--- a/src/HOL/Auth/OtwayRees.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Fri Oct 14 15:48:31 2022 +0100
@@ -15,27 +15,18 @@
inductive_set otway :: "event list set"
where
- (*Initial trace is empty*)
Nil: "[] \<in> otway"
-
- (*The spy MAY say anything he CAN say. We do not expect him to
- invent new nonces here, but he can also use NS1. Common to
- all similar protocols.*)
+ \<comment> \<open>Initial trace is empty\<close>
| Fake: "\<lbrakk>evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) \<rbrakk>
\<Longrightarrow> Says Spy B X # evsf \<in> otway"
-
- (*A message that has been sent can be received by the
- intended recipient.*)
- | Reception: "\<lbrakk>evsr \<in> otway; Says A B X \<in>set evsr\<rbrakk>
- \<Longrightarrow> Gets B X # evsr \<in> otway"
-
- (*Alice initiates a protocol run*)
+ \<comment> \<open>The spy can say almost anything.\<close>
+ | Reception: "\<lbrakk>evsr \<in> otway; Says A B X \<in>set evsr\<rbrakk> \<Longrightarrow> Gets B X # evsr \<in> otway"
+ \<comment> \<open>A message that has been sent can be received by the intended recipient.\<close>
| OR1: "\<lbrakk>evs1 \<in> otway; Nonce NA \<notin> used evs1\<rbrakk>
\<Longrightarrow> Says A B \<lbrace>Nonce NA, Agent A, Agent B,
Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace>
# evs1 \<in> otway"
-
- (*Bob's response to Alice's message. Note that NB is encrypted.*)
+ \<comment> \<open>Alice initiates a protocol run\<close>
| OR2: "\<lbrakk>evs2 \<in> otway; Nonce NB \<notin> used evs2;
Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> \<in> set evs2\<rbrakk>
\<Longrightarrow> Says B Server
@@ -43,10 +34,7 @@
Crypt (shrK B)
\<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace>
# evs2 \<in> otway"
-
- (*The Server receives Bob's message and checks that the three NAs
- match. Then he sends a new session key to Bob with a packet for
- forwarding to Alice.*)
+ \<comment> \<open>Bob's response to Alice's message. Note that NB is encrypted.\<close>
| OR3: "\<lbrakk>evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server
\<lbrace>Nonce NA, Agent A, Agent B,
@@ -58,10 +46,8 @@
Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>,
Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace>
# evs3 \<in> otway"
-
- (*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.
- Need B \<noteq> Server because we allow messages to self.*)
+ \<comment> \<open>The Server receives Bob's message and checks that the three NAs
+ match. Then he sends a new session key to Bob with a packet for forwarding to Alice\<close>
| OR4: "\<lbrakk>evs4 \<in> otway; B \<noteq> Server;
Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
@@ -70,14 +56,14 @@
Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
\<in> set evs4\<rbrakk>
\<Longrightarrow> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway"
-
- (*This message models possible leaks of session keys. The nonces
- identify the protocol run.*)
+ \<comment> \<open>Bob receives the Server's (?) message and compares the Nonces with
+ those in the message he previously sent the Server.
+ Need @{term"B \<noteq> Server"} because we allow messages to self.\<close>
| Oops: "\<lbrakk>evso \<in> otway;
Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace>
\<in> set evso\<rbrakk>
\<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway"
-
+ \<comment> \<open>This message models possible leaks of session keys. The nonces identify the protocol run\<close>
declare Says_imp_analz_Spy [dest]
declare parts.Body [dest]
@@ -110,12 +96,12 @@
lemma OR2_analz_knows_Spy:
"\<lbrakk>Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk>
\<Longrightarrow> X \<in> analz (knows Spy evs)"
-by blast
+ by blast
lemma OR4_analz_knows_Spy:
"\<lbrakk>Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk>
\<Longrightarrow> X \<in> analz (knows Spy evs)"
-by blast
+ by blast
(*These lemmas assist simplification by removing forwarded X-variables.
We can replace them by rewriting with parts_insert2 and proving using
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Fri Oct 14 15:48:31 2022 +0100
@@ -267,7 +267,7 @@
nonces.
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
-apply (simp (no_asm) add: used_Nil)
+unfolding used_Nil
done
So, we must use old-style supply fresh nonce theorems relying on the appropriate axiom*)