5G-AKA Partial Deconstruction (?)
felipecboeira
Hello all,
I am experimenting with the 5G-AKA model and I have been running into partial deconstructions during the interactive proof (as I understand from the green dashed arrow in the image below). I wonder what I could do given that Tamarin reports no partial deconstructions left (the GUI shows ‘refined sources deconstructions complete’). Would additional [sources] or [reuse] lemmas be required to avoid this situation? Or should ‘!KD’ goals be avoided altogether?
Thanks in advance!
Best regards,
Felipe
Ralf Sasse
Hello Felipe,
Once the GUI shows you that there are no more partial deconstructions left, you should not see any in the proofs you create. Additional [reuse] lemmas will certainly have no effect, additional [sources] lemmas can change the precomputation, but you would have no idea if it improved anything as it would still (at best) show that there are no partial deconstructions left.
However, in lemmas you should only ever use "K(..)" facts, for
which Tamarin gives guarantees. There are very few situations
(often involving sources lemmas) where you may want to use KU, but
never KD.
So, the screenshot you show surprises me if there really are no partial deconstructions left, but use of KD would explain that something weird happens. I thus recommend to change that, and expect the problem to be gone.
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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/6e368004-ff01-4c1e-91f5-58d769ad5556n%40googlegroups.com.
Jannik Dreier
Let me add some more explanation here: what you see in the graph is a
so-called "open chain", which means that Tamarin needs to work out if
and how the intruder could deduce the term at the bottom (here "f5(...)
XOR ...") from the protocol output at the top. These chains can appear
at many points during Tamarin's reasoning, and this happens even if
there are no partial deconstructions. Normally, they can be resolved as
we are looking pro a precise term, and should thus not be problematic
for the reasoning.
Technically, partial deconstructions are open chains which appear during
the precomputations. There Tamarin needs has less information about the
terms to deduce, hence he sometimes fails to resolve the chains, and we
end up with what is called "partial deconstructions".
To sum up: if you don't have partial deconstructions, open chains that
appear during the interactive proof are normally not a problem. (In your
example, did Tamarin manage to solve the open chains?) On the contrary,
if you have partial deconstructions, you will end up with many open
chains all the time, and this can be problematic.
Cheers,
Jannik
>>
>> Thanks in advance!
>>
>>
>> Best regards,
>>
>> Felipe
>>
>> --
>> 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
>> https://groups.google.com/d/msgid/tamarin-prover/6e368004-ff01-4c1e-91f5-58d769ad5556n%40googlegroups.com
> --
> 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
> <https://groups.google.com/d/msgid/tamarin-prover/5e43455e-7f01-58c0-c6d7-db6578efd499%40inf.ethz.ch?utm_medium=email&utm_source=footer>.
--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
felipecboeira
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/ade98479-edef-c33a-009d-79ba945d0841%40jannikdreier.net.