observational issue

[hua hua]

When using Tamarin to prove Observational Equivalence, I encountered an infinite loop while trying to prove the XOR operation and couldn't escape it(Using the sent XOR messages to continuously construct new XOR messages). What should I do? Below, I have provided the minimal example along with images

.

[hua hua]

Dear all,

May be my description above is not clear,below is the specific example and description.

there are two ues and one sn, ue and sn has the shared key k.

protocol:
    ue sends supi(ue's identify) sysmmetric encryption by k to sn
    sn sends autn(ak xor hnmac)
The problem is when proving Observational_equivalence about Rule_Destrd_xor,it will not terminate.
By manual researching,i find it is because there are many sns that can send autn,the attacker can use autn

to build new term,it seems endless!

the code is attached,if you have any questions ,do not hesitate to ask me! I am looking forward to your reply.