-
Notifications
You must be signed in to change notification settings - Fork 3
[Feature] Adding support for accountability lemmas #56
Description
Is your feature request related to a problem? Please describe.
batch-tamarin does not handle accountability lemmas. It is not possible to add such lemmas to a task as they are not statically in the .spthy file but only generated when invoking Tamarin.
This tool checks existence of every lemma specified in a task prior to invoking Tamarin; disallowing to specify such lemmas by their name.
Describe the solution you'd like
Handling accountability lemmas just as all other lemmas:
- allowing to reference individual acc. lemmas by their full name in the config file which means that the check of these files should take such lemmas into account and not just the static ones
- if a task does not specify a specific lemma ("run all lemmas") then all accountability sub-lemmas should be executed
Describe alternatives you've considered
I do not have strong opinions on the specific implementation, but likely one needs to invoke tamarin once prior to the task checks/when generating the tasks and scheduling the lemmas.
If this is undesirable overhead considering that accountability lemmas are rarely used, I could also think of an option in the config, which only does this when explicitly specified. Alternatively batch-tamarin could first look for the presence of acc. lemmas.
Additional context