Find It With A Pencil: An Efficient Approach for Vulnerability Detection in Authentication Protocols

Smart devices improve the quality of life by collecting, analyzing, and transmitting data across different channels. Unfortunately, public media are prone to adversaries, and such devices must protect the privacy and confidentiality of users' data. Although authentication and key agreement protocols achieve the goal, they may suffer from hidden vulnerabilities; detecting them requires solid mathematical knowledge. Informal methods can discover protocol vulnerabilities, but most of them are limited to analyzing a specific protocol. Therefore, it is essential to provide a way for analyzing arbitrary ones. This paper proposes several algorithms to perform informal analyzes in O ( n ³ ×log( n )). Also, the article offers some ideas for optimizing these algorithms to achieve O ( n ² ), where n is the number of involved parameters in the protocol. Additionally, this paper introduces three graphical representations for vulnerability detection and examines their strengths and weaknesses. The compact version of such an expression has a better performance compared to the others. This method enables students with a weak mathematical background to analyze complex protocols on a piece of paper. The article explores four protocols published in recent years and describes how adversaries can obtain session keys in different scenarios.