Abstract
Security protocols are widely used to provide secure communication in many critical applications such as e-commerce and defense. Numerous formal methods have been used to ensure the desired working of security protocols. Formal methods provide rigorous analysis but are complex, whereas informal method are simple but lack the power to express the details of the analysis. Strand-space framework has become a popular formal method for analyzing security protocols due to its graph-theoretic nature. Benefiting from the expressiveness of this method and utilizing the intuitiveness of informal logical arguments, we propose a simplified generic approach based on a challenge-response criterion to discover man-in-the-middle attacks in authentication protocols.
Man-in-the-middle attacks result in discrepancies in the parameters among the participants of a protocol. To discover the possibility of man-in-the-middle attack on a protocol, we propose that each participant investigate the parameters of the other participants of the protocol by finding out the true originator of its received messages. With the help of an example, we demonstrate how the inability in finding out the true originator of a message guides us through a sequence of logical arguments eventually leading to a successful man-in-the-middle attack.