Unexpected counterexample trace on modified tutorial example

[Lucas Lin]

Hello, 

I am working through the initial example. I tried modifying it to allow a MitM attack. Tamarin found a counterexample trace but the counterexample trace seems to use the Reveal_ltk which should've been forbidden. 

To allow the MitM attack, I modified the Register_pk rule to send the public key into the insecure channel so the attacker can forge this message. The client reads the public key from the channel too. 
```
rule Register_pk:
    [ Fr(~ltk) ]
  -->
    [ !Ltk($A, ~ltk), Out(<$A, pk(~ltk)>) ]

rule Client_1:
    [ Fr(~k)         // choose fresh key
    , In(<$S, pkS>)   // lookup public-key of server
    ]
  -->
    [ Client_1( $S, ~k )    // Store server and key for next step of thread
    , Out( aenc(~k, pkS) )  // Send the encrypted session key to the server
    ]
```

I wanted to falsify the security property: 
```
lemma Client_session_key_secrecy:
  " /* It cannot be that a  */
    not(
      Ex S k #i #j.
        /* client has set up a session key 'k' with a server'S' */
        SessKeyC(S, k) @ #i
        /* and the adversary knows 'k' */
      & K(k) @ #j
        /* without having performed a long-term key reveal on 'S'. */
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "
```

This is the counterexample trace autoprove found. It doesn't use the MitM attack and instead calls Reveal_ltk on the server which I thought was disallowed by the `not(Ex #r. LtkReveal(S) @ r)`. 


If I instead simplify the reveal Ltk to not know about the device name, then Tamarin gives me the counterexample I expected to find where the attacker deceives the client by giving it a wrong public key. 
```
rule Reveal_ltk:
    [ !Ltk(A, ltk) ]
  --[ LtkReveal() ]->
    [ Out(ltk) ]
...
      & not(Ex #r. LtkReveal() @ r)
```


I've attached the .spthy files for the two pictures. They can be generated by running autoprove in the webui. 

Having no experience with Tamarin, I thought I might be misinterpreting the counterexample trace. Any help in clarifying what's going on would be greatly appreciated!

[Cas Cremers]

Hi,

There is no problem with the counterexample in your model, it is as expected based on your modifications.

Observe that the formula does not disallow *all* key reveals: it only disallows revealing the key of the party mentioned in the corresponding SessKeyC fact.

Ultimately, this counterexample is possible because in your modified Client_1 rule, there is no link between the identity ($S in the graph) and the public key (pk(~ltkS) : the network adversary can trivially change either.  That is in fact what happens in the example: the generated key pair was for server $S.1 , but the client thinks the public key is for server $S.

In your graph, you have a server $S.1 and a client who falsely thinks they are talking to server $S. The adversary changes the message pair (between register_pk) and client_1 so that the client incorrectly thinks the public key belongs to server $S. Then,  server $S.1 decrypts the message, and responds. The response is accepted by the client Client_2 rule, and the client thinks they computed a shared key with server $S, and logs an action fact SessKeyC( $S, ~k). In reality, the key ~k is shared with server $S.1 ; and thus the adversary can reveal $S.1's session key (because $S.1 != $S )

Hope this helps,

Cas

[Sasse Ralf]

Hello!

The issue is that in your 'unexpected' attack there are two servers. One, called $S.1 which is actually active and whose key is revealed. The other, $S does not show up directly but it's name is used to confuse the recipient. This is possible as you have modified the authentic key distribution via state facts to using the adversary modifiable channels. (This is a great way to try things out!)

Note that the formula

`not(Ex #r. LtkReveal(S) @ r)`. 

prevents only the specifically named server S also appearing in the session key fragment

SessKeyC(S, k) @ #i

To be the one that may not be revealed. In your graph, that S is unified as $S. So $S cannot be revealed. Any other name, including $S.1 can be revealed, which is what happened.

In your second version, where you use

not(Ex #r. LtkReveal() @ r)

No servers Ltk may be revealed at all.

So, the difference is that one particular name cannot be revealed vs the rule not being allowed to be used at all, rhus no server key can be revealed.

All the best, and happy proving,

Ralf

P.S.: excuse formatting and typos, typing on mobile.

--
You received this message because you are subscribed to the Google Groups "Tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/0a1ecd78-3fef-4080-926d-e3253d8fd7adn%40googlegroups.com.

[Lucas Lin]

I hadn't noticed the modifications would change how reveal works. The traces make a lot more sense now. Thanks for the clarifications.