Geodesic
Analysis of Russian key-agreement protocols using automated verification tools
Matematičeskie voprosy kriptografii, Tome 8 (2017) no. 2, pp. 131-142 
A. M. Semenov. Analysis of Russian key-agreement protocols using automated verification tools. Matematičeskie voprosy kriptografii, Tome 8 (2017) no. 2, pp. 131-142. http://geodesic.mathdoc.fr/item/MVK_2017_8_2_a10/
@article{MVK_2017_8_2_a10,
     author = {A. M. Semenov},
     title = {Analysis of {Russian} key-agreement protocols using automated verification tools},
     journal = {Matemati\v{c}eskie voprosy kriptografii},
     pages = {131--142},
     year = {2017},
     volume = {8},
     number = {2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MVK_2017_8_2_a10/}
}
TY  - JOUR
AU  - A. M. Semenov
TI  - Analysis of Russian key-agreement protocols using automated verification tools
JO  - Matematičeskie voprosy kriptografii
PY  - 2017
SP  - 131
EP  - 142
VL  - 8
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/MVK_2017_8_2_a10/
LA  - en
ID  - MVK_2017_8_2_a10
ER  - 
%0 Journal Article
%A A. M. Semenov
%T Analysis of Russian key-agreement protocols using automated verification tools
%J Matematičeskie voprosy kriptografii
%D 2017
%P 131-142
%V 8
%N 2
%U http://geodesic.mathdoc.fr/item/MVK_2017_8_2_a10/
%G en
%F MVK_2017_8_2_a10

Voir la notice de l'article provenant de la source Math-Net.Ru

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.

[1] Properties (Goals), http://www.avispa-project.org/delivs/6.1/d6-1/node3.html

[2] Cheremushkin A. V., Cryptographic protocols: basic properties and vulnerability, Publ. centre “Akademija”, 2009 (in Russian)

[3] Nesterenko A. Yu., “A new key agreement protocol based on Diffie–Hellman scheme”, Sistemy vysokoi dostupnosti, 8:2 (2012), 81–90 (in Russian)

[4] Nesterenko A. Yu., “On an approach to the construction of secure connections”, Mathematical aspects of cryptography, 4:2 (2013), 101–111

[5] Dolev D., Yao A. C., “On the security of public key protocols”, IEEE Trans. Inf. Theory, 29:2 (1983), 198–208 | DOI | MR | Zbl

[6] Blanchet B., “An efficient cryptographic protocol verifier based on Prolog rules”, Proc. 14th IEEE Computer Security Foundation Workshop (CSFW), 2009, 82–96

[7] Armando A. et al., “The AVISPA tool for the automated validation of Internet security protocols and applications”, Lect. Notes Comput. Sci., 3576, 2005, 281–285 | DOI | Zbl

[8] Cremers C. J. F., Scyther–Semantics and Verification of Security Protocols, Ph.D. Thesis, Eindhoven Univ. Technology, 2006

[9] Matyukhin D. V., On some properties of common key establishment schemes using infrastructure of public keys in a context of development of standardized cryptographic solutions, , 2011 (in Russian) http://www.ruscrypto.ru/accotiation/archive/rc2011/

[10] Nesterenko A. Yu., On a protocol of common key computation, , 2012 (in Russian) http://www.ruscrypto.ru/accotiation/archive/rc2012/

[11] Grebnev S. V., On the possibility of standardization of a key establishment protocol, , 2014 (in Russian) http://www.ruscrypto.ru/accotiation/archive/rc2014/

[12] Boyd C., Mathuria A., Protocols for Authentication and Key Establishment, Springer Science Business Media, 2003

[13] Cremers C., Mauw S., Operational Semantics and Verification of Security Protocols. Information Security and Cryptography, Springer, Heidelberg etc., 2012

[14] Lowe G., “A hierarchy of authentication specifications”, Proc. 10th IEEE Computer Security Foundation Workshop (CSFW), IEEE, Piscataway, CA, 1997, 31–44 | DOI