Hang while Saturating Sources

[Daniel Zimmerman]

Hi, all! I'm having a confusing issue that I'm not sure how to even begin to address. I have a theory that parses fine, precomputes fine, and where all the lemmas verify (though some are a bit time consuming). I then add one additional rule to the theory, and Tamarin can't even finish precomputation; it hangs during the process of saturating sources, and when I watch the verbose output, it just hangs after a while (presumably stuck while attempting to solve a goal that it hasn't output to the console yet; it doesn't respond to Ctrl-C when in this state either, and I have to kill it externally). I haven't let it run long enough in that situation to see if it would eventually die due to lack of memory, but maybe it would. I tried running the interactive prover with "-s=0" to see if I could load the theory and see what's going on, but once I click on it in the interactive prover, it hangs there as well in the same fashion.

I've attached the theory, with the problematic rule commented out (it's easy to find, because it says "RULE COMMENTED OUT BECAUSE IT HANGS TAMARIN"), to this message. If anybody happens to have the time to take a look. Any suggestions would be appreciated.

Thanks!

-Dan

[Felix Linker]

Hi Dan,

I had a quick look, it's weird indeed. I have two theories.

Theory A: The commented out rule itself is not the "real" culprit, because (a) none of its conclusions or action facts are referenced anywhere, (b) it only sends one message that seems of a "boring" format. You just send a signature and some values. However you do use !TAS_Trustee_Set as a premise and it seems that this fact may do some looping. So it could be that the rule TrusteeSetup_TAS_Finalize_Registration actually causes problems, but Tamarin doesn't explore it in precomputations because its conclusion isn't used. I'm not entirely sure, though, whether Tamarin would not explore it if its conclusion isn't used, but maybe worth checking out.

Theory B: In your message, you send out this variable "name" which can come from TAS_State_RegisterTrustee (which can loop), and which again can come from TAS_State_IdentityKeyGen where "name" is a fresh variable. It could be that you run into partial deconstructions here because Tamarin tries figuring out what "name" can be (Tamarin could think: "Maybe a fresh value?! Indeed a fresh value! Worth looking into!") and gets stuck. You could easily test this hypothesis just by replacing "name" with a public value in this rule.

I hope one of these theories helps you!

Best,

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/b79fd45a-b277-4184-a3c8-14a2b24db405n%40googlegroups.com.

[Daniel Zimmerman]

Thanks for the quick response! I tried your easy test for theory B, and that did fix the problem - but of course, only doing it for that rule is problematic because it can't execute if nothing ever generates a fact with a public name. I actually decided that it would be reasonable to replace `name` with a public variable everywhere (all the names are public anyway), so now it's `$name` everywhere (with no Fr(name) facts); I've attached the updated version. Once I did that, though, I had the same issue again. With that change in place I tried it on a larger machine than I was using, and found that Tamarin actually _does_ complete the precomputation - it just uses a huge amount of memory, takes about 20 minutes, and comes up with 126240 partial deconstructions (though, interestingly, it is then still able to prove all the lemmas it was able to prove before, which I find surprising in the presence of so many partial deconstructions). I'm going to try to get the interactive prover to dump that very large list of partial deconstructions so I can see what's going on (though it may not be able to do so with the resources I have); maybe there's a straightforward source lemma to add that would help get rid of them, though I'd imagine it wouldn't help with the precomputation time.

With respect to your Theory A, !TAS_Trustee_Set does not do any looping - at least, it was not intended to. A different fact, TAS_RegisterTrustee_Set, does looping; but it's not one of the premises of that possibly-problematic rule, and the looping it does was part of what the lemmas in the file verified as behaving properly.

[Daniel Zimmerman]

As a quick follow-up, I decided after watching some verbose output to see if cutting down the MIN_TRUSTEES() and MAX_TRUSTEES() to both be "(%1)" would give me something more manageable, and indeed it does; it results in only 64 partial deconstructions (though the lemmas still verify). But the partial deconstructions seem... weird. Every single source for a partial deconstruction is that one rule that I had originally commented out, and it's reporting partial deconstructions for facts like "!KU(%1)" (doesn't make sense to me, since natural numbers are all public anyway) and "!KU(verify(t.1, t.2, t.3))" (doesn't make sense to me, since verify is a public function). I wonder if my particular use of multisets and natural numbers has somehow triggered some, for lack of a better term, bizarre behavior during precomputation.

I suppose the thing to do now is to come up with a different strategy for modeling this particular protocol, but it really would be interesting to know what is going on here.

-Dan