AKA-Protocol-unlinkability #84
Description
To the best of my knowledge, the 3G AKA protocol does not possess unlinkability. An attacker can exploit different failure messages, such as MAC_Failure and SQN_Failure, to carry out a linkability attack. However, when I executed the files in /examples/trace_equivalence/3G-AKA-protocol/unlinkability, I did not find any linkability attacks. Is this due to the modeling approach, or is it because the current tool is unable to detect such attacks?