DETECTION OF INFORMATION SYSTEM VULNERABILITIES BASED ON IDENTIFICATION AND AUTHENTICATION PROCEDURES

Abstract

The article investigates a critical aspect of cybersecurity—logical flaws in authentication mechanisms—that may result in severe vulnerabilities within access control systems. The focus is placed on a specific class of errors arising from incorrect formulation of credential verification logic, which can inadvertently allow unauthorized access. To illustrate this issue, the authors propose a formal model that encapsulates a common logical misconfiguration: authentication is granted if either a valid password is provided or the user identifier is missing. Such a condition, though seemingly benign, introduces a dangerous loophole that can be exploited by adversaries to bypass authentication entirely.

To rigorously analyze the security implications of this flaw, the model is subjected to formal verification using the ProVerif tool—a widely recognized framework for automated analysis of cryptographic protocols. ProVerif enables the simulation of various attack scenarios and the verification of key security properties such as confidentiality and authentication. The results of the analysis reveal that the flawed logic permits authentication bypass under certain conditions, confirming the presence of a vulnerability that could be exploited in real-world systems.

The findings underscore the importance of applying formal methods during the design and validation stages of security protocols. By modeling and verifying authentication logic before deployment, developers can identify and eliminate subtle errors that might otherwise compromise system integrity. The article advocates for the integration of formal verification tools into the development lifecycle of secure systems, emphasizing their role in enhancing resilience against logical attacks and ensuring robust access control.