Is there any existing analysis for this construction to turn a tweakable blockcipher into a PRF? I'm basically looking at this construction to turn a tweakable blockcipher $E_c(x)$ taking a key $k$, nonce $n$, counter $c$ (forming tweak $t = c||n$) and an input $x$ into a PRF on an arbitrary-length message $M$ that has $m$ blocks. Without further ado:

$$tag = E_0(E_1(M_1) \oplus \dots \oplus E_{m-1}(M_{m-1})  \oplus M_{m} \oplus E_{\ell + |M_m|}(0) \oplus E_{\lambda + |M_m|}(0))$$

$l$ is a constant larger than any legal value for $m$. $\lambda$ is larger than any legal value for $l + |M_m|$. $|M_m|$ is the length of the final block, and the XOR of the last two elements $M_{m} \oplus E_{\ell + |M_m|}(0)$ is truncated to $|M_m|$ bytes. $E_{\lambda + |M_m|}(0)$ is not truncated.

The closest to this construction what I found is the authentication part of OCB3 mode defined in terms of the tweakable blockcipher. How the last block is handled however is quite different.
I don't have a proof myself, but here's how you could analyze this / prove it secure yourself, if you want to have a go.

Your construction is basically $F(M) = E_0(G(M))$, where $G(M) = E_1(M_1) \oplus \dots \oplus E_{\lambda+|M_m|}(0)$ (that long thing defined in the question).  To prove this secure, it suffices to prove the following:


The tweak values used in computing $G(M)$ are never $0$.
It is highly unlikely that the attacker can find a "collision".  In other words, say that two messages $M,M'$ form a "collision" if $G(M)=G(M')$.  Consider an (adaptive) attacker with an oracle for $F$, and let $M^1,\dots,M^q$ denote the $q$ messages that the attacker queries its oracle on.  Let $\mathsf{BAD}$ denote the event that there exists some $i,j$ with $i\ne j$ and $G(M^i)=G(M^j)$.  If you can prove that $\Pr[\mathsf{BAD}]$ is negligible, then you are home-free.  That's because $E_0(Y^1),\dots,E_0(Y^q)$ will be pseudorandom if $Y^1,\dots,Y^q$ are all distinct.


The first condition should be easy to establish, as long as you put appropriate bounds on the length of the message to ensure that $l+|M_m|$ and $\lambda+|M_m|$ never wrap around to become equal to $0$.

You will have to analyze the second condition carefully.  It looks like you might be able to establish that the second condition holds through some sort of case analysis, but that looks too tedious for me to do it -- so I'm going to leave that to you to establish.



Other comments.  I don't understand why you have $E_{l+|M_m|}(0)$ in the xor; that looks pointless to me.  I don't understand why you treat $M_m$ differently (premature optimization?).  I don't understand why you don't just use some existing construction, like PMAC.

If you're going to invent something new, the following seems cleaner and easier to analyze:

$$F(M) = E_0(E_1(M_1) \oplus E_2(M_2) \oplus \cdots \oplus E_m(M_m) \oplus E_\lambda(\text{length}(M))),$$

where $\lambda$ is a constant chosen to be larger than any possible value of $m$, and where $M_m$ is padded with zeros (say) deterministically.



Related work. I suggest you make sure ythat you read the following papers:


http://cseweb.ucsd.edu/~mihir/papers/xormacs.html - Describes a similar but not identical construction, and offers a proof of security.
A Block-Cipher Mode of Operation for Parallelizable Message Authentication - PMAC is also very similar, so make sure you take a look at it.  It's not clear to me why you have invented something new, rather than just using PMAC.  I don't see any advantage of your scheme over PMAC.
Improved Security Analyses for CBC MACs - I recommend you read their proof of security for ECBC.  It is the framework I outlined above (show that the input to a final PRF/PRP is free of collisions across all queries, then it follows that the output is pseudorandom).