Formalized Description of Message Encryption in Messaging Apps Using Automata Theory
Dmitry V. Pashchenko, Синев Михаил Петрович, Dmitry A. Trokoz, Alexey Ivanovich Martyshkin, Marina Veselova, Ksenia Zabrodina, Valeria Safronova, Ulyana Puchkova · 2019
This article describes the method of end-to-end encryption of messages in messaging apps using the automata theory, which are necessary for the visual representation of this mechanism. Interpretation of end-to-end encryption on event-driven non-deterministic automaton allows to implement these methods not only by software, but also by hardware. Since at present there is a high probability of loss and falsification of users personal data and storing the correspondence in a decrypted form on the network, such software methods of message encryption as symmetric and asymmetrical are used now; their distinctive features were described in this article. On the basis of these encryption methods, two protocols, which are the most reliable and frequently used in modern messaging apps, were considered. A serious vulnerability was found in one of the methods. It is missing in another protocol due to the use of Double Ratchet and triple Diffie-Hellman. This vulnerability was described in this article. In the protocols analysis, the Diffie-Hellman algorithm and the AES-256 standard were detailed. The AES-256 standard is represented by a form of mathematical model using the automata theory, on the basis of which a hardware implementation of the encryption mechanism is possible.