src/HOL/Auth/Message.thy
changeset 2484 596a5b5a68ff
parent 2373 490ffa16952e
child 2516 4d68fbe6378b
equal deleted inserted replaced
2483:95c2f9c0930a 2484:596a5b5a68ff
    46 translations
    46 translations
    47   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    47   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    48   "{|x, y|}"      == "MPair x y"
    48   "{|x, y|}"      == "MPair x y"
    49 
    49 
    50 
    50 
    51 constdefs  (*Keys useful to decrypt elements of a message set*)
    51 constdefs
       
    52   (*Message Y, paired with a MAC computed with the help of X*)
       
    53   HPair :: "[msg,msg]=>msg"
       
    54     "HPair X Y == {| Hash{|X,Y|}, Y|}"
       
    55 
       
    56   (*Keys useful to decrypt elements of a message set*)
    52   keysFor :: msg set => key set
    57   keysFor :: msg set => key set
    53   "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    58   "keysFor H == invKey `` {K. EX X. Crypt K X : H}"
    54 
    59 
    55 (** Inductive definition of all "parts" of a message.  **)
    60 (** Inductive definition of all "parts" of a message.  **)
    56 
    61