Partial deconstructions on adversary rules

[Petar Paradžik]

Dear all,

I'm experimenting with some custom rewrite rules for Diffie-Hellman. After
defining rules and starting Tamarin in interactive mode, I get partial
deconstructions that are the result of the corresponding adversary rules. The following
image should make things more clear.

I suppose that the last deconstruction chain cannot be solved because it starts
with the message variable "x.18" and the constraint solving rule for
deconstruction chains (last rule in Figure 10, on page 10, in Automated
Analysis of Diffie-Hellman Protocols and Advanced Security Properties)
disallow refining chains that start from a message variable.  Now, if partial
deconstructions were consequence of a protocol rule, they would be resolved by
source lemmas.  On the other hand, this problem is internal to Tamarin and
adversary rule "#vr16" does not have action facts required to specify the
internal source lemma.  Do you have any advice on how to approach this
problem? I guess one could use different rewrite rules to avoid the problem
in the first place.

Thanks.

Best regards,
Petar

[Petar Paradžik]

Nevermind, I think I figured it out.

Thanks!

Best regards,

Petar