Chaining lemmas

[Jonathan Katz]

I am trying to using Tamarin to prove relatively simple things, but proofs are taking a long time. (To be clear: I am trying to use the command-line interface.)

Specifically, I can currently easily prove two lemmas

   lemma1: A => B

   lemma2: B => C

However, Tamarin runs exponentially longer when I try to prove

  lemma3: A => C

(note that I annotate Tamarin to reuse lemma1 and lemma2).

Are there some best practices for doing this? For example, would it be faster to prove

   lemma3': A => B & C

? Or should I just avoid the command line entirely?

In slightly more detail, my lemmas look like this:

   lemma lemma1 [reuse]:

  "All A B  #i.
     Predicate1(A, B) @ i
     ==>
     Ex C. Predicate2(B, C) @ i"

   lemma lemma2 [reuse]:

  "All B C #i.
     Predicate2(B, C) @ i
     ==>
     (Ex #j. Predicate3(B, C) @ j)
     | (Ex #k. Predicate4(B) @ k)"

and I would like to prove

   lemma lemma3:

   "All A B #i.

     Predicate1(A, B) @ i

     ==> 

     (Ex C #j. Predicate3(B, C) @ j)

     | (Ex #k. Predicate4(B) @ k)"  

--

Jonathan Katz Senior Staff Research Scientist | jkcr...@google.com Safeworks -- Applied Research in Privacy, Safety, and Security Google LLC

[Felix Linker]

Hi Jonathan,

Whether to use the command line is a matter of choice. I typically prove my models secure by starting from the final, desired security property, and only introduce auxiliary lemmas as required. This is easier if you have visual feedback. But when you only use the autoprover (pressing a), using the command line should be no different from using the UI.

"All P ==> Ex Q" lemmas can lead to a slowdown whenever the model allows for a P to be introduced from a Q, or when you can instantiate multiple Qs, e.g., because some parameters of Q are existentially quantified. This slowdown is independent of the chaining of lemmas as you describe it.

As you only experience the slowdown when proving lemma 3, it may be that in your case we have that C gives you an A, gives you a B, gives you a C, etc. It could also be that Tamarin ignores lemma 1 for lemma 2 as it's never applies/is not needed and thus not prioritized during proof search.

What can help is phrasing your auxiliary lemmas like: "All. P & (not Ex. Q) ==> Ex. Q," which will have similar effects in your backwards search.

Hope that helps! Please ask follow-up questions, should you have them!

Cheers,

Felix

--
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 visit https://groups.google.com/d/msgid/tamarin-prover/CADhumsncUbsUU-u%2BowJ5Y6vA-KDsWObt%2Bv%2B%3D__%3DUbo7xHcxX_g%40mail.gmail.com.