Verifying helper lemmas about sub-protocols without case splitting on how it's used

[Lucas Lin]

Hello everyone, 

I am modeling a protocol that uses PAKE (password-authenticated-key-exchange) as part of it's protocol. I wanted to prove that the adversary must know the password to know the generated shared key. 

```
lemma Adversary_Must_Know_Password_To_Know_Init_Shared_Key [reuse]:
    all-traces "
        All password shared_key #i #j.
            PAKE_Init_Success(password, shared_key) @ #i &
            K(shared_key) @ #j
        ==>
            (Ex #k. K(password) @ #k & #k < #i)
        "
```
autoprove easily found the prove when I modeled PAKE in it's own file (allowing the adversary to start arbitrary runs) but when I tried to include it in my bigger protocol, autoprove no longer works. I tried manually proving it but also got lost in all the cases of the way pake was used. My understanding is that since the pake works for any arbitrary password it shouldn't matter how it's used in the protocol, so the lemma should always hold without the solver needing to case-split on how it's used. 

Does anyone know of better ways to compose protocols? Perhaps, instead of putting the real PAKE in my bigger protocol I should replace it with a ideal pake similar to simulation proofs and argue informally that it's reasonable? 

Less specific to just PAKE, I would really like to figure out if there's a way to neatly slot in protocols that take arbitrary inputs into bigger protocols. I'm analyzing Bluetooth and by focusing on authenticating an arbitrary transcript, the solver finishes in a minute whereas including dh key exchange and exchanging IO capabilities explodes the solver time to several hours and makes it really hard to make progress.  

[Ziyu Mao]

Hi, 
Regarding your attached theory pairing_as_authentication_XNC, I ran it with --heuristic=S and found that the lemma you are interested in can still be proved automatically with the latest Tamarin within about 90 seconds (though not instantly). You might try: tamarin-prover pairing_as_authentication_XNC.spthy --prove=Adversary_Must_Kno
w_Password_To_Know_Init_Shared_Key --heuristic=S.

[Lucas Lin]

Thanks for the tip, I'll do that.