Writing the definition of sha 256 in Coq must have been of great fun, hehe. | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		mpu on June 6, 2015 \| parent \| context \| favorite \| on: Verified Correctness and Security of OpenSSL HMAC Writing the definition of sha 256 in Coq must have been of great fun, hehe.

YAYERKA on June 6, 2015 [–]

"Verification of a Cryptographic Primitive: SHA-256", Andrew Appel

https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf

nickpsecurity on June 7, 2015 | [–]

Thanks for the link. I always enjoy reading Appel's work.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact