Inconsistent trace

[Jan Winkelmann]

Hi all,

after a long break I'm back on a project where we analyze a project
using Tamarin. This time the context is a protocol where parties
broadcast information to other parties which then update their local
state accordingly and sometimes broadcast a response.

In one of our properties we found an attack trace that doesn't make
sense to us. The facts consumed in the AcceptInvite rewrite rule at
the bottom appear inconsistent. The In(..) fact contains both
pk(~devSK.1) and pk(~devSK), while the !Device facts consumed only use
pk(~devSK). The rule is as follows:

rule AcceptInvite:
let
invTxt = <'invite', fid, InvrVK, InveeVK>
InvrVK = pk(InvrSK)
InveeVK = pk(InveeSK)
invitation = <invTxt, sign(invTxt, InvrSK)>
acceptTxt = <'accept', fid, InveeVK>
acceptMsg = <acceptTxt, sign(acceptTxt, InveeSK)>
in
[
In(invitation),
!Device(InvrVK),
!Device(InveeVK),
!State_IsInFusionID(InveeVK, fid, InvrVK)
]
--[
StateChange_ConsentedToFusionID(InveeVK, fid, InveeVK),
InvitedBy(InvrVK)
]->
[
!State_ConsentsToFusionID(InveeVK, fid, InveeVK),
Out(acceptMsg)
]

I would expect that the InveeVK and InvrVK from the !Device facts
would need to be consistent with the local macro 'invitation'.
However, the InveeVK in the acceptTxt macro is pk(~devSK.1). The fact
that this trace is shown as an attack makes me thing that either our
model is wrong or that I am missing something in how to use Tamarin or
interpret the results. Any insight in why this is shown would be
helpful!

The attack trace and full theory are attached. We are trying to prove
the lemma only_accept_when_invited_trivial.

I am looking forward to your ideas!

[Cas Cremers]

Hello Jan,

One thing I noticed in your model in the 'let' construct is that you don't use it in the more common "replacements are applied in the following"; instead using InveeVK on the right of the invTxt definition, and then later defining InveeVK a few lines down. Tamarin internally just syntactically replaces such let constructs in whatever follows inside the rule; I suspect your model means that after those substitutions, there is still an (otherwise unbound) InveeVK in invTxt. I guess you mean that "all" InveeVK should be replaced, but your model misses that first one.

I recommend swapping the order of the lines in the let, such that you define invTxt *after* you define IveeVK, and see if that makes a difference. Recall the intuition for the `let x=y` lines is: replace all following occurrences of x by y, within this rule.

Best,

Cas

--
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/20210826201137.Horde.XvsFpa0AzJSjqSo2NVAYnqC%40webmail.tu-harburg.de.