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
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.
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.