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