src/HOL/Auth/Message.thy
changeset 2484 596a5b5a68ff
parent 2373 490ffa16952e
child 2516 4d68fbe6378b
     1.1 --- a/src/HOL/Auth/Message.thy	Tue Jan 07 12:42:48 1997 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Jan 07 16:28:43 1997 +0100
     1.3 @@ -48,7 +48,12 @@
     1.4    "{|x, y|}"      == "MPair x y"
     1.5  
     1.6  
     1.7 -constdefs  (*Keys useful to decrypt elements of a message set*)
     1.8 +constdefs
     1.9 +  (*Message Y, paired with a MAC computed with the help of X*)
    1.10 +  HPair :: "[msg,msg]=>msg"
    1.11 +    "HPair X Y == {| Hash{|X,Y|}, Y|}"
    1.12 +
    1.13 +  (*Keys useful to decrypt elements of a message set*)
    1.14    keysFor :: msg set => key set
    1.15    "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    1.16