Modified version of FirstTimeUser.spthy that loops in rule I_1 when pressing 1 repeatedly

[Daniel Andrade]

Hello.

I modified FirstTimeUser.spthy by adding the same state, State($I, ~nonce), to the input and to the output of rule I_1. Then tried finding a trace for lemma functional.

1. Using autoprove still presents a solution, although I_1 is repeated three times.
   
2. Pressing 1 repeatedly, however, leads to non-termination since I_1 keeps repeating.

For the first case, I don't know why it terminates with autoprove, though I suspect it's due to iterative deepening.

For the second case, I'm trying to solve the issue using a sources lemma. However, this doesn't appear to be working. Which leads me to the question:

Is my sources lemma incorrect, or could it be that a sources lemma cannot solve this issue? (Maybe because I'm applying it to a state fact and not to a message?)

• Note 1: Using a persistent fact for State() would solve the problem, and generate a proper figure without repeating I_1, but I'm wondering whether this can be solved with a sources lemma instead.
• Note 2: Tamarin doesn't seem to consider this case as a partial deconstruction, or at least it doesn't appear in the GUI as such (is says deconstructions complete).
  

The modified version of FirstTimeUser.spthy is at this gist:
https://gist.github.com/andrade/7ec537eda56338c44a6927e9784c8b71

---

Figure for first case (autoprove, terminates, but repeats I_1 x3):

Figure for second case (pressing 1, non-termination):

---

P.S. I'm a graduate student working in systems security (TEEs, e.g. SGX), not in formal verification, so I could be asking something that is obvious for someone with a background in this area.