Modelling multiparty protocols

[tamarin-prover]

Dear Tamrin Prover Maintainers,

I have just discovered Tamarin Prover as part of my research project. The user manual helped me to get to grips with the software very effectively, thank you very much.
I am looking to model a protocol involving 3 or more parties, starting with a very simple example with Alice, Bob and Carol. Alice generates a cleartext message and sends it to Bob, who forwards it to Carol. All the links are controlled by a Dolev-Yao adversary.

The protocol is as follows:
Alice -> Bob: msg
Bob -> Carol: msg

Alice will send the message using Out(msg), Bob will retrieve it using In(msg), then send it to Carol again using Out(msg), who will receive it using In(msg).

How can we model the fact that Alice only sends the message to Bob and not also to Carol?

Here is a proposal for modelling the protocol in question:

---

theory AliceBobCarolInsecure

begin

// Defining a directory server that contains identities if the parties

rule Node_Directory:

[ Fr(~idNodeA) ]

-->

[ !PubId($A, ~idNodeA)

, Out(~idNodeA) ]

// Each party get the identity of its predecessor and its successor

rule Init_Alice:

[ Fr(~idThreadAlice)

, !PubId(Alice, idNodeAlice)

, !PubId(Bob, idNodeBob)] //

-->

[ St_Alice_1(Alice, Bob, ~idThreadAlice) ]

rule Init_Bob:

[ Fr(~idThreadBob)

, !PubId(Alice, idNodeAlice)

, !PubId(Bob, idNodeBob)

, !PubId(Carol, idNodeCarol) ]

-->

[ St_Bob_1(Alice, Bob, Carol, ~idThreadBob) ]

rule Init_Carol:

[ Fr(~idThreadCarol)

, !PubId(Bob, idNodeBob)

, !PubId(Carol, idNodeCarol) ]

-->

[ St_Carol_1(Bob, Carol, ~idThreadCarol) ]

// Sending the cleartext message x

rule Alice_send_Bob:

[ St_Alice_1(Alice, Bob, ~idThreadAlice)

, Fr(~x) ]

--[ Send_toBob(Alice, ~x) ]->

[ Out(~x), St_Alice_2(Alice, Bob, ~idThreadAlice, ~x)]

rule Bob_receive_Alice_send_Carol:

[ St_Bob_1(Alice, Bob, Carol, ~idThreadBob)

, In(x) ]

--[ Recv_fromAlice(Bob, x)

, Send_toCarol(Alice, x) ]->

[ Out(x), St_Bob_2(Alice, Bob, Carol, ~idThreadBob, x)]

rule Carol_receive_Bob:

[ St_Carol_1(Bob, Carol, ~idThreadCarol)

, In(x) ] // <-- How can I model the fact that it comes from Bob, from the untrusted communication channel, and not from Alice?

--[ Recv_fromBob(Carol, x) ]->

[ St_Carol_2(Bob, Carol, ~idThreadCarol, x)]

end

---

I am aware that there are still some gaps in my knowledge of how to model protocols correctly. If you have any leads/papers or parts of the manual that I should focus on, I would like to hear from you.

I would be grateful if you could help me understand this.

Best regards,

Guillaume Nibert

[Simon BOUGET]

Hi there,

> How can we model the fact that Alice only sends the message to Bob and not also to Carol?

If you mean, "how to model that the message is 'physically' sent to Bob?"; you don't. With a Dolev-Yao adversary, it can always send the message to Carol anyway.

If you mean "how to model that Alice intend to send the message to Bob?", you record it in Alice state, it's about her information, not about what happens on the network. So what you did in your "St_XXX_1" is a good start.

However, you seem to assume more than what can really be deduced. For instance, in rule "Bob_receive_Alice_send_Carol" you add to the trace "Recv_fromAlice(Bob, x)", but Bob cannot know that this message is actually from Alice, it could be from anyone. All that Bob see is a message x arriving on the channel, he doesn't know anything else about this message.

Side-note: it's hard to be sure without knowing what you're trying to do exactly, but I don't think you need that "Node Directory" rule, and can rewrite your Init_Rules in that way:

rule Init_Alice:

[ Fr(~idThreadAlice) ] //

-->

[ St_Alice_1($Alice, $Bob, ~idThreadAlice) ]

Hope that helps,

Simon

--
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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/9f757555-4eb0-4359-a42c-5083da3f48c5n%40googlegroups.com.

[Guillaume Nibert]

Hello,

Thank you for your very clear answer. For Carol to be able to identify the message she is going to receive, I need to add tests, with pattern-matching, with or without the use of let... in... or restrictions with facts actions in the trace. Taking your comments into account, here is a modification to the theory:

---

theory AliceBobCarolInsecure

begin

// Each party get the identity of its predecessor and its successor

rule Init_Alice:

[ Fr(~idThreadAlice)]

-->

[ St_Alice_1($Alice, $Bob, ~idThreadAlice) ]

rule Init_Bob:

[ Fr(~idThreadBob)]

-->

[ St_Bob_1($Alice, $Bob, $Carol, ~idThreadBob) ]

rule Init_Carol:

[ Fr(~idThreadCarol) ]

-->

[ St_Carol_1($Bob, $Carol, ~idThreadCarol) ]

// Sending the cleartext message x

rule Alice_send_Bob:

[ St_Alice_1($Alice, $Bob, ~idThreadAlice)

, Fr(~x) ]

--[ Send_toBob(~x) ]->

[ Out(<$Alice, $Bob, ~x>), St_Alice_2($Alice, $Bob, ~idThreadAlice, ~x)]

rule Bob_receive_Alice_send_Carol:

[ St_Bob_1($Alice, $Bob, $Carol, ~idThreadBob)

, In(<$Alice, $Bob, x>) ]

--[ Recv_patternBobWants(x), Send_toCarol(x) ]->

[ Out(<$Bob, $Carol, x>), St_Bob_2($Alice, $Bob, $Carol, ~idThreadBob, x)]

rule Carol_receive_Bob:

[ St_Carol_1($Bob, $Carol, ~idThreadCarol)

, In(<$Bob, $Carol, x>) ]

--[ Recv_patternCarolWants(x) ]->

[ St_Carol_2($Bob, $Carol, ~idThreadCarol, x)]

lemma executable:

exists-trace

"Ex x #i #j #k #l. Send_toBob(x) @ i & Recv_patternsBobWant(x) @ j & Send_toCarol(x) @ k & Recv_patternCarrolWants(x) @ l & i < j & j < k & k < l"

end

---

And so in this case, should the Recv_patternBobWants fact action make sense? Bob does not know the message is from Alice, it could be, it could also be from the adversary, but it is in right format. If I want to check that it comes from Alice, I could use public key cryptography...

If I understand correctly, to model that a message is physically sent to Bob, I would have to change the channel model based on the information in the advanced_features section of the manual. For example, I could create an exclusive channel between Alice and Bob, and another exclusive channel between Bob and Carol, but thinking in that way I forget that I am up against a Dolev-Yao adversary...

So a question comes to mind: is it possible to model several adversaries in Tamarin who do not collude with each other, but who each have complete control of their network (e.g. the link (network 1) between Alice and Bob is controlled by adversary 1 and the link (network 2) between Bob and Carol is controlled by adversary 2, each adversary is omnipotent in the network they control)?

The theory seems to work, but Tamarin says "Loaded new theory! WARNING: ignoring the following wellformedness errors:" without specifying the errors. Do you have any idea how I could "debug" this?

Best regards,

Guillaume Nibert

[Simon BOUGET]

> Bob does not know the message is from Alice, it could be, it could also be from the adversary, but it is in right format. If I want to check that it comes from Alice, I could use public key cryptography...

Yes, exactly.

> If I understand correctly, to model that a message is physically sent to Bob, I would have to change the channel model

Yes. I'd try an Authentic Channel first, p.116.

> For example, I could create an exclusive channel between Alice and Bob

I'm not sure how you would do that, and I'm skeptical it would be an accurate representation of what you're trying to model, but hard to tell without more details.

Note that even if Alice and Bob use an Authentic Channel, it does not mean they have an exclusive channel. Anyone can use the authentic channel, and anyone will have the guarantee that messages received are really from who they appear to be from.

> thinking in that way I forget that I am up against a Dolev-Yao adversary...

Kinda yes, but that's not necessarily a problem. Dolev-Yao is a very powerful adversary, and in a lot of scenarios, it makes sense to add restrictions (such as more advanced channel rules) to what the default adversary can do. You have to loop back to the real system that you're trying to model and check what the real adversary can actually do in practice.

> is it possible to model several adversaries in Tamarin who do not collude with each other, but who each have complete control of their network

I don't think there is a straightforward way to model multiple adversaries. One possible work-around for what you describe: work with some form of secure channels and add separate adversary rules for each of the "networks", as recognized by who is sending the message initially. Then add a Restriction that adversary rules from different "networks" cannot be both executed in the same run.

In that case, you still have just 1 adversary, but you're sure it doesn't do an attack on both networks at once, so any attack found by Tamarin will be possible to execute for (at least) one of your "true" adversary that you're trying to model.

Maybe someone else can chime in with a better solution?

> without specifying the errors.

Usually, the errors follow on the next lines, if that's really the end of the message, that's really strange... No idea what could be happening.

Also, you seem to be forcing j<k, but in a "simple" run, you should have j=k, no?

Best,

Simon

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/aca22e3d-be59-4fe3-852a-cdb087b6ea54n%40googlegroups.com.

[Guillaume Nibert]

Hello,

Thank you very much for these valuable answers. Yes, it is j=k, I was wrong, thank you.
I still have a question about the graphs generated by Tamarin. Now let us suppose that Alice sends 2 encrypted messages to Bob and Carol.

The new associated theory is as follows:

--

theory AliceBobCarol

begin

builtins: symmetric-encryption

rule shared_symmetric_keys:

[ Fr(~key) ]

--[ KeyGeneration($A) ]->

[ !SessionKey(~key, $A) ]

rule Init_Alice:

[ Fr(~idThreadAlice)]

-->

[ St_Alice_1($Alice, $Bob, $Carol, ~idThreadAlice) ]

rule Init_Bob:

[ Fr(~idThreadBob)]

-->

[ St_Bob_1($Alice, $Bob, ~idThreadBob) ]

rule Init_Carol:

[ Fr(~idThreadCarol) ]

-->

[ St_Carol_1($Alice, $Carol, ~idThreadCarol) ]

rule Alice_send_Bob_Carol:

[ St_Alice_1($Alice, $Bob, $Carol, ~idThreadAlice)

, Fr(~x)

, Fr(~y)

, !SessionKey(~kAB, $Bob)

, !SessionKey(~kAC, $Carol)]

--[ Sent_Bob(~x, ~kAB), Sent_Carol(~y, ~kAC)]->

[ Out(<'1', $Alice, $Bob, senc(~x, ~kAB)>), Out(<'2', $Alice, $Carol, senc(~y, ~kAC)>), St_Alice_2($Alice, $Bob, ~idThreadAlice, ~x, ~y)]

rule Bob_receive_Alice:

let

x = sdec(encryption_x, ~kAB)

in

[ St_Bob_1($Alice, $Bob, ~idThreadBob)

, !SessionKey(~kAB, $Bob)

, In(<'1', $Alice, $Bob, encryption_x>) ]

--[ Reveived_BAlice(x, ~kAB) ]->

[ St_Bob_2($Alice, $Bob, ~idThreadBob, x)]

rule Carol_receive_Alice:

let

y = sdec(encryption_y, ~kAC)

in

[ St_Carol_1($Alice, $Carol, ~idThreadCarol)

, !SessionKey(~kAC, $Carol)

, In(<'2', $Alice, $Carol, encryption_y>) ]

--[ Received_CAlice(y, ~kAC) ]->

[ St_Carol_2($Alice, $Carol, ~idThreadCarol, y)]

lemma executable:

exists-trace

"Ex x y kac kab #i #j #k #l. Sent_Bob(x, kab) @ i

& Sent_Carol(y, kac) @ j

& Reveived_BAlice(x, kab) @ #k

& Received_CAlice(y, kac) @ l

& i < k

& j < l"

end

--

Why do I see 2 instances of the Alice_send_Bob_Carol rule with the Out('1'...) viewpoint and then the Out('2'...) viewpoint with a total of 4 Fr(~k) instances on the graph when I am only generating two keys? Is this related to this passage in the introduction (first paragraph) to the manual: "Tamarin can then be used to automatically construct a proof that, even when arbitrarily many instances of the protocol's roles are interleaved in parallel, together with the actions of the adversary, the protocol fulfils its specified properties. In this manual, we provide an overview of this tool and its use."?

Best regards,

Guillaume Nibert

[Guillaume Nibert]

I have just found it, it is the time constraint that I have added, I should modify my lemma in that way:

---

lemma executable:

exists-trace

"Ex x y kac kab #i #j #k. Sent_Bob(x, kab) @ i

& Sent_Carol(y, kac) @ i

& Reveived_BAlice(x, kab) @ j

& Received_CAlice(y, kac) @ k

& i < j

& i < k"

---

Thank you for all your help.

Best regards,

Guillaume Nibert

[Guillaume Nibert]

There is one final question I would like to ask about the following protocol:

Alice -> Bob: {msg}kAB
Bob -> Carol: {msg}kBC

where kAB is a shared symmetric key between Alice and Bob, and kBC a shared symmetric key between Bob and Carol.

Why does Carol receive a message from Alice/Adversary, why does Carol use !SessionKey(~kAB, $Bob) whereas what I have specified is !SessionKey(~kBC, $Bob)?

---

theory AliceBobCarol

begin

builtins: symmetric-encryption

rule shared_symmetric_keys:

[ Fr(~skey) ]

--[ KeyGen($A) ]->

[ !SessionKey(~skey, $A) ]

rule Init_Alice:

[ Fr(~idThreadAlice)]

-->

[ St_Alice_1($Alice, $Bob, ~idThreadAlice) ]

rule Init_Bob:

[ Fr(~idThreadBob)]

-->

[ St_Bob_1($Alice, $Bob, $Carol, ~idThreadBob) ]

rule Init_Carol:

[ Fr(~idThreadCarol)]

-->

[ St_Carol_1($Bob, $Carol, ~idThreadCarol) ]

// Alice -> Bob: {msg}kAB

rule Alice_send_Bob:

[ St_Alice_1($Alice, $Bob, ~idThreadAlice)

, Fr(~x)

, !SessionKey(~kAB, $Bob) ]

-->

[ Out(senc(~x, ~kAB)), St_Alice_2($Alice, $Bob, ~idThreadAlice, ~x)]

// Bob -> Carol: {msg}kBC

rule Bob_receive_Alice_send_Carol:

[ St_Bob_1($Alice, $Bob, $Carol, ~idThreadBob)

, !SessionKey(~kAB, $Bob)

, !SessionKey(~kBC, $Carol)

, In(senc(x, ~kAB)) ]

--[ Received_fromAlice($Alice, x) ]->

[ Out(senc(x, ~kBC)), St_Bob_2($Alice, $Bob, $Carol, ~idThreadBob, x)]

rule Carol_receive_Bob:

let

decryption = sdec(encryption, ~kBC)

in

[ St_Carol_1($Bob, $Carol, ~idThreadCarol)

, !SessionKey(~kBC, $Carol)

, In(encryption)]

--[ Received_fromBob($Bob, decryption) ]->

[ St_Carol_2($Bob, $Carol, ~idThreadCarol, decryption)]

lemma executable:

exists-trace

"Ex x Alice Bob #i #j. Received_fromAlice(Alice, x) @ #i & Received_fromBob(Bob, x) @ #j & i < j"

end

---

Best regards,

Guillaume Nibert

[Simon BOUGET]

One thing that is critical to understand is that you are not writing deterministic instructions for a program to execute, you are describing the rules of what is allowed. Then, the tool itself does whatever it "wants" inside those rules, not necessarily what you intend.

That's why you had two instances of the protocol in your previous question, you did not FORCE the tool to have only one Alice_send_etc. rule application, so when trying to find a run with the two "Receive" facts you requested in your lemma, the tool took the "simplest" route available: use a new Alice_send application to generate each Receive fact.

("want" and "simple" refer to the internal working of the tools and the heuristic it uses, and I don't want to get into the details; what's important to keep in mind from a user perspective is that you -purposefully- don't have direct control over that, the tools is in charge of picking a specific run, you just provide the general rules)

Similarly, in this new situation, you have nothing in your rule "Carol_receive_Bob" that forces the message to come from the same agent that executed the rule "Bob_receive_etc.". It is one possible execution of the protocol, for sure, but it's not the only one at all. And so the tool just picked the "simplest" one from its perspective.

Generally, when this kind of situations happen, it is because your rules are under-specified, and you have implicit assumptions that are not explicit in the specifications.

In the current situation, I think the likely issue is your init rules: there is nothing that indicates who is sharing which encryption keys with who.

In particular:

> why does Carol use !SessionKey(~kAB, $Bob) whereas what I have specified is !SessionKey(~kBC, $Bob)?

==> This name in the !SessionKey fact is not significant outside the Carol_receive_rule. The scope for a variable name is a single rule, to make sure that the same variable appearing in different Facts of the same rule hold the same value. But re-using the same name between different rules is not significant. It makes the specifications more readable/intuitive, but tends to "hide" implicit assumptions that are not actually enforced by the rules. Note how your shared symmetric keys are used: one is consumed 3 times, and the other only once, so it's not actually shared with anyone.

Best,

Simon

To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/e27ed736-fcaf-41e5-85b4-be3a2ad4192bn%40googlegroups.com.

[Guillaume Nibert]

Hello,

Thank you for all your help!

Best regards,

Guillaume Nibert