A Question on Partial Deconstructions

[Daniel Zimmerman]

I've been working on some protocols that use a secure channel abstraction very much like the one described in the Tamarin book, and have run into some behavior around partial deconstructions that I don't understand. First, the secure channel abstraction:

rule SecureChannel_Send:
    [ SecureSend(~cid, S, R, m) ]
  --[ SecureChannel_Out(~cid, S, R, m),
      SecureChannel_Message(m) ]->
    [ SecureMessage(~cid, S, R, m) ]

rule SecureChannel_Receive:
    [ SecureMessage(~cid, S, R, m) ]
  --[ SecureChannel_In(~cid, S, R, m) ]->
    [ SecureReceive(~cid, S, R, m) ]

/*
  This rule models a compromised sender on a secure channel,
  where the adversary can inject messages.
 */
rule SecureChannel_Compromised_Inject:
    [ In(<~cid, S, R, m>) ]
  --[ Reveal(S, 'SecureChannel'),
      SecureChannel_Injected(~cid, S, R, m),
      SecureChannel_InjectedMessage(m) ]->
    [ SecureMessage(~cid, S, R, m) ]

/*
  This rule models the interception of a message on a secure
  channel.
*/
rule SecureChannel_Compromised_Intercept:
    [ SecureMessage(~cid, S, R, m) ]
  --[ Reveal(R, 'SecureChannel'),
      SecureChannel_Intercepted(~cid, S, R, m),
      SecureChannel_InterceptedMessage(m) ]->
    [ Out(~cid),
      Out(S),
      Out(R),
      Out(m) ]

What's happening is that, in some (but not all) protocols where all the communication (other than explicit reveals of keys and such to the adversary) is carried out using SecureSend and SecureReceive facts, I am seeing partial deconstructions— sometimes many of them—that cause Tamarin to spend an enormous amount of time in precomputation. But when I run with --auto-sources, Tamarin generates a sources lemma that boils down to generating actions on some (but not all) rules that use SecureReceive(cid, S, R, m), of the form AUTO_IN_FACT_...(cid, s, R, M), corresponding AUTO_OUT_FACT... actions on the SecureChannel_Receive rule (all of which are redundant with the existing SecureChannel_In(~cid, S, R, m) action) , and a lemma that says that the AUTO_IN_FACTs must be preceded by corresponding AUTO_OUT_FACTs but does not, in any way, mention adversary knowledge. This eliminates all the partial deconstructions.

If I replace the multiple AUTO_IN_FACT_...(cid, s, R, M)actions that --auto-sources generates with a single IN_SECURE_CHANNEL(cid, S, R, m)action in all the same locations (of course, replacing the cid, S, R, m variables with the appropriate local ones), eliminate all the AUTO_OUT_FACT... actions, and replace the very long lemma it generates with a short lemma that says that IN_SECURE_CHANNEL(cid, s, R, m) must be preceded by SecureChannel_In(~cid, S, R, m), that also eliminates all the partial deconstructions.

However, the lack of adversary knowledge in the lemma and the fact that there were partial deconstructions in the first place confuse me, because the SecureChannel_Receive rule is the only possible source of a SecureReceive(cid, S, R, m)linear fact, and if a partial deconstruction arose with respect to the original source of any fresh values mentioned in a SecureReceive, I would not expect that partial deconstruction to be resolved without mentioning adversary knowledge in the sources lemma. Meanwhile, my theory with 27 rules and restrictions (including the secure channel rules above) and 60 cases takes over 9 minutes of precomputation to find 840 partial deconstructions that are cut to 0 by seemingly just telling Tamarin "hey, this rule that is the only possible rule that can generate this fact is actually the one that generated this fact", without saying anything about adversary knowledge.

I feel like I must be missing something about "what makes a partial deconstruction". I'd appreciate any insight anybody might be able to share.

-Dan

[Felix Linker]

Hi Dan,

I'm not sure I was able to follow your thought process entirely, but I can tell you something more general about partial deconstructions.

Secure channel models are the most common place (in my experience) for partial deconstructions. Partial deconstructions typically occur if there is a rule that let's the adversary learn some term (in your case, that rule is SecureChannel_Compromised_Intercept) without any constraints (in your case, the adversary learns the free variable m) and Tamarin fails to find any constraints for that term during its precomputations. Tamarin only knows that the adversary can learn some free variable (could be anything) and whenever it now must consider whether the adversary learnt some concrete term during backward search, it must consider this rule.

Source lemmas only require referring to adversary knowledge if the adversary can influence which term they learn. For example, a decryption oracle rule like: [ In(senc(m,k)), !Key(k) ] --> [ Out(m) ] would also very likely lead to partial deconstructions. For such rules, you would typically write a sources lemma like: "For all messages m that the adversary learns from the decryption oracle, m comes from one of the cases of honest encryption, or the adversary encrypted m themselves." In the latter case, Tamarin need not consider the decryption oracle rule as a source of learning a term, because the adversary already knows it.

I am surprised you can solve the partial deconstruction issues by writing a source lemma referring to SecureChannel_In as that has no constraints on m either. My guess would be that maybe your saturation/open chains limit is just one too low, and by using that sources lemma, you allow Tamarin to start the sources computation from the SecureChannel_Receive rule. But that's really just a guess.

In general, your sources lemmas have the form: "For all terms that the adversary can learn from <PROBLEMATIC-RULE>, they come from one of the following honest-client rules: ...." And sometimes, you need an additional branch for adversary knowledge, if the term can be adversary provided.

I hope this helps!

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/6c1bf903-6a3c-47e8-b19d-0760a386c1f3n%40googlegroups.com.

[Daniel Zimmerman]

Felix,

That was very helpful, thanks. And what you said about partial deconstructions basically matched my intuition, particularly "In general, your sources lemmas have the form: "For all terms that the adversary can learn from <PROBLEMATIC-RULE>, they come from one of the following honest-client rules: ...." And sometimes, you need an additional branch for adversary knowledge, if the term can be adversary provided." - but that's where I was puzzled, because I'd have thought that saying "the terms must come from SecureChannel_Receive" would be insufficient, and because the sources lemma doesn't say anything like your general form at all - anything the adversary learns from SecureChannel_Compromised_Intercept _cannot_ come from SecureChannel_Receive, because the former consumes the same linear fact as the latter, so only one of them gets to execute. But eliminating the SecureChannel_Compromised_Intercept rule does eliminate all the partial deconstructions, as expected.

I did attempt to validate your guess by doubling the open chains limit and eliminating the sources lemma, and Tamarin didn't complain about there being too many open chains anymore, but it still ended up with 840 partial deconstructions. So that's not what's happening, which makes me more puzzled about what could actually be happening

I'd be happy to send along the entire theory, but it's nearly 1100 lines long (3600+ including proof scripts), and I know nobody's going to have time to look at that. But if I happen across a smaller example of the same phenomenon, I'll post it here.

-Dan