Establishing and fixing security protocols weaknesses using a logic-based verification tool

Formal verification aims at providing a rigid and thorough means of evaluating the correctness of security protocols and also establishing that the protocols are free of weaknesses that can be exploited by attacks. This paper discusses the process of formal verification using a logic-based verification tool. The verification tool with attack detection capabilities is introduced, and the verification process is demonstrated by way of a case study on two published security protocols that provide mutual authentication using smart cards. The performed verification reveals new weaknesses in the protocols that can be exploited by a replay attack and a parallel session attack. The impact of these attacks is that an attacker is able to masquerade as a legitimate remote user to cheat the system. The reasoning why these attacks are possible is detailed and an amended protocol, resistant to these attacks is proposed. Formal verification of the amended protocol provides confidence in the correctness and effectiveness of the proposed modifications.