Re: [tamarin-prover] error result about Observational_equivalence

[Ralf Sasse]

As is well known, the observational equivalence mode is sound, meaning all proofs are real, however, it is not necessarily complete, i.e., attacks may be false.

In your case, you have run into this, and if you are sure the attack is false, then you do not know whether the property holds or not. You only know that in the way you have modeled it, Tamarin won't be able to prove it. Tamarin might be able (with manual exploration or heuristics or oracles) to construct another attack which would be real. So, you truly do not know if the property holds or not.

Cheers,
Ralf

On 23.10.24 10:31, hua hua wrote:

When I proved the Observational Equivalence, Tamarin found an attack, but after reviewing the attack path, I realized it is not a real attack. Below are the source code ,the attack code and the image of the attack path. Could this be a bug in Tamarin
--
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/b45ef1e6-db40-4c04-87b1-e146cb9c9c18n%40googlegroups.com.

[hua hua]

Thank you for your response. If I want to prove the unlinkability of the AKA protocol, meaning the result is true, how should I modify the modeling? The modeling code is referenced from `develop/examples/ccs18-5G/5G-AKA-untraceability/5G_AKA_simplified_privacy_active.spthy`. Could you can help me identify the issues in the modeling. The code is the attachment of the above "privacy.spthy."   I look forward to your reply.

[hua hua]

Thank you for your response. If I want to prove the unlinkability of the AKA protocol, meaning the result is true, how should I modify the modeling? The modeling code is referenced from `develop/examples/ccs18-5G/5G-AKA-untraceability/5G_AKA_simplified_privacy_active.spthy`.Could you help me identify the issues in the modeling. The code is the attachment of the above "privacy.spthy." I look forward to your reply.

在2024年10月23日星期三 UTC+8 18:39:57<Ralf Sasse> 写道：