The Coq mailing list

[Andrew Appel <appel AT CS.Princeton.EDU>]

Dear Bas:

Indeed, it is a kind of hijacking, since I doubt this will be of general interest to the coq-club.

As stated in the paper (page 3):

What we mechanized is the classic Bellare/Canetti/Krawczyk 1996 security proof for HMAC,

using some ideas from the Bellare 2006 security proof for HMAC.

The formal statement of this security result is given as Theorem HMAC_PRF on page 8.

The "HMAC brawl" is an argument in the crypto community about how to account

for precomputation by the adversary, as explained in the two references we cite, [19] and [33].

No one claims that Bellare et al. have a buggy proof; only that the theorem

they stated is less useful than they claim.  We claim that our proof is not buggy (the

Coq kernel agrees with us), but I will not make a claim about its cryptographic utility

(and neither does the Coq kernel).  In the future, if the cryptographers state and prove

another theorem, I expect we will be able to mechanize that in Coq.  That mechanization

will be *modular*---independent of the verification that the C program satisfies its

functional spec---as stated in the last sentence of the "HMAC brawl" paragraph on page 3.

Sincerely,

Andrew Appel

From: "Bas Spitters" <b.a.w.spitters AT gmail.com>
To: "Coq Club" <coq-club AT inria.fr>
Sent: Monday, January 4, 2016 4:43:34 PM
Subject: Re: [Coq-Club] VST release 1.6

Sorry to hijack this thread a little. Since you are mentioning your
very nice paper on OpenSLL, could you comment a bit more on the "HMAC
brawl". As you indicate in sec 3 there is some discussion about
precisely what the security model is, and hence what has been
verified.

Thanks,

Bas