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