Due: Wed, 01 Jun 2016 23:00:00 -0700
Read Implementing TLS with Verified Cryptographic Security, Oakland 2013.
Take a look at the source code.
How does this paper formally define secrecy?
How does the TCB of miTLS compare to the TCB of the HMAC implementation?
How do the guarantees made by miTLS compare to the guarantees made by the HMAC implementation?
Provide a list of questions you would like to discuss.