Tamarin induction performance problem with list-based iterative model

[Nikodem Witkiewicz]

Hi, group

I have encountered an efficiency problem with induction. There is a list of pairs <X, t or f> where the X values are fresh and t and f are constants. For each pair, we check whether the constant is t or f. If it is t, then the fact P(X) is created; otherwise, nothing happens. Finally. there is a rule called "Use" that requires P(X) in its premise in order to apply. I want to prove that if the pair with X contains the constant f, then there is no "Use" rule with P(X) in its premise.

To prove the lemma, I constructed some helper lemmas so that Tamarin does not end up in an Infinite loop. Surprisingly, proving the lemma still requires a huge amount of resources. When I use a two-element list, it takes 84023 steps, and with three-element lists, the process is killed after using roughly 25-30 GB of RAM.

I resolved this problem by excluding the iterative algorithm. I wrote a separate rule for each case. Consequently, Tamarin proves the lemma in less than a second. However, using the iterative algorithm and induction would be more convenient for larger lists.

I would appreciate any advice on how to reduce the complexity of the problem.

I am sending the following attachments:

• code for the two-element iterative model;
• code for the three-element iterative model;
• code for the three-element non-iterative model.

Cheers,

Nikodem