Моделирование протокола взаимодействия tls на основе сети Петри при реализации защищенных соединений

УДК 004.056.53

МОДЕЛИРОВАНИЕ ПРОТОКОЛА ВЗАИМОДЕЙСТВИЯ ТЬ8 НА ОСНОВЕ СЕТИ ПЕТРИ ПРИ РЕАЛИЗАЦИИ ЗАЩИЩЕННЫХ СОЕДИНЕНИЙ

Ю.Ю. Громов, А.В. Яковлев, Ю.В. Минин, Е.О. Васюкова

Проведен анализ функционирования протокола безопасности транспортного уровня ТЬ8, что позволило выявить основные функциональные требования, предъявляемые к нему. Сетевая динамическая модель представлена вербально и формально с учетом особенностей реализуемого протокола, обсуждается алгоритм обработки клиентского запроса сервером. Приведено полное описание модели, включая описания позиций, переходов, начальной маркировки сети, а также дерево достижимости. Анализ свойств динамической модели помогает получить важную информацию о структуре и динамическом поведении моделируемой системы. В результате моделирования выявлено узкое место протокола, приводящее к задержкам в обслуживании и предложено решение его устранения

Ключевые слова: транспортный уровень, шифрование, хеш-функция, аутентификация

Стремительное развитие информационных технологий и быстрый рост глобальной сети Интернет привели к формированию информационной среды, оказывающей влияние на все сферы человеческой деятельности. Новые технологические возможности облегчают распространение информации, повышают эффективность производственных процессов, способствуют расширению деловых операций в процессе бизнеса .

Важным фактором, влияющим на развитие корпоративной информационной системы предприятия, является поддержание массовых и разнообразных связей предприятия через Интернет с одновременным обеспечением безопасности этих коммуникаций. Применение информационных технологий немыслимо без повышенного внимания к вопросам информационной безопасности. Ущерб от нарушения информационной безопасности может привести к крупным финансовым потерям и даже к полному закрытию компании. Поэтому одной из актуальных задач, которая стоит сегодня перед разработчиками и поставщиками информационных технологий, является решение проблем информационной безопасности, связанных с широким распространением Интернета, а также сетей intranet и extranet [1].

Объектом защиты информации является информационная сеть частного предприятия, имеющего главный центр в Москве и ряд информационных центров в ряде городов России. Доступ к корпоративным ресурсам осуществляется через виртуальную частную сеть VPN с удаленным доступом, которая позволяет объединить сотрудников, находящихся в командировках, «мобильных» сотрудников, мелкие информационные центры. По сети передается конфиденциальная информация, включающая в

Громов Юрий Юрьевич - ТГТУ, д-р техн. наук, профессор, e-mail: gromovtambov@yandex.ru, тел. (4752) 63-92-86

Яковлев Алексей Вячеславович - ТГТУ, канд. техн. наук, доцент, тел. (4752) 63-13-58

Минин Юрий Викторович - ТГТУ, канд. техн. наук, доцент, тел. (4752) 63-13-58

Васюкова Екатерина Олеговна - ТГТУ, студентка, тел. (4752) 63-13-58

себя сведения о заказчиках, производственную информацию, сведения о проектах и разработках, используемых ноу-хау. В связи с этим возникает необходимость защиты конфиденциальной информации.

Для шифрования информации, передаваемой между инициатором и терминатором соединения, будет осуществляться с помощью часто используемого для защиты транспортного уровня протокола TLS.

TLS (англ. TransportLayerSecurity - безопасность транспортного уровня) - криптографический протокол, обеспечивающий защищённую передачу данных между узлами в сети Интернет. TLS предоставляет возможности аутентификации и безопасной передачи данных через Интернет с использованием криптографических средств [2].

TLS-протокол основан на протоколе NetscapeSSL версии 3.0 и состоит из двух частей -TLSRecordProtocol и TLSHandshakeProtocol.

Протокол установления соединения (TLSHandshakeProtocol) используется при передаче сообщений, чтобы договориться, если это необходимо, о составе шифров от сервера к клиенту и от клиента к серверу и обменяться информацией, для того чтобы обеспечить криптографическую безопасность.

В течение этого handshake клиент и сервер принимают соглашение относительно параметров, используемых для установления защищенного соединения.

Последовательность действий при установлении TLS-соединения [2-4]:

• клиент подключается к серверу, поддерживающему TLS, и запрашивает защищенное соединение;

• клиент предоставляет список поддерживаемых алгоритмов шифрования и хеш-функций;

• сервер выбирает из списка, предоставленного клиентом, наиболее устойчивые алгоритмы, которые также поддерживаются сервером, и сообщает о своем выборе клиенту;

• сервер отправляет клиенту цифровой сертификат для собственной аутентификации. Обычно цифровой сертификат содержит имя

сервера, имя доверенного центра сертификации и открытый ключ сервера;

• клиент может связаться с сервером доверенного центра сертификации и подтвердить аутентичность переданного сертификата до начала передачи данных;

• для того чтобы сгенерировать сеансовый ключ для защищенного соединения, клиент шифрует случайно сгенерированную цифровую последовательность открытым ключом сервера и посылает результат на сервер. Учитывая специфику алгоритма асимметричного шифрования, используемого для установления соединения, только сервер может расшифровать полученную последовательность, используя свой закрытый ключ.

Моделирующие возможности сетей Петри и их эффективность в приложениях объясняются прежде всего тем, что сеть Петри - это интеграция графа и дискретной динамической системы, она может служить, таким образом, и статической, и динамической моделью представляемого с ее помощью объекта. Несомненным достоинством сетей Петри является математически строгое описание модели. Это позволяет проводить их анализ с помощью современной вычислительной техники [5].

Формальное описаниепротокола ТЬБ на основе аппарата сетей Петри выглядит следующим образом [5,6]:

1) конечное множество позиций:

Р = {Р1, Р2, Рз, Р4, Р5, Рб, Р7, Р8, Р9, Р11, Р12, Р13,

Р14> p15, Р1б p17, Р18 Р19> p20, Р21 p22, Р23 p24, p25, Р26 p27, Р28 Р29 Р30, Р31 p32, p33, p34, p35, Р3б p37, Р38 Р39 Р40, Р41, Р42, Рх1, Рх2}.

2) конечное множество переходов:

Т= {10 11, 12, 13, 14, 15, 1б 17, ¡8, ¡9, 1ю, 1ц, 112, 113, 114,

tl5, Ьб 117, 118, 119, 120ъ Ьь ^ 123, 124я 125, 12б}-

3) множество входных позиций перехода:

1={ 1(10), 1(11), 1(12), 1(13), 1(14), 1(15) ,1(1) 1(17) ,1(18), 1(19) ,1(110) ,1(111), 1(112), 1(113), 1(114) ,1(115) ,1(11б), 1(117), 1(118), 1(119), 1(120), 1(121), 1(122), 1(123), 1(124), 1(125), Щб) }

1(10)={Р1}, 1(11)={Р2,Р4}, 1(12)={Р5}, 1(13) = {Рб}, 1(14)={Р3, Р7}, 1(15)={Р8, Р11}, 1(1б)={Р9}, 1(17)={Р13}, 1(1ц)={Р12, Р14}, Ц19)={Р1б, Р17}, Ц110)={Р18}, Ц1ц> = {Р15, Р19}, 1(112)={Р21, Р22}, 1(113>={Р20}, 1(114)={Р23, Р24, Рх1, Рх2}, 1(115)={Р2б, Р27}, 1(11б)={Р25}, 1(117)={Р28}, 1(118)={Р29, Р30}, 1(119)={Р32}, 1(120)={Р33}, 1(121)={Р31, Р34}, 1(122)={Р3б}, 1(123)={Р35, Р37}, 1(124)={Р38}, 1(125)={Р41}, 1(12б)={Р42}-

4) множество выходных позиций перехода:

О = {0(1), 0(12), й(1з), 0(14), 0(15), 0(1б), 0(17),

0(18), 0(19), 0(110), 0(111), 0(112), 0(113), 0(114), 0(115), 0(11б), 0(117), 0(118), 0(119), 0(120), 0(121), 0(122), 0(123), 0(124), 0(125), 0(12б)}.

0(10)={Р3, Р4}, 0(1)={Р5}, 0(12)={Рб}, 0(13)={Р7, Р9}, 0(14)={Р8}, 0(15)={Р12}, 0(1б)={Р11, Р13}, 0(Ь)={Р14, Р17}, 0(1ц)={Р15, Р1б}, 0(19)={Р18},

0(1ю)={Р19, Р21}, 0(1ц)={Р20}, 0(112)={Р24},

0(113)={Р22, Р23}, 0(1Ы)={Р25, Р2б}, 0(115)={Р29},

0(11б)={Р27, Р28}, 0(1П)={Р30, Р31}, 0(1щ)={Р32},

0(119)={Р33, Р42}, 0(120)={Р34, Р3б}, 0(121)={Р35},

O(l22) = {p31, p39j, O(l23)={p38j, O(t24)=(p40, p4l},

O(l25)=(p1}, O(l26)={p2}.

5) начальная маркировка:

ц0 = {1, 1,0,0, 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0, 0,

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3,<х>}.

Содержание компонентов модели протокола TLS [2-4]

Обозн. элемента Описание Маркировка

pb p2 Начальное состояние Р {pi}=i, И {p2}=i

p3 Отправлен запрос на установление соединения

p4 Сообщение ClientHello

p5 Сообщение Cli-enffleИoпринято

p6 Характеристики соединения выбраны

p?

pi0 Подходящие характеристики соединения не найдены

pil

pi4 Запрос сертификата клиента

pi5 Сертификат клиента отправлен

pi6 Сообщение «Сертификат клиента»

pi7 Запрос сертификата клиента отправлен

pia Сертификат клиента получен

pi9

p22

p25(p26) Клиент (сервер) сгенерировал секретный ключ

p27 Сообщение ChangeCipherSpec

p2a

p30 Сообщение Finished

Продолжение таблицы

Р31 Сообщение Finished отправлено клиентом

Р32 (Р33) Сообщение Finished получено (расшифровано) сервером

Р34 Сообщение ChangeCipherSpec

Р35 Сообщение ChangeCipherSpec получено клиентом

Р36 Сообщение ChangeCipherSpec отправлено сервером

Р37 Сообщение Finished

Р39 Сообщение Finished отправлено сервером

P38 ( P40) Сообщение Finished получено (расшифровано) клиентом

Р41 Сообщение Finished не расшифровано клиентом

P42 Сообщение Finished не расшифровано сервером

Pxl Открытый ключ PreMasterSecret PiPxl}=1

Px2 Случайное число MiPx2}=™

to Отправить сообщение «ClientHello»

tl Получить сообщение «ClientHello»

t2 Выбрать нужные характеристики соединения

t3 Отослать сообщение "ServerHello"

t4 Получить сообщение «ServerHello»

t6 Отправить сертификат сервера

t5 Получить сертификат сервера

t7 Запросить сертификат клиента

t8 Отправить сертификат клиента

t9 Получить сертификат клиента

t10 Отправить сообщение " ServerHelloDone"

tll Получить сообщение " ServerHelloDone"

tl3 Отправить сообщение " ClientKeyExchange"

tl2 Получить сообщение " ClientKeyExchange"

t14 Сгенерировать секретный ключ

tl6 Отправить сообщение "ChangeCipherSpec"

tl5 Получить сообщение "ChangeCipherSpec"

tl7 Отослать зашифрованное сообщение "Finished"

tl8 Получить зашифрованное сообщение "Finished"

tl9 Расшифровать сообщение "Finished"

t20 Отправить сообщение "ChangeCipherSpec"

t21 Получить сообщение "ChangeCipherSpec"

t22 Отослать зашифрованное сообщение "Finished"

t23 Получить зашифрованное сообщение "Finished"

t24 Расшифровать сообщение "Finished"

t27 Разорвать соединение, т.к. подходящие характеристики не выбраны

Окончание таблицы

he Разорвать соединение, т.к. сервер не смог расшифровать сообщение "Finished"

t25 Разорвать соединение, т.к. клиент не смог расшифровать сообщение "Finished"

Рис. 1. Сеть Петри, моделирующая алгоритм работы протокола TLS

а) б)

Рис. 2. Граф достижимости для исходной модели протокола ТЬ8 и модифицированной строго сохраняющей модели протокола ТЬ8

Сеть Петри, моделирующая алгоритм работы протокола ТЬ8 представлен на рис. 1. Граф достижимости для исходной модели протокола ТЬ8 и модифицированной строго сохраняющей модели протокола ТЬ8 изображен на рис. 2.

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

Позиция сети Петри является безопасной, если число фишек в ней никогда не превышает 1. Сеть Петри безопасна, если безопасны все позиции сети.

В построенной с помощью аппарата сетей Петри модели протокола ТЬ8 есть позиции, которые небезопасны. Проблемный блок сети приведен на рис. 3.

б)

Рис. 3. Небезопасный участок модели протокола ТЬ8 и модифицированный безопасный блок генерации секретного ключа в модели протокола ТЬ8

На рис. 3 а небезопасными являются позиции рх1 (генерация открытого ключа РгеМаз1ег8ееге1) и рх2 (генерация случайного числа). Данные позиции можно сделать безопасными, разрешив пользователю генерировать открытый ключ РгеМаз1ег8ееге1 и случайное число только один раз за сеанс подключения. При ошибке генерации процесс соединения будет разорван и процедуру аутентификации придется начинать заново. Модифицированный блок генерации секретного ключа представлен на рис. 3б.

Анализ свойств построенной модели показывает, что сеть является активной и устойчивой, т.к. ни один переход сети не является тупиковым и возбуждение ни одного перехода не может быть снято срабатыванием другого какого-либо перехода. Также данная сеть обладает свойством достижимости, потому что из любого состояния можно достичь состояния 82 посредством последовательности переТамбовский государственный технический университет

ходов. Узким местом данной модели является переход t14 - генерация секретного ключа. Условия данного перехода всегда выполняются, но при определенных обстоятельствах возможно возникновение задержек в обслуживании данного компонента системы. Для решения этой проблемы предлагается использовать системы массового обслуживания, представляющие собой хорошо изученный и проверенный аппарат для работы в системах с предполагаемыми задержками в обработке задач.

Литература

1. Шаньгин В.Ф. Защита компьютерной информации. Эффективные методы и средства / В.Ф. Шаньгин. // М.:ДМК Пресс, 2008. - 544 с.

2. Семенов Ю.А. Протокол TLS версия 1.0. URLhttp://book.itep.ru/6/tls.htm (дата обращения: 10.09.2013).

3. T. Dierks, E. Rescorla. The Transport Layer Security (TLS) Protocol, Version 1.2 (August 2008). URLhttp://tools.ietf.org/html/rfc5246 Архивировано из первоисточника 9 февраля 2012.

4. E. Rescorla. Understanding the TLS renegotiation at-tack.EducatedGuesswork (5 ноября 2009). Архивировано из первоисточника 9 февраля 2012.

5. Питерсон Дж. Теория сетей Петри и моделирование систем: Пер. с англ. - М.: Мир, 1984. - 264 с.

6. Макущенко Я.О., Яковлева А.В. «Использование аппарата сетей Петри для моделирования протокола TLS». Сборник трудов Международной конференции «Актуальные проблемы прикладной математики, информатики и механики», 26-28 сентября 2011 г. - Воронеж: ИПЦ ВГУ, 2011. - с 283-289.

7. Махортов, С. Д. Алгебраический подход к исследованию и оптимизации баз знаний продукционного типа [Текст] / С. Д. Махортов, С. Л. Подвальный // Информационные технологии. - 2008. - № 8. - С. 55-60.

8. Подвальный, С. Л. Принципы разработки интеллектуальных систем моделирования [Текст] / С. Л. Подвальный, Т. М. Леденева, Е. С. Подвальный, А. Д. Поваляев, А. А. Маслак // Информационно-измерительные и управляющие системы. - 2013. - Т. 11. - № 8. - С. 025-030.

SIMULATION INTEROPERABILITY PROTOCOL TLS BASED PETRI NETS WHEN IMPLEMENTING SECURE CONNECTIONS

Yu.Yu. Gromov, A.V. Yakovlev, Yu.V. Minin, E.O. Vasjukova

The analysis of the functioning of the transport layer security protocol TLS, which allowed to identify the main functional requirements to it. Network dynamic model is presented verbally and formally taking into account features implemented protocol processing algorithm discussed client request server. We give a complete description of the model , including position descriptions , transitions , initial marking network and reachability tree . Analysis of the properties of the dynamic model helps to get important information about the structure and dynamic behavior of the modeled system. As a result of modeling the bottleneck protocol , leading to delays in service and provides a solution to eliminate it

Key words: transport layer encryption, hash function , authentication