Due: Wed, 25 May 2016 23:00:00 -0700
Read Verified Correctness and Security of OpenSSL HMAC, USENIX Security 2015.
Take a look at the git repo, especially
the directories fcf, hmacfcf, and sha.
What is their TCB? Please describe in your own words (don’t just copy-paste from the list in the paper).
Given their TCB, what do they prove about their HMAC function?
What do you think was the most exciting contribution of this paper? This can be one or more of the items from Figure 1, or something more general.
Provide a list of questions you would like to discuss.