Issue with Diffie-Hellman pre-computation when keys are split across rules

[martin-d2]

Sorry for the slightly weird question / bug report; to some extent I've found a workaround, but I still don't know why it's behaving like this.

The following spthy seems to get stuck indefinitely in pre-computation.

theory DH_example
begin

builtins: diffie-hellman


rule New_Server:
	[ Fr(~svrKey1), Fr(~svrKey2) ]
	-->
	[ Server(~svrKey1, ~svrKey2) ]

rule New_Endpoint:
	let 
	endpointPubKey = 'g' ^ ~endpointKeySecret
	in
	[ Fr(~endpointKeySecret) ]
	-->
	[ Endpoint(endpointPubKey) ]

rule Key_Error:
	let
	key1 = endpointPubKey ^ svrKey1
	key2 = endpointPubKey ^ svrKey2
	in

	[ Server(svrKey1, svrKey2), Endpoint(endpointPubKey) ]
	-->
	[ Error(key1, key2) ]

end

If I change svrKey1 and svrKey2 in Key_Error to be marked as fresh ~svrKey1 and ~svrKey2 (in the let/in section and in the Server(...) fact), it finishes pre-computation instantly. Similarly, if I generate the keys as fresh locally in the Key_Error rule (and they're therefore marked fresh) it is fine.

Weirdly, if we only have one key in the Error(...) fact in the Key_Error rule, it takes a second or so to do the pre-computation, but is otherwise fine — either one of key1 or key2. It only seems to break with two (or more?)

Do you know why this breaks Tamarin's pre-computation? By inspection, the svrKey1 and svrKey2 values can only be fresh, but I guess it isn't working that out for some reason.

Any thoughts appreciated! :-)