Collapse attacker derivations

[addap]

Based on cleandot.py, we collapse connected attacker derivation nodes.
For now the collapsible nodes are collected into a new type of "CollapseNode", which just contains the original nodes but is printed as a single point node. All edges that normally go to or originate from one of the collapsed nodes start/ends at the point node (internal edges are not rendered).

This example is taken from examples/csf12/DH2_original.spthy which gets quite large.

before	after

This is not a perfect visualization. As you can see on the right side, many nodes are collapsed into a single point and it looks like the box on the lower right depends on nodes on the upper left, although this is only because of the visualization.
As a next step it would be possible to remove the point node and instead connect the predecessor and successor nodes directly, creating new edges by merging the styles of the original edges.

[rsasse]

This is a great idea, being able to hide the details of what the adversary is doing inside the graphs. However, with the current status of the approach, and specifically in the graph in the example, it can be very misleading to the modeler.

As you state yourself:

it looks like the box on the lower right depends on nodes on the upper left, although this is only because of the visualization.

and looking at the graph pictures you provide (thanks a lot!) I find this to be a big issue. Maybe not even so much in this example, but much more in an example where there are some other protocol rules further to the top left, and their output is used by the adversary there. The visualization will then really confuse the modeler and link unrelated rules.

The suggestion of a direct connection of source and target nodes, without such a possibly misleading merge point, may be better, but does require some thought and a few examples to evaluate it.

[cascremers]

@rsasse we are not changing the default representation here: this is only under the toggle for more compact display methods (>= L3). I went through many alternative choices before, and this is a reasonable compaction.
We can later revise this if we need to.

[cascremers]

Looks good! The only missing thing is an explanation in the manual somewhere.

[rsasse]

Thanks @cascremers I see. Still, being possibly that misleading is not ideal, I fear. Any alternatives I was quickly thinking about to make this point clear, and prevent confusion, do end up going back to the non-compacted version in the worst case. So, I now understand the choice needs to be made to throw things together, with this possible side-effect. Alright!

Thanks @addap for contributing this!

[cascremers]

I did find some remaining bugs during testing. Consider the file NAXOS-eCK_PFS.spthy in Tamarin's examples/csf12 directory.
There is one lemma: autoprove a finds a counterexample/attack trace. With abbreviations, but without collapsing adversary nodes, the graph looks like this:

with collapsed adversary nodes, the graph looks like this:

Note the following bugs:

• There is a cycle at the bottom from and to the coerce #vk.5 node. This node should not be displayed in any case, but there should not be a cycle either.
• The node #vk.3 should have also been collapsed.

[cascremers]

p.s. @rsasse :
the original dependency graphs allow you to track all dependencies for all elements accurately. In contrast, in a linearized trace, one would not be able to see any of such dependencies anymore -- whatever preceeds an action "might" be a required predecessor, or could be independent. However, in Tamarin we have no guarantee that any produced dependency graph is "the most general" version of such a graph anyway.

When using L3 simplification, you can think of the collapsed nodes here as a middle ground that states "next, the adversary is going to take terms [t1,...,tN] and use them to produce some other terms [u1,...,uM] ".

If you want to know the exact dependencies, you just switch back to L2 (which is the default anyway).