Executing SphincsPlus - Githubissues

GaloisInc / cryptol-specs

A central repository for specifications of cryptographic algorithms in Cryptol

BSD 3-Clause "New" or "Revised" License

30 stars 6 forks source link

Executing SphincsPlus #35

Open ramsdell opened 3 years ago

ramsdell commented 3 years ago

A coworker of mine, Becky Powell, has been trying to get SphincsPlus running within Cryptol. Before Cryptol 2.10, the performance of hash functions has made this goal impossible, but now, she gets some results. Alas, the results are not correct. The purpose of this issue is to share the driver files she used so that others can join the debugging process. The attached files are

SphincsPlus.diff - removes error reporting that trips up runs
Sphincs128sSHA256simple.cry - driver that selects parameters
SHA256MGF1.cry - pulls appropriate hash function from SuiteB
HMAC.cry - HMAC using SuiteB
SuiteB.cry - Copy of SuiteB used for tests
test_Sphincs.bat - batch file for Cryptol

SphincsPlus.diff.txt

Sphincs128sSHA256simple.cry.txt

SHA256MGF1.cry.txt

test_Sphincs.bat.txt

atomb commented 3 years ago

Thanks for pointing this out! When we originally wrote this we had the experience, like you, that we couldn't evaluate it on concrete test vectors, using the interpreter at the time. I'm glad that the new primitives make it possible to evaluate, and I'm sure the results of your initial explorations will help speed up figuring out what's wrong.