verifpal
verifpal copied to clipboard
Cryptographic protocol analysis for real-world protocols.
I'm trying out verifypal to prove some PAKE protocols, and I'm struggling with OPRF using passwords for blind salt, as in OPAQUE. - I cannot find out how to invert...
I want to prove the identity of one party through signing an arbitrary value provided by the other party. Either: - I do not know/have the appropriate query to express...
Here's a full log demonstrating the issue and hopefully giving enough to reproduce it. ``` $ verifpal --version verifpal version 0.27.2 $ cat chap.vp # available at https://verifhub.verifpal.com/10b484cb797eb532e64c8896eaa2d35b attacker[active] principal...
The commit bcefa459a79d435b88d26836f45148ad1260eb90 was added to address some false attacks in https://lists.symbolic.software/pipermail/verifpal/2020/000299.html, but was reverted by the "Cleanup" commit 35e0a28a64afeee67ea9bb587ae8eddcd8621e2e. The necessary lines seem to be in verifyActiveMutatePrincipalState in cmd/vplogic/verifyactive.go....