search

symbolicsoft / verifpal

Cryptographic protocol analysis for real-world protocols.
https://verifpal.com
GNU General Public License v3.0
41 stars 4 forks source link

Fix false attacks in authentication queries by rewriting primitives and checking later for equivalence #6

Closed max-p-log-p closed 1 month ago

max-p-log-p commented 4 months ago

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. The code in the email fails after the cleanup commit was added, but doesn't fail before the cleanup commit.

To test, use the code in https://verifhub.verifpal.com/45ae1e65ce5ea647a2985bb098dc35e4 and modify it so that bob uses the done message after it is received.

nadimkobeissi commented 1 month ago

Thanks!