Is 16-byte Poly1305 more secure than 16-byte HMAC-SHA1? (Actually curious. Citation: I've done all the matasano crypto challenges, and all of the stripe µctf stuff :).)
I believe so? Isn't there a 2^80 attack on SHA1? I think the bigger issue is that the security proof for a polynomial MAC is much clearer (and the MAC itself is much faster).
On average a bruteforce attack will find a match halfway through the keyspace, so that would be 2^80 for SHA1... and only 2^64 for Poly1305 and anything else with a 128-bit width (that isn't broken in some other manner.)
Halfway through the tag space of a 160-bit tag is 2^159. You're looking for an exact match, not just a collision.
The collision attack on SHA-1 should not threaten HMAC-SHA1. Even HMAC-MD5 hasn't been successfully attacked yet, AFAIK.
Poly1305 is arguably less misuse-resistant, since it requires a nonce.
That's typical of AEAD modes in general, though. GCM also requires a nonce.
Do you have a decent reference for the proof of poly MACs?
You can start at the Poly1305 paper and follow the cites all the way back to Wegman and Carter, or (somewhat more modern) to Krawczyk's "cryptographic CRCs". Or, if I may be permitted to once again coattail 'pbsd, start the other way: