Analysis of Russian key-agreement protocols using automated verification tools

We study several Russian key-agreement cryptographic protocols for compliance with specified security properties in view of possible adoption of these protocols as standardized solutions intended to be used in the Russian Federation. We have used a number of automatic cryptographic protocol verification tools available in the Internet such as Proverif, AVISPA-SPAN and Scyther, to simulate examined protocols. We find a number of vulnerabilities and propose ways to fix them.