[Verifpal] (feature request) Multiple scenarios

[Nadim Kobeissi]

Dear Aurélien,

This seems like a great idea! Noting this down as a target feature to support. I definitely think I will implement this, I’m convinced it would be an excellent addition.

Thanks,

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 1, 2019, at 12:12 PM, Aurélien Nicolas <aurel at qed-it.com> wrote:
> 
> 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
> 
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal