LRW: proof for GF multiplication to be e-AXU2

[Fruhwirth Clemens <clemens@xxxxxxxxxxxxx>]

The tweakable cipher mode paper by Liskov, Rivest and Wagner require the
function H, which is used in the C=E(H(T) XOR P) XOR H(T) cipher mode
construction, to be an epsilon-AXU2 function. Formally, the definition
is Pr[h(x) XOR h(y) = z] < epsilon. (See
http://citeseer.ist.psu.edu/liskov02tweakable.html for better
illustrated definition, 3.1, page 7)

LRW-AES obviously uses this construction and implies that the
multiplication under GF(2^128) is of the family of epsilon-AXU2
functions. I have some ideas how to interpret the e-AXU2 requirement and
my intuition takes a good guess that a GF multiplication does fulfill it
(except I think there might be a problem with multiplications involving
zero as one of the operands.)

However, I would like to know, if there is a formal proof available, or
if someone has a sketch how to construct one. 

Thanks,
-- 
Fruhwirth Clemens <clemens@endorphin.org>  http://clemens.endorphin.org

This is a digitally signed message part