Tamarin building infinite chains of the same rule (similar to looping behaviour)

[Daniel Clark]

Hi,
I've got the attached simplified model, where:
    1. The Server sends its cert(certS) to the Client
    2. The Client verifies certS, then encrypts its own cert(certC) and a nonce(Nc) with the Server's public key (from certS)
    3. The Server decrypts and verifies certC and Nc.
Plus a simple non-injective agreement lemma that doesn't terminate.

The issue comes because the certificates have no identifying elements to indicate whether they're from a client or server. This means that the M2 rule has a valid source of certS by extracting the certC from another run of the M2 rule. This builds a chain of M2 rules that continues indefinitely. As seen from the image here (from manually stepping through for a while)




I know the manual talks about fixing loops by having an inductively proven reuse lemma like:
lemma AlwaysStarts [use_induction, reuse]:
    " All x #i. Loop(x) @i ==> Ex #j. Start(x) @j " // Effectively: If I'm looping on a value x, then at some point I started with x.
   
But I don't think I can apply this to my code because there is no "x", all the values in the loop change each iteration because it creates a whole new set of certificates.

I don't want to restrict the protocol to say that M2 can only source its certSs from M1, to limit it to only 1 or 2 Clients/Servers, or to add a field to the certificates to identify if they are for a 'Client' or 'Server', because it could then miss genuine attacks.

Ideally I'm thinking of some sort of concept that limits the size of that loop of M2s to only being one or two rules long.chain

Does anyone know of any way to stop Tamarin getting stuck in such loops? I feel like I'm just missing something obvious.

Thanks in advance,
Dan

[Ali S]

Hi Dan,

I am facing a similar issue. Were you able to find a solution to prevent Tamarin from repeatedly using the same rule as its own input? This usually happens, when I introduce new fresh values in the rules.

Thanks,

Ali

[Andy Hammer]

From what I can see, this is a similar issue to one that I had, where there was an infinite chain of the same rule. I referenced Issue 606 on the github, and writing a helper lemma with a weaker guarantee and reusing it help prove this stronger guarantee.

[Petar Paradžik]

User-defined heuristic may help.

Download attached oracle file and execute: tamarin-prover interactive --heuristic=O --oraclename=TestModel.oracle TestModel.spthy

[Daniel Clark]

Thanks so much for that reply, it works perfectly.

For future reference, that oracle deprioritises goals which solve for the server certificate.

I've rewritten it as the following simple tactic:
tactic: DePrioServerCerts
    deprio:
        regex "!KU\( sign\(<\$ServerID.*"

My understand of why this works, is because:

1. The server cert is what it's looping on

2. It's looping on it because the default heuristic is trying to find a server cert for the client to use in M2, but because it hasn't yet 'linked' the client and server via a complete message, it has no way of knowing what the "correct" cert is (i.e. which server it must belong to), so it sources it from infeasible places. The first infeasible place is a completely different server instance (which it soon discovers doesn't work), and then it tries to source it from another M2 instance, which causes the loop.

3. By deprioritising goals which look for the server certificate, it means it first solves the entire rest of the protocol, which solidifies which server it needs to find a cert for, and then solves for that cert (which it finds quickly).

4. Now of course if such a cert doesn't exist, then it would have to find a different solution for the rest of the protocol which does have a matching server cert, which may take time, but it wouldn't be stuck in that loop so it would eventually terminate.

Please do correct me if I'm wrong about any of this!

Thanks,

Dan