Open AccessPDA Language for Dynamic Analysis of Cryptographic Protocols
Author(s) -
Liudmila Babenko,
Ilya Pisarev
Publication year - 2020
Publication title -
voprosy kiberbezopasnosti
Language(s) - English
Resource type - Journals
ISSN - 2311-3456
DOI - 10.21681/2311-3456-2020-05-19-29
Subject(s) - computer science , cryptographic protocol , protocol (science) , replay attack , cryptography , cryptographic primitive , spectrum analyzer , process (computing) , programming language , computer security , authentication (law) , medicine , telecommunications , alternative medicine , pathology
Purpose of the article: development of an algorithm for dynamic analysis of the source codes of cryptographic protocols using the PDA language for the possibility of using your own attack models. Method: a source code generation method was used to simulate the attacker’s side when transmitting messages between legal parties according to the Dolev-Yao model. The method of false termination is also used, which is used in dynamic analysis and allows detecting attacks during simulation. Results: this paper presents the PDA language for dynamic analysis of the source codes of cryptographic protocols. An approach to dynamic analysis based on the principle of false termination is described. The process of modeling an active attack by an intruder is presented. The elements of the PDA language are described and an example of the description of the test protocol in this language is given. A test protocol in the C# programming language has been implemented. The effectiveness of the dynamic analysis was tested by simulating a replay attack. The security verification of the test cryptographic protocol was carried out using the well-known verification tools Scyther and Avispa. The comparison of the main indicators of the known means and the dynamic protocol analyzer proposed by the authors is carried out. The main advantages of the approach proposed by the authors are presented. The further direction of work is described.