10.14489/vkit.2015.07.pp.023-028

DOI: 10.14489/vkit.2015.07.pp.023-028

Борхаленко В. А.
АВТОМАТНАЯ МОДЕЛЬ НАРУШИТЕЛЯ ДЛЯ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ ИНФОРМАЦИОННОГО ОБМЕНА
(с. 23-28)

Аннотация. Рассмотрена расширенная модель нарушителя Долева–Яо с использованием тактик различных атак. С помощью автоматов Бюхи приведены короткое математическое описание и пример использования данной модели нарушителя для проверки свойств безопасности криптографического протокола SSL (Secure Sockets Layer) на основе метода Model Checking.

Ключевые слова: модель Долева–Яо; математическое моделирование; метод верификации на моделях; криптографические протоколы; информационная безопасность.

Borhalenko V. A.
THE AUTOMATA INTRUDER MODEL FOR DATA EXCHANGE CRYPTOGRAPHIC PROTOCOLS FORMAL VERIFICATION
(pp. 23-28)

Abstract. In this article the expanded Dolev–Yao model of intruder with additional requirements to intruder’s possibilities is described. It is assumed that the intruder can use the well-known attack tactics like man in the middle, replay or DoS and knows the protocol. The brief formal description of the attack models is given using Buchi state machines. The safety and liveness system options applied to cryptographic protocols are formalized using the LTL (Linear Temporal Logic). Also we show in the article the Buchi state machines that allow all ω-words on which are feasible the negations of the LTL formulas described above. We use the SPIN system as a tool for modeling and verifying SSL (Secure Sockets Layer) protocol. The example of applying the expanded intruder model for SSL security properties verification using model checking method is given in this report. Also the article contains the results of the SSL specifications verification and traces that lead to insecure states.

Keywords: Dolev–Yao model; Mathematical modeling; Model checking; Cryptographic protocols; Information security.

+ - Информация об авторах (About the Authors) Click to collapse

Рус

В. А. Борхаленко (Национальный исследовательский университет «Московский энергетический институт») E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

Eng

V. A. Borhalenko (National Research University “Moscow Power Engineering Institute”) E-mail: Этот e-mail адрес защищен от спам-ботов, для его просмотра у Вас должен быть включен Javascript

+ - Библиографический список (References) Click to collapse

Рус

1. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных систем. СПб.: БХВ-Петербург, 2010. 560 c.
2. Косачев А. С., Пономарева В. Н. Анализ под-ходов к верификации функций безопасности и мобиль-ности. М.: ИСП РАН, 2004. 101 c.
3. Мао В. Современная криптография: теория и практика: пер. с англ. М.: Вильямс, 2005. 763 c.
4. Powell J. D. Model Checking for Software Security Properties [Электронный ресурс]. URL: http://trs-new. jpl.nasa.gov/dspace/bitstream/2014/7143/1/03-0769.pdf (дата обращения: 10.05.2015).
5. Maggi P., Sisto R. Using Spin to Verify Security Properties of Cryptographic Protocols // SPIN of Lecture Notes in Computer Science. 2002. V. 2318. P. 187 – 204.
6. Henda N. B. Generic and Efficient Attacker Models in SPIN [Электронный ресурс]. URL: http://spinroot. com/spin/Workshops/ws14/spin20140_submission_18.pdf (дата обращения: 10.05.2015).
7. Нестеров С. А. Информационная безопасность и защита информации. СПб.: Изд-во Политехн. ун-та, 2009. 125 c.
8. Давыдов А. Н. Атаки на протоколы установле-ния ключа [Электронный ресурс] // Безопасность инфор-мационных технологий: тр. науч.-техн. конф. 2004. С. 99 – 104. URL: http://пниэи.рф/activity/science/BIT/T5.pdf (дата обращения: 05.01.2015).

Eng

1. Karpov Iu. G. (2010). Model checking. Verification of parallel and distributed systems. St. Petersburg: BKhV-Peterburg.
2. Kosachev A. S., Ponomareva V. N. (2004). Analysis of approaches to the verification of security and mobility functions. Moscow: ISP RAN.
3. Mao V. (2005). Modern cryptography: theory and practice. Moscow: Williams.
4. Powell J. D. Model checking for software security properties. Available at: http://trs-new. jpl.nasa.gov/dspace/bitstream/2014/7143/1/03-0769.pdf (Accessed: 10.05.2015).
5. Maggi. P., Sisto R. (2002). Using spin to verify se-curity properties of cryptographic protocols. SPIN of Lecture Notes in Computer Science, 2318, pp. 187-204. doi: 10.1007/3-540-46017-9_14
6. Henda N. B. Generic and efficient attacker models in SPIN. Available at: http://spinroot. com/spin/Workshops/ws14/spin20140_submission_18.pdf (Accessed: 10.05.2015).
7. Nesterov S. A. (2009). Information security and da-ta protection. St. Petersburg: Izdatel'stvo Politekhnicheskogo universiteta.
8. Davydov A. N. (2004). Attacks on protocols for key establishment. Security of information technologies: pro-ceedings of the scientific and technical conference, pp. 99 – 104. Available at: http://пниэи.рф/activity/science/BIT/T5.pdf (Accessed: 05.01.2015).

+ - Заказать электронную версию статьи (Purchase digital version of a single article) Click to collapse

Рус

Статью можно приобрести в электронном виде (PDF формат).

Стоимость статьи 350 руб. (в том числе НДС 18%). После оформления заказа, в течение нескольких дней, на указанный вами e-mail придут счет и квитанция для оплаты в банке.

После поступления денег на счет издательства, вам будет выслан электронный вариант статьи.

Для заказа статьи заполните форму:

{jform=1,doi=10.14489/vkit.2015.07.pp.023-028}

Eng

This article is available in electronic format (PDF).

The cost of a single article is 350 rubles. (including VAT 18%). After you place an order within a few days, you will receive following documents to your specified e-mail: account on payment and receipt to pay in the bank.

After depositing your payment on our bank account we send you file of the article by e-mail.

To order articles please fill out the form below:

{jform=2,doi=10.14489/vkit.2015.07.pp.023-028}