Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Guard/Guard_Yahalom.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 23746 a455e69c31cc 
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -16,31 +16,38 @@
 subsection{*messages used in the protocol*}
 
 abbreviation (input)
-  ya1 :: "agent => agent => nat => event"
+  ya1 :: "agent => agent => nat => event" where
   "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
 
-  ya1' :: "agent => agent => agent => nat => event"
+abbreviation (input)
+  ya1' :: "agent => agent => agent => nat => event" where
   "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
 
-  ya2 :: "agent => agent => nat => nat => event"
+abbreviation (input)
+  ya2 :: "agent => agent => nat => nat => event" where
   "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
 
-  ya2' :: "agent => agent => agent => nat => nat => event"
+abbreviation (input)
+  ya2' :: "agent => agent => agent => nat => nat => event" where
   "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
 
-  ya3 :: "agent => agent => nat => nat => key => event"
+abbreviation (input)
+  ya3 :: "agent => agent => nat => nat => key => event" where
   "ya3 A B NA NB K ==
     Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
                     Ciph B {|Agent A, Key K|}|}"
 
-  ya3':: "agent => msg => agent => agent => nat => nat => key => event"
+abbreviation (input)
+  ya3':: "agent => msg => agent => agent => nat => nat => key => event" where
   "ya3' S Y A B NA NB K ==
     Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
 
-  ya4 :: "agent => agent => nat => nat => msg => event"
+abbreviation (input)
+  ya4 :: "agent => agent => nat => nat => msg => event" where
   "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
 
-  ya4' :: "agent => agent => nat => nat => msg => event"
+abbreviation (input)
+  ya4' :: "agent => agent => nat => nat => msg => event" where
   "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
isabelle