This repository accompanies the paper "A Tight Security Proof for SPHINCS⁺, Formally Verified", authored by Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub.
The most recent version of the paper can be found here.
This repository comprises EasyCrypt scripts primarly aimed at the formal verification of the security of SPHINCS⁺, effectively verifying a modular version of the proof presented in
Recovering the Tight Security Proof of SPHINCS⁺.
Due to the module approach, we are able to reuse some of the artifacts produced in the formal verification of XMSS.
Furthermore, this repository contains several generic, reusable libraries (employed in the development) that are either novel or improvements over previous libararies.
-
Notifications
You must be signed in to change notification settings - Fork 0
This repository accompanies the paper "A Tight Security Proof for SPHINCS⁺, Formally Verified", authored by Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub.
License
MM45/FV-SPHINCSPLUS-EC
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
This repository accompanies the paper "A Tight Security Proof for SPHINCS⁺, Formally Verified", authored by Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub.