Diffie-Hellman with Symmetric Encryption Execution Problem

[Ali S]

Dear Tamarin group,

I have a simple Diffie-Hellman model with symmetric encryption, where an initiator sends a fresh request and a responder replies with a fresh response. Both messages symmetrically encrypted with DH established keys.

The responder has a long-term DH key initialized in rule Resp_1 rule, and receives requests encrypted with a session key generated with this long-term key and the initiator's DH key.

In the following rule, the responder receives a request encrypted with the public key of the initiator and long-term key of the responder. Then, generates a fresh DH key and uses it to encrypt the response along with the initiator's public key (received in the premises). However, when I include the received request (req) in the response sent in the following rule, the executability lemma fails and the initiator does not receive the response. If I remove the request, it works fine. Could you please provide some guidance on what I might be doing wrong in this scenario?

rule Resp_2:
        [
          !Rltk($R, ltk) // Responder has access to its private long-term DH key used for request encryption
        , In(< epkI, senc( <$I, $R, req>, epkI ^ ltk ) >) // Received from Init_1
        , Fr(~resp) //Fresh response
        , Fr(~ephR) //Fresh DH key
        ]
        --[
          NS_Responds(req, ~resp, epkI ^ ltk, epkI ^ ~ephR)
        ]->
        [
          Out(< 'g' ^ ~ephR, senc(< $R, $I, req, ~resp>, epkI ^ ~ephR) >)
        ]

// Initiator receives the response
rule Init_2:
        [
          Init_Waiting_Response($I, $R, req, ephI)
        , In(< epkR, senc(<$R, $I, req, resp>, epkR ^ ephI) >)
        ]
        --[
          Init_resp( req, resp, epkR ^ ephI )
        ]->
        [
        ]

Many thanks for your time and attention,
Ali

[Daniel Clark]

Hi!

So looking at your model there are a few of things to note:

1. From what I see when trying to prove it, it's not that tamarin fails to find a trace for your executability lemma, it just doesn't terminate when trying to prove it, is that correct?

2. If you open the model in interactive mode, and manually step through the proof (selecting "simplify" and then option 1 each time), your excitability lemma does actually prove fine. The fact that this result is different to when it's autoproved is a bit of a quirk of tamarin (see https://github.com/tamarin-prover/tamarin-prover/issues/343 and https://github.com/tamarin-prover/tamarin-prover/issues/118 for more info).

3. When you open it in interactive mode you can see that it's got 90 partial deconstructions left. If you look at the partial deconstructions (search for "partial" in the refined sources) - it's useful to turn graph simplification off for this (using the options menu in the top right) - it reveals that the issue, in all 90 cases, is how tamarin sources req, relating to the resp_2 rule.The manual has some good pages on fixing partial deconstructions, which I'd recommend you read. Luckily, in most cases, tamarin can fix these on its own, just add the --auto-sources flag to tamarin when you run it. --auto-sources will generate a sources lemma for you that teaches tamarin how to solve the partial-deconstructions via a sources lemma.

4. Notably when you try to prove that source lemma, it actually finds a trace by forging the init_1 message. If this is an expected attack then you'll have to not use auto-sources and resolve your partial deconstructions in a different way (the manual can help with this). If it this isn't an expected attack, then you should update your model appropriately and test again.

I hope this helps,

Dan

[Ali S]

Dear Dan,
Thank you so much for your detailed explanation, your answer has been very helpful in solving my problem.

The problem that I had was similar to the "Needham-Schroeder-Lowe Public Key Protocol" example in the "Precomputation: refining sources" section of the manual.

I used "auto-sources" switch as you mentioned, but it seemed to be a complicated solution for my current problem. So, I added a source lemma that solved the problem.

> 1. From what I see when trying to prove it, it's not that tamarin fails to find a trace for your executability lemma, it just doesn't terminate when trying to prove it, is that correct?

Exactly. For some reason Tamarin keeps generating resp_2 rule instances, without running Init_1 rule. Thus, the memory usage grows and auto-prove never ends. The graph was similar to "Why partial deconstructions complicate proofs" section of the manual.

Best wishes to you,

Ali