[Verifpal] (feature request) Multiple scenarios

Aurélien Nicolas aurel at qed-it.com
Sun Sep 1 12:12:43 CEST 2019

Dear Nadim,

in the manual, a method is explained to simulate a scenario by modifying
the source file. E.g. what happens when Alice leaks her long-term key.

The scenarios could be captured permanently in the source file, for the
purpose of documentation and sharing the results with others. It could look
like this for instance:

// Normal protocol operations

queries [
    // Normal properties

    // Enter the scope of scenario 1: Alice leaks her key.
    Alice -> Bob: secret_key

    queries [
        // Properties that are still maintained in this scenario.

Then Verifpal would run multiple analysis in one go (one per queries block).

Thanks for the amazing work,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190901/a5134627/attachment.htm>

More information about the Verifpal mailing list