[Verifpal] (feature request) Multiple scenarios

[Aurélien Nicolas]

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,
Aurel
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190901/a5134627/attachment.htm>