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/Message.thy
changeset 2484 596a5b5a68ff
parent 2373 490ffa16952e
child 2516 4d68fbe6378b 
--- a/src/HOL/Auth/Message.thy	Tue Jan 07 12:42:48 1997 +0100
+++ b/src/HOL/Auth/Message.thy	Tue Jan 07 16:28:43 1997 +0100
@@ -48,7 +48,12 @@
   "{|x, y|}"      == "MPair x y"
 
 
-constdefs  (*Keys useful to decrypt elements of a message set*)
+constdefs
+  (*Message Y, paired with a MAC computed with the help of X*)
+  HPair :: "[msg,msg]=>msg"
+    "HPair X Y == {| Hash{|X,Y|}, Y|}"
+
+  (*Keys useful to decrypt elements of a message set*)
   keysFor :: msg set => key set
   "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
isabelle