Minimization/Pruning of Proof Scripts?

[Daniel Zimmerman]

Hi, all! In some modeling I've been doing, I've found it necessary to generate proof scripts for executability lemmas, because the amount of time it takes Tamarin to generate the proofs is prohibitive for continuous integration/verification processes. However, I'm running into an issue. 

In order for Tamarin to find the execution trace that satisfies the executability lemma, I have to tell it to search breadth-first (otherwise it tends to get stuck in loops)... but when seraching breadth-first, it produces a _huge_ proof script (for example, it gave me about 23MB of proof script for a trace that it found at depth 146) that includes all the proof steps it tried that didn't succeed. Is there any straightforward, automated way of pruning such a proof script so that it has only the one execution that it needs, or is the only recourse to prune it "by hand"?

Thanks!

-Dan

[Cas Cremers]

Hi Dan,

We often solve this differently. When you are looking for an exists-trace lemma (like executability), you can effectively provide "hints" for the proof search by adding more events with shared variables in your lemma. Since it is trace-exists, adding more events there does not invalidate the result. Instead, it just looks for a more specific example, narrowing the search space.

For example, assume you have a initiator role with 4 steps, where the last has an action "InitStep4(~tid,...)" and you want to express this is reachable. One way of writing this is:

  lemma Lemma1:
    exists-trace "Ex tid ... #i4 . InitStep4(tid, ...)@i4 "

However, you can also look for a more specific trace.

  lemma Lemma2:
    exists-trace "Ex tid ... #i1 #i2 #i3 #i4 . InitStep1(tid, ...)@i1 & InitStep2(tid, ...)@i2 & InitStep3(tid, ...)@i3 & InitStep4(tid, ...)@i4 

    & #i1 < #i2 &  #i2 < #i3 & #i3 < #i4"

More things that you could add to Lemma 2:
 - Where possible, bind the variables appearing in the actions across the multiple steps.

 - Add clauses to specify actions that should not appear, or appear only once, so they avoid your particular looping scenarios.

 - Specify that all received messages were previously sent by protocol rule instances (typically requires adding some actions to specify)

The second lemma is typically easier to verify because it looks for a much more specific trace. 

You can then convince yourself manually that lemma 2 implies lemma 1. Of course, if you want Tamarin to check, you can first prove lemma 2, make it reusable, and then write lemma 1 afterwards, after which the proof of lemma 1 should be trivial.

hope this helps,

Cas

[Daniel Zimmerman]

Thanks for getting back to me!

I have tried exactly what you suggested in the past, with varying degrees of success, but if all I want is a single proof of executability, it seems to me that I get the most success out of the least manual effort by just letting Tamarin do a breadth-first search (potentially overnight, but that's fine as long as I don't have to be sitting in front of it). I do still think it would be useful to have a "proof script pruner"; though; not just for this particular situation, but also for situations where I generate a proof script in the interactive prover and it ends up with a whole bunch of branches that are listed in the proof script but not taken, which take up (potentially a lot of) unnecessary space when I store them alongside/in the theory. Or, even more useful, perhaps Tamarin should have an option for exists-trace lemmas that tells it to output only the proof script for the first trace it finds.

If there isn't already a script out there that does this, perhaps I'll write one; I already have one that doesn't really work well at all, but works well enough that I can fix the resulting pruned proof script by hand and have it verify. 

Thanks again!

-Dan