Questions regarding KD and KU facts

[justin]

Hi all, I am fairly new to Tamarin and I'm trying to understand the verification theory behind it. 

1. Why is the action fact K(x) in the isend rule and not irecv?

2. What is the purpose of the coerce rule? I understand it's to allow the adversary to change a KD tagged fact to a KU tagged fact, but is there a more intuitive reason?

2. Why is the key in the deconstruction rule for decryption tagged KU instead of KD? Or more generally, why is only the first premise fact a KD fact and the other facts KU facts?
     My understanding is that the other premises facts, which are arguments to the first premise fact, needs to have been constructed by the adversary or derived from a message sent by the protocol via the coerce rule?

Thanks,
Justin

[Felix Linker]

Hi Justin,

Tamarin uses a specific type of reasoning about adversary knowledge to avoid infinite loops. The idea is the following: The adversary first collects all messages they received. Then, using „destruction rules“ (KD-related where D stands for „down“) they extract the smallest terms they can learn from these messages. For example, if the adversary receives a tuple <a, b>, they learn a and b. If they receive send(m, k), they only learn that term (unless they know k, then they also learn m). Finally, using „construction rules“ (KU-related where the U stands for „up“) the adversary combines all these smallest terms to larger terms which then make up the adversary knowledge. The coerce rule simply passes the boundary from KD to KU, and it only works this way to avoid loops.

The K fact simply expresses adversary knowledge, thus, it comes from KU. Tamarin’s built-in rules never use K facts (afaik), so K only appears when you reference it in a lemma yourself.

I hope this answers all your questions!

Cheers,

Felix

--
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/4768c836-9745-4055-886a-2d46d35e040an%40googlegroups.com.