Question about the asymmetric-encryption example

[Ali S]

Hi everyone,

I have two basic questions regarding the asymmetric-encryption example provided in the Property Specification section of the tutorial (Pages 58, 59 in the PDF version).

First: What does "lemma secret_B" proves there? The proof shows that an adversary can inject a random value, and impersonate '$A'. The injected n is not secret and the adversary knows it. Is this a correct interpretation of the property and proof? If yes it does not prove that the protocol run does not provide message secrecy, but injection and impersonation is possible.

Second: Why the message secrecy property is not defined in a way that for all traces that A sends an encrypted message with the public key of B, the adversary cannot know the encrypted message?

I got a bit confused by breaking the secrecy of message from the perspectives of A and B.

Thank you for all your help and support,

Ali

[Marco Calipari]

Hey!

For question 1: Check out Lowe's hierarchy of authentication from his 1997 paper( 1997-lowe-hierarchy.pdf (computer.org)  ). It explains how authentication can be modelled  based on roles. The same idea applies to secrecy too. Basically, it says if a value n is secret and an agent claims to be in role 'A', ecc ecc.." You do this to avoid traces that, otherwise would not make sense

For question 2:

In Tamarin, we use action facts to support our lemmas, meaning we can't directly use asymmetric encryption objects for proofs. Instead, we state conditions like, "If a value n is claimed secret in all traces, then the adversary K cannot know n." This approach lets us specify under what conditions our security claims hold true.

This is how I interpreted the lemma, I hope this makes sense.
Best

[Ali S]

Thank you for your quick response,

I read the paper of hierarchy of authentication, and it makes sense for authentication. For authentication it is understandable that when agent B authenticates itself to agent A in a unilateral authentication, agent A can authenticate B and not the other way. But what does it mean for secrecy (Confidentiality)? B is not sending anything to A in that example (Pages 58, 59 in the PDF version), and the attack that the "lemma secret_B" shows is does not show that the message sent by A is compromised, but the adversary can inject a fresh message and that is not secret (If I understood the attack correctly). Does this lemma say that not all the messages received by agent B are unknown to the adversary?

Exactly, what I meant for question 2 was: Isn't it more accurate to write a secrecy lemma as follows for the protocol run:

lemma protocol_secrecy:
    // All traces wherein agent A sends a message to Agent B
    "All n #i #j. Secret(n) @i & Role('A') @i &
    // And agent B receives the message
     Secret(n) @j & Role('B') @j &
     // Order of protocol run
     i < j
     ==>
     // The adversary does not know the transmitted message
     (not (Ex #k. K(n)@k)) | (Ex B #k. Reveal(B)@k & Honest(B)@i)

Thank you!

[Simon BOUGET]

Hi Ali,

This part is indeed a bit tricky to understand at first. The key point that may be misleading is that the lemma "secret_B" is NOT a "serious" property that anyone would want to prove in the first place, it's just here in the manual to try and explain how lemmas work and show the difference between a valid lemma that can be proven and an invalid one with a counterexample.

> it does not prove that "the protocol run does not provide message secrecy", but "injection and impersonation is possible".

That's the idea, yes. But again, "secret_B" is not a serious property, it was not TRYING to prove "the protocol run does provide message secrecy". In fact, we DO know that the protocol provides secrecy, because that's what "secret_A" shows, that one is the "serious" version.

> Second: Why the message secrecy property is not defined in a way that for all traces that A sends an encrypted message with the public key of B, the adversary cannot know the encrypted message?

Yes, that's basically what "secret_A" means. It's just that the model in this example allows for a leak of the Ltk, so the rigorous property has to consider this possibility.

To be precise, "secret_A" translates to:

if A sends a secret n, then either the adversary never knows n, or B leaked their Ltk.

___

So why's "secret_A" the right way to show that, and why is "secret_B" wrong, with the tool finding a counterexample?

The way I like to look at it, the Action fact "Secret(n)" means "the agent executing this rule thinks that n is Secret". So in "secret_A", the first part translates to "when A thinks n is secret, then either...", and this makes sense because A is the source of the data, and the one who should be worried about secrecy.

But in "secret_B" on the other hand, the condition "when B thinks n is secret..." does not make any sense, B just received a message from the network, secrecy is not their problem, they should be worried about authentication (which is the very next section in the manual).

(Similarly, "Honest(X)" means "the agent executing this rule thinks that X is Honest", not that X is actually Honest.)

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/b2166655-ac88-4a7d-a492-661d8e56d732n%40googlegroups.com.

[Cas Cremers]

Hi all,

"secret_B" is definitely an extremely relevant property. It establishes the guarantee that a party executing the responder role gets about the secrecy of a value (which in this case was received). It is critical to formulate and verify such properties for each role of a protocol where that role may rely on the secrecy of a value later. If we were to consider a version of TLS 1.3, it is not immediately obvious to see whether a received value is secret, even if the peer was not compromised. Still, each role (notably B here) might use such a received value as a key to potentially encrypt sensitive values. Thus, verifying the property would be extremely critical.

In this particular case, I think that perhaps the confusion comes from the simplicity of the example. In this case, it is easy to see that B cannot rely on the received value being secret, even if it appears to be coming from an honest A, because the adversary can insert any message. For more complex protocols, this might be a much more intricate argument.

Fwiw, I do agree the "Honest(x)" here is not the most descriptive fact name, and we'll be updating this in the near future. The fact doesn't encode any assumption on the role execution -- rather, it is a bookkeeping fact to later formulate under which conditions the desired security property might hold. A clearer naming scheme would be to use "Peer(x)" and "Actor(x)" in the rule, and then to re-use these in the property to state that the value should be secret if the Peer/Actor was not compromised.

Best,

Cas