Automated Verification Of Cryptographic Protocol Implementations

When implementing systems using a secure data connection between components, it is important to analyze the security of data transmission. Secure data transfer is achieved by using cryptographic protocols. It is important to verify the security of cryptographic protocols already implemented in the system, since this is the last iteration of their compilation in the form of their implementation in the selected progranuning language. The paper proposes a scheme and approaches for creating an automated security verifier of cryptographic protocol implementations. The problems that arise when implementing cryptographic protocols in progranuning languages are described. A verification scheme based on the use of a source code analyzer for extracting the structure of cryptographic protocols, translating their structure of the Alice-Bob format protocol into the specification language for formal verifiers, and dynamic analysis of the implementation code is presented. The approaches for the implementation of the analyzer, translator and dynamic analyser are described, as well as the future work.