DH and Partial Deconstructions Question

[Emilie]

Hi there,

I'm learning Tamarin by modelling an Oblivious Pseudo-Random Function. I'm running into some difficulties with partial deconstructions due to the DH exponentiation.

Here is an example:


(In my model, the server has a secret k. The client sends a blinded value over, and the server raises this to power of k. I'm trying to prove that k remains secret.)

I've read Chapter 9 of the Manual and some threads on this group. As I understand it, Tamarin thinks it can derive any value from this rule, and I should resolve this by adding a sources lemma stating where the facts could come from. I've modelled mine after what was shown in the Manual (this proves but did not help reduce deconstructions).

```
lemma types [sources]:
    "
    (All res k #i . ServerRespond(k, res) @ #i
    ==>
        (Ex #j . !KU(res) @ #j & #j < #i) |
        (Ex #j . Out_ClientSend(res) @ #j & #j < #i))
```

It seems the issue is more that symbolically, the model can "know" inv(k) in t.1^inv(k). I've tried to write some restrictions/lemmas to avoid this, but I can't use inv nor ^/* so this hasn't helped.

The only thing I can think of is using a custom function to model the exponentiation instead of using the DH builtins. This feels unsatisfying but seems sound.

Would anyone have any pointers for how to reduce the partial deconstructions? Are there any similar DH proofs that I could reference? Spec attached — thanks for any insights or help.

All the best,
Emilie

[Felix Linker]

Hi Emilie,

Sorry for the delayed response.

The reason your lemma doesn't help is because the adversary can learn "res ^ ~k", which is not res. So proving a sources lemma referring to res, doesn't help.

I once proved something about a theory too that uses three Diffie-Hellman exponentiations. You can find that model here: https://github.com/lumaier/securedrop-formalanalysis/tree/develop One way I aproached partial deconstruction was to force that the incoming term is of shape 'g'^x via pattern-matching. This effectively assumes that you receive a valid group element, e.g., not DH_neutral. This should fix the issue because the most the adversary can learn from such a term through cancellation is 'g', which doesn't help them.

Maybe try that out. Let me know whether it works!

Best,

Felix

[Emilie]

Hi Felix,

The pattern matching on 'g'^x instead worked! Thank you so much for the pointer and for your reference model.

All the best,

Emilie