4 ms·
Here's the full paper: http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf
by hypotext 11y ago
Here's the full paper: http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf
- nickpsecurity 11y agoThanks. My favorite part is your thorough breakdown of the assurance case in section one. For redoing security evaluations, I recommended [1] a while back that vendors illustrate the assurance levels of each component in their systems. Your breakdown looks closer to my recommendation than most things I've seen. Such a breakdown is both honest and shows exactly where improvements (or mitigations) need to happen. Otherwise, verifications were as practical and good as I'd expect. My favorite section to scope out, Related Work, gave me new insights as usual. You also had a useful idea of future work [2]. All together, great work. [1] https://www.schneier.com/blog/archives/2014/04/friday_squid_bl_419.html#c5457853 https://www.schneier.com/blog/archives/2014/04/friday_squid_... [2] "One important future step is to con- dense commonalities of these libraries into an ontology for crypto-related reasoning principles, reusable across multiple language levels and realised in multiple proof assistants. "