A Question about Adversary Capability

[Daniel Zimmerman]

Hi, all!

I've attached a theory that implements a fixed variant of the Needham-Schroeder symmetric key protocol. All the lemmas verify, but I had to include a restriction that I wouldn't have thought I needed to include, about the adversary not discovering any of the long-term keys shared between the server and the other protocol parties. Those keys are established with a rule like this:

rule Setup:

[ Fr(~k) ]

--[ KeyGen($A), SharedKey($A, ~k) ]->

[ !SharedKeyWithServer($A, ~k) ]

These shared keys are never sent in messages, though they are used to encrypt messages (with the "symmetic-encryption" builtin). I also had several partial deconstructions, for which I wrote source lemmas; but once I did that, I was still left with many partial reconstructions, which all had in common the fact that the adversary somehow used one of these shared keys to forge a protocol message. Adding the restriction:

restriction SharedKeysRemainSecret:

"

All A k #i.

SharedKey(A, k)@i

==>

not (Ex #j. KU(k)@j)

"

eliminated all of those (though, when I had originally written the restriction with "K(k)" instead of "KU(k)", it did _not_ eliminate them and the adversary kept somehow using those keys in the partial reconstructions.

I feel like there must be something I'm misunderstanding about adversary knowledge, or I've made some kind of silly mistake in my protocol theory, because I can't figure out how the adversary could derive these keys. Any insight would be much appreciated.

Thanks!

-Dan ZImmerman

[Ralf Sasse]

Hi Dan,

The main point to think about when adding a restriction is that it is an additional assumption that you are making. Tamarin then uses this assumption and has an easier time proving other properties, of course. Thus, adding the assumption that certain keys are never known by the attacker can very easily lead to missed attacks. 

An extreme example showing this issue is to add the restriction "false" after which you can prove any all-traces lemma, as there are no traces anymore.

For your protocol, the source for the partial deconstructions is that certain opaque values are being sent around as part of larger messages, are then decrypted, and output in the clear (they are also encrypted, but it's a free variable in the rule it happens). These could/should usually be other encryptions with specific content [unless the adversary maybe inserted them?], but you need to convince Tamarin of that. Your sources lemma unfortunately does not help, while the --auto-sources produced lemma also does not help. So, you need to consider a different sources lemma. I would suggest starting with a prefix of the protocol (commenting out later rules) and see if you can solve that.

Note that partial deconstructions do not mean that Tamarin knows a way the adversary can derive something, but rather, that Tamarin is not yet convinced that the adversary cannot derive that specific thing. This is subtle but important to realize. The sources lemma gives Tamarin the help to understand what the content is, and thus how it won't help.

KU vs K is an internal difference, and indeed it is sometimes necessary to use KU, specifically for sources lemmas.

Cheers,
Ralf

--
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/fcb8fbc0-43a6-41ef-9e4c-79f178e3696cn%40googlegroups.com.

[Simon BOUGET]

Hi Ralf,

> KU vs K is an internal difference, and indeed it is sometimes necessary to use KU, specifically for sources lemmas.

I'm not sure how to interpret this, sorry ^^'

Should we always use KU for source lemmas?

Should we never use KU for NON-source lemmas?

Or is it something in between with maximum uncertainty?

Also, maybe a more practical approach: if I'm in front of my own protocol, how can I determine if my specific case is one of those exceptions where KU is necessary?

Thanks!

--Simon

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/8e1b5cf8-3137-4055-bee8-37f7a681c527%40inf.ethz.ch.

[Cas Cremers]

Hi Simon,

TL;DR: Use K, not KU/KD. However, if you have some understanding of Tamarin's internals, it is okay to sometimes use KU for auxiliary lemmas (source or not) where it can help for some properties.

For your main lemmas (the actual theorems you aim for) the recommendation is to always use K, because KU/KD are not formally defined in the semantics.

In general, when K works, using KU/KD would be strictly worse.

There are cases where K doesn't allow you to prove some properties. Notably, you cannot use K to formalize something like "If the adversary reaches state S, it must have also derived t" because term derivations do not need to lead to K facts in the action trace -- which you can see from the formal semantics and the interaction with the adversary rules. However, in the current implementation of Tamarin's adversary rules and search algorithm, a constructive adversary derivation of t in the process of reaching S will cause a KU(t) in the action trace. This can help to prove some properties, and is also useful for induction.

For auxiliary lemmas (i.e. reuse) it can sometimes be helpful to use KU as suggested above, and since this is only an intermediate step, it means that the main lemma/theorem is still well-defined even if some future change to Tamarin's algorithm subtly changes the meaning of KU/KD in side cases.

Soon we will publish some more guidelines on this.

Best,

Cas

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/CABhg3Hnh-530Av7raYWrU30CMa88iZj1U00Xt0vzfd7mymgqoQ%40mail.gmail.com.

[Simon BOUGET]

Very clear explanation, thanks a lot Cas.

--Simon

To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/CABdrxL70GNNT9828Y_Ne3jLm-xC3h8_KHznn1WfTLZX3477CWQ%40mail.gmail.com.

[Daniel Zimmerman]

On Tuesday, March 4, 2025 at 4:57:46 PM UTC+8 Ralf Sasse wrote:

For your protocol, the source for the partial deconstructions is that certain opaque values are being sent around as part of larger messages, are then decrypted, and output in the clear (they are also encrypted, but it's a free variable in the rule it happens). These could/should usually be other encryptions with specific content [unless the adversary maybe inserted them?], but you need to convince Tamarin of that. Your sources lemma unfortunately does not help, while the --auto-sources produced lemma also does not help. So, you need to consider a different sources lemma. I would suggest starting with a prefix of the protocol (commenting out later rules) and see if you can solve that

I took a closer look, and it seems (unsurprisingly) that this only becomes a problem when there are multiple different "kinds" of opaque value being sent around. I wrote up a simple theory (ping.spthy, attached below) with 3 roles: a sender, a receiver, and a relayer. The sender and receiver share a key (as do the relayer and the receiver, but that's not used until the follow-up theory), and the sender symmetrically encrypts a nonce and sends it as an opaque value alongside its ID (in the clear); that's relayed by the relayer, which adds its own nonce and ID (both in the clear) to the message alongside the sender's ID and the opaque value. The receiver then receives that and decrypts the opaque value. No partial deconstructions occur when that protocol is analyzed, and I am able to prove a couple of lemmas about it. 

However, if I extend the protocol so that the receiver then responds to the sender, generating a new opaque value that must be decrypted by the relayer as an intermediate step (pingpong.spthy, also attached below), then I (again unsurprisingly) get partial deconstructions (this is, of course, a simplified version of the first few steps of the protocol I had before). The difficulty I'm having is that I can't figure out how to get rid of them; I can write lemmas that reduce the number of partial deconstructions (for example, by adding a couple of action facts I can write that the receipt of a particular nonce by the receiver must have been preceded either by an adversary derivation of that nonce or by a sender send of that nonce), but Tamarin can't prove those. And often, I'll write a lemma that I _think_ should reduce the number of partial deconstructions, and that Tamarin is indeed able to prove, but it ends up _increasing_ the number of partial deconstructions instead (which doesn't make sense to me at all; why can a valid sources lemma, even if it's not particularly helpful, make Tamarin less able to determine what the adversary can or can't derive?).

I assume that there's something fundamental that I'm not understanding about how to address partial deconstructions/how to construct good sources lemmas. Again, any assistance would be much appreciated.

-Dan