Tamarin chooses to find complex trace before simple trace

[Daniel Clark]

Hi,

I'm experiencing an issue in a larger model where instead of my desired (and simplest) behaviour of sourcing two values from the same instance of a persistent fact, Tamarin defaults to creating a second instance of it and gets one value from each instance.

I'm not sure I've explained it well, so I've attached a minimal example.

Here's the trace for canEnd:

There's also the situation where I put a Once() restriction on the CreateA rule, and we get:

Neither of these are the desired outcome, which would be where rule A1 is only used once, and both ~a and ~b are pulled from that one A1 usage.

Obviously I could change !A(~a, ~b) to be a linear fact, or put a Once() restriction on A1, but I actually want Tamarin to be able to create these situations, I just want it to find the simpler "desired" case first.

I can't find a way to force this to happen even in the interactive mode. Am I missing something or is there a modelling trick to force my desired outcome, where it finds the trace where it sources both ~a and ~b from the same A1 instance first?

Thanks very much in advance

Dan

[Felix Linker]

Hi Daniel,

You’re not missing anything. Tamarin delays unification as far as possible, and will thus always first instantiate another rule before re-using an old one. This is the more general behaviour: You can still apply a unifier to make the rule instantiations of A1 become equal, but not the other way around.

I presume you want to prove an exists-trace lemma that should „look as expected.“ In this case, assuming that you only expect one instance of A1, you could simply add this expectation to your exists-trace lemma. For example:

  Ex ... (F() & All #x #y. A1() @ #x & A1() @ #y ==> #x = #y)

This should then give you a trace where TransferA and TransferB come from the same rule.

I hope this helped!

Cheers,

Felix

On 17 Apr 2024, at 21:52, Daniel Clark <danielcl...@gmail.com> wrote:

Hi,

I'm experiencing an issue in a larger model where instead of my desired (and simplest) behaviour of sourcing two values from the same instance of a persistent fact, Tamarin defaults to creating a second instance of it and gets one value from each instance.

I'm not sure I've explained it well, so I've attached a minimal example.

Here's the trace for canEnd:

<A1.png>

There's also the situation where I put a Once() restriction on the CreateA rule, and we get:

<OnceA1.png>

Neither of these are the desired outcome, which would be where rule A1 is only used once, and both ~a and ~b are pulled from that one A1 usage.

Obviously I could change !A(~a, ~b) to be a linear fact, or put a Once() restriction on A1, but I actually want Tamarin to be able to create these situations, I just want it to find the simpler "desired" case first.

I can't find a way to force this to happen even in the interactive mode. Am I missing something or is there a modelling trick to force my desired outcome, where it finds the trace where it sources both ~a and ~b from the same A1 instance first?

Thanks very much in advance

Dan

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/77de07b8-3811-4965-88c5-28b60da1c03dn%40googlegroups.com.
<A1.png><test.spthy><OnceA1.png>

[Daniel Clark]

Hi,
That's really useful to know about Tamarin delaying unification as much as possible. Thank you!

Unfortunately in my case, what I've actually got is a secrecy lemma, so restricting the search like you suggest could end up missing things. The reason why I'm trying to push Tamarin to investigate the simple/obvious/unified case first is that I know that secrecy is falsified even in that simple case, and this all actually happens quite late in the protocol, so Tamarin spends significant time/resources building multiple complex un-unified cases and eventually runs out of memory before finding the very simple vulnerability.

Have you any thoughts on what I can do?

Thanks again!
Dan

[Simon BOUGET]

Hi,

You can add a run identifier in your fact, and have your rule check that run ID.

So, to illustrate in your minimal example :

- change rule A1 to generate a fresh run ID Fr(~runID), and modified Transfer facts, with TranferA(~runID, a) and TransferB(~runID, b)

- then in rule X2, force the two facts in the premise to have the *same* runID, and you will ensure that both Transfer facts come from the same instance of A1

- later, when you want to start exploring the more complex cases, you can change X2 again to allow different run IDs, and this will go back to the situation you currently have. Note that you can do this JUST by changing X2, you don't have to modify A1 or the arity of the Transfer facts again, so it's relatively easy to do (at least in this minimal example)

It's hard to tell if this is a suitable solution for your *real* case, but I hope it can at least give you some ideas.

(By the way, totally unrelated to your question, but I think in rule A1 you should not force a and b to be fresh. Writing the model like that means that, at the time point when rule A1 is executed, the agent can be sure that a and b are fresh, so check if that is really what you mean.)

Best,

Simon

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/1924f735-c90e-465d-9a0d-013373394027n%40googlegroups.com.

[Daniel Clark]

Hi Simon,

That was actually super helpful, it seems obvious now you say it, but it gave me a bunch of ideas which were exactly what I needed, thank you!

Dan