Looping behaviours when using counters with natural-numbers and GreaterThan restrictions

[Daniel Clark]

Hi,
tl;dr: How can I model counters using natural-numbers and a GreaterThan restriction such that incoming messages can have any higher counter (not just exactly 1 higher), without causing looping behaviour?

I've created a simplified model (attached) that exhibits the issue I'm having, where Tamarin gets stuck in a loop calling rule R4. We can see the issue when we're trying to solve Secrecy_M4 (which I know should fail), and the exists-trace lemma canAcceptM4. Lemma canAcceptM4_Once gives the ideal trace. There are a few Partial Deconstructions but --auto-sources handles them without issue. I've included the tactic DePrioritiseCounter which quickly and cleanly demonstrates the issue.

The quirk in this protocol is that the M3 message (rule R4), can be sent by the client multiple times, without waiting for a response before sending the next message, and increasing the counter each time. This causes Tamarin to endlessly loop when trying to solve it, ever increasing the counter. This quirk also means that an incoming message could have a counter that's more than 1 higher than the internal counter, hence my use of a GreaterThan restriction.

I feel like the correct solution here is some sort of inductively proven reuse lemma, but I just can't wrap my head around it.

Thanks so much for taking the time to read this and I'd really appreciate any input on my issue,
Dan