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

FirstTimeUserWithLoop.spthy

theory FirstTimeUserWithLoop
begin


/* Alice&Bob specification

	I knows:k
	R knows:k
	I -> R: senc(n,k)

*/

builtins: symmetric-encryption

/* protocol */

rule setup:
	[ Fr(~k), Fr(~m) ]
	--[]->
	[ AgSt($I,<~k,~m>), AgSt($R,~k) ]

// 1: Create new setup lemma to generate state for initiator, I
rule some_setup:
	[ Fr(~nonce) ]
	--[ A1(~nonce) ]->
	[ State($I, ~nonce) ]

// 2: Add `State($I, ~nonce)` to both input and output
rule I_1:
	[ AgSt($I,<~k,~m>), State($I, ~nonce) ]
 	--[ Send($I,~m), A2($I, ~nonce) ]->
	[ Out(senc(~m,~k)), State($I, ~nonce) ]

rule R_1:
	[ AgSt($R,~k), In(senc(m,~k))  ]
	--[ Receive($R,m), Secret(m) ]->
	[ ]

lemma nonce_secret:
	"All m #i #j. Secret(m) @i & K(m) @j ==> F"

// 3: Did not change lemma. But now loops in GUI while pressing `1` repeatedly
lemma functional: exists-trace
	"Ex I R m #i #j.
		Send(I,m) @i
		& Receive(R,m) @j "

// 4: Try adding sources lemma to break loop
//    (instead of using persistent State() )
lemma break_loop [sources]:
	"All I n #i. A2(I, n)@i ==> (
		(Ex #j. KU(n)@j & j<i) |
		(Ex #j. A1(n)@j)
	)"

end

// $ tamarin-prover interactive FirstTimeUserWithLoop.spthy --quit-on-warning