src/HOL/Auth/Message.thy

 
 type_synonym
   key = nat
 
 consts
-  all_symmetric :: bool        \<comment>\<open>true if all keys are symmetric\<close>
-  invKey        :: "key=>key"  \<comment>\<open>inverse of a symmetric key\<close>
+  all_symmetric :: bool        \<comment> \<open>true if all keys are symmetric\<close>
+  invKey        :: "key=>key"  \<comment> \<open>inverse of a symmetric key\<close>
 
 specification (invKey)
   invKey [simp]: "invKey (invKey K) = K"
   invKey_symmetric: "all_symmetric --> invKey = id"
     by (rule exI [of _ id], auto)

       is the private key and vice versa\<close>
 
 definition symKeys :: "key set" where
   "symKeys == {K. invKey K = K}"
 
-datatype  \<comment>\<open>We allow any number of friendly agents\<close>
+datatype  \<comment> \<open>We allow any number of friendly agents\<close>
   agent = Server | Friend nat | Spy
 
 datatype
-     msg = Agent  agent     \<comment>\<open>Agent names\<close>
-         | Number nat       \<comment>\<open>Ordinary integers, timestamps, ...\<close>
-         | Nonce  nat       \<comment>\<open>Unguessable nonces\<close>
-         | Key    key       \<comment>\<open>Crypto keys\<close>
-         | Hash   msg       \<comment>\<open>Hashing\<close>
-         | MPair  msg msg   \<comment>\<open>Compound messages\<close>
-         | Crypt  key msg   \<comment>\<open>Encryption, public- or shared-key\<close>
+     msg = Agent  agent     \<comment> \<open>Agent names\<close>
+         | Number nat       \<comment> \<open>Ordinary integers, timestamps, ...\<close>
+         | Nonce  nat       \<comment> \<open>Unguessable nonces\<close>
+         | Key    key       \<comment> \<open>Crypto keys\<close>
+         | Hash   msg       \<comment> \<open>Hashing\<close>
+         | MPair  msg msg   \<comment> \<open>Compound messages\<close>
+         | Crypt  key msg   \<comment> \<open>Encryption, public- or shared-key\<close>
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
 syntax
   "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")

   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) where
-    \<comment>\<open>Message Y paired with a MAC computed with the help of X\<close>
+    \<comment> \<open>Message Y paired with a MAC computed with the help of X\<close>
     "Hash[X] Y == \<lbrace>Hash\<lbrace>X,Y\<rbrace>, Y\<rbrace>"
 
 definition keysFor :: "msg set => key set" where
-    \<comment>\<open>Keys useful to decrypt elements of a message set\<close>
+    \<comment> \<open>Keys useful to decrypt elements of a message set\<close>
   "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
 
 
 subsubsection\<open>Inductive Definition of All Parts" of a Message\<close>
 

   case (Nonce n)
     show ?case
       by simp (metis Suc_n_not_le_n)
 next
   case (MPair X Y)
-    then show ?case \<comment>\<open>metis works out the necessary sum itself!\<close>
+    then show ?case \<comment> \<open>metis works out the necessary sum itself!\<close>
       by (simp add: parts_insert2) (metis le_trans nat_le_linear)
 qed auto
 
 subsection\<open>Inductive relation "analz"\<close>