From ffd5807cbeddf2492579d0cd6214eceaccc0ae2a Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sat, 23 Mar 2024 10:26:42 -0400 Subject: [PATCH] Update README.md Adding last yard --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index f4d9120b..6e4374b9 100644 --- a/README.md +++ b/README.md @@ -12,6 +12,10 @@ This repository contains the Coq formalisation of the paper:\ ([ieee](https://www.computer.org/csdl/proceedings-article/csf/2021/760700a608/1uvIdwNa5Ne), [eprint](https://eprint.iacr.org/2021/397/20210526:113037)) +Secondary literature: +* **The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography** at CPP'24. +Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, and Bas Spitters. ([DOI](https://doi.org/10.1145/3636501.3636961)) + This README serves as a guide to running verification and finding the correspondence between the claims in the paper and the formal proofs in Coq, as well as listing the small set of axioms on which the formalisation relies