1.      Теоретическая часть

Криптографические протоколы играют значимую роль в задаче защиты информации. Усилиями криптологов в разное время было создано большое количество криптографических протоколов различного назначения [2, 3]. Существует множество примеров, когда в, как казалось, уже хорошо изученных протоколах, обнаруживались ошибки. Так, например, ошибка, обнаруженная Деннингом и Сакко, в протоколе аутентификации Нидхема-Шрёдера, позволяет злоумышленнику выдавать старый, скомпрометированный сеансовый ключ за новый [2]. Очевидно, что во избежание такого рода ошибок, необходимо иметь возможность анализа протоколов формальными методами, позволяющими находить изъяны в криптографических протоколах. Одним из наиболее популярных и разработанных методов анализа протоколов является формальный анализ протоколов с применением методов BАN-логики.
BАN-логика [1] была предложенна Барроузом (Burrоws), Абади (Аbаdi) и Нидхамом (Nееdhаm) для анализа протоколов передачи ключей. BАN-логика состоит из набора кванторов возможных взаимных доверий участников (например, убеждение, что сообщение было послано неким другим участником), некоторого набора правил вывода для получения новых кванторов доверий из старых и набора модальных операторов, описывающих взаимосвязи между участниками и данными. Она включают в себя язык, который описывает различные утверждения о доверии и знании участников относительно сообщений, и некоторые правила вывода, которые используются для вывода новых утверждений из предыдущих.
Основная идея BАN-логики состоит в отслеживании восприятия сторонами поступающей информации, а именно, какие данные они принимают на веру, какие данные им точно известны и какие могут быть выведены логическим путем из достоверных для них фактов [2].
При использовании BАN-логики не моделируются ни различие между простым просмотром сообщения и пониманием его, ни пересмотр доверий, ни знание [1]. Все эти аспекты адресуются к неформальному отображению спецификации протокола в спецификацию BАN-логики, которое авторы называют идеализацией. Таким образом, анализу протокола предшествует его идеализация, которая производится человеком самостоятельно согласно описанию протокола. Идеализированные протоколы считаются более ясными и обладающими более полной спецификацией, чем традиционные описания. В терминах BАN-логики протокол рассматривается на абстрактном уровне, следовательно, ошибки конкретной реализации, такие как тупики или неправильное использование криптосистемы, при анализе не обнаруживаются. Методами BАN-логики анализируется непосредственно криптографический протокол, а используемые в нем криптографические методы считаются стойкими.
В настоящей работе будут рассмотрены основы BАN-логики: обозначения , основные постулаты и построение идеализированных протоколов.

Объекты BАN-логики

Перечислим объекты, которые различают в BАN-логике и укажем их обозначения.
-Участники протокола (обычно обозначаются А, B, S);
-Общие ключи (shаrеd kеys) шифрования, применяемые при симметричной криптографии, обозначаются где индексы в обозначении указывают на участников, использующих данных ключи.
-Открытые ключи (рubliс kеys), используемые при асимметричной криптографии, обозначаются (А, B, S – участники, которым принадлежат данные открытые ключи).
- – секретные ключи для соответствующих открытых ключей.
- – специальные числовые значения (нонсы, метки времени).
-X, Y – формулы и утверждения.
Конъюнкция – это единственная используемая логическая операция в BАN-логике, обозначается запятой. Свойства ассоциативности и коммутативности считаются доказанными.

Базовая система обозначений

Базовая система обозначений, принятая в BАN-логике, приведена в таблице 1.
Таблица 1 – Базовая система обозначений

Основные постулаты BАN-логики

При анализе протоколов аутентификации следует различать два времени: прошлое и настоящее. Настоящее время начинается со старта данного сеанса работы протокола. Все сообщения, посланные до этого, считаются старыми сообщениями, и в ходе работы протокола необходимо предотвращать возможность появления таких сообщений. Все веры, принятые в настоящем неизменны на протяжении всего сеанса работы протокола; более того действует следующее правило: что если участник Р заявляет утверждение Х, то он в действительности верит в Х. Однако те веры, которые были приняты в прошлом не обязательно должны быть переведены в настоящее. Такое простое разделение времени на прошлое и настоящее является достаточным для использования в BАN-логике.
Зашифрованное сообщение представляется как логическое утверждение, связанное с ключом шифрования и зашифрованное им. Если две отдельные зашифрованные части включены в одно сообщение, то они рассматриваются как два разных сообщения. Сообщение не может быть понято участником , который не знает ключ (или, в случае ассиметричной криптографии, участником, который не знает секретного ключа); ключ не может быть вычислен из зашифрованного сообщения.
Каждое шифрованное сообщение содержит избыточность, достаточную для того чтобы пользователь, расшифровывающий данное сообщение, имел возможность проверить, что он использовал правильный ключ. Кроме того, сообщения содержат информацию, необходимую пользователю, чтобы обнаружить и проигнорировать его собственные сообщения.
В таблице 2 перечислены основные правила вывода BAN-логики, используемые для получения новых утверждений и вер участников протокола. В постулатах использована запись вида , что означает, что так как утверждения А и В верны, то верно и утверждение С.
Таблица 2 – Основные правила вывода в BAN-логике

Правила значения сообщения (ПЗС) имеют отношение к интерпретации сообщений. Два первых правила позволяют интерпретировать шифрованные сообщения, а третье правило позволяет интерпретировать сообщения с секретами. Они все объясняют процесс получения верований о происхождении сообщений. В случае использования общих ключей правило означает, что если участник Р верит, что ключ K есть только у него и Q, и получает сообщение X, шифрованное на ключе K, то Р верит, что это Q прислал сообщение X. Чтобы данное правило имело смысл, необходимо гарантировать, что участник Р не послал сообщение X сам себе.
В случае использования общего секрета правило означает, что если пользователь Р верит, что секрет Y есть только у него и у пользователя Q, и получает то Р верит, что это пользователь Q прислал X. Эта формула основывается на том, что гарантирует, что не послано Р самому себе.
Перечислим еще несколько формул вывода, связанных с правилом значения сообщений:

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

где H(X) – функция хеширования.
Согласно правилу проверки нонсов (ППН), если участник P верит в свежесть утверждения X, заявленного Q, то Р верит и то, что Q верит в X. Это единственный постулат, который позволяет перейти от Это абстрактно отражается в практике разработчиков протоколов при использовании вызовов и ответов. Один участник протокола создает новое высказывание как вызов. Так как вызов был сгенерирован недавно, любое сообщение, его содержащее воспринимается как своевременное и рассматривается серьезно. Обычно, вызовы, в отличии от ответов на них , не нуждаются в зашифровании
Правило полномочий (ПП) указывает, что если Р верит, что Q создал утверждение X, и Р доверяет вере Q в X, то Р убеждён в истинности X. Необходимое свойство оператора веры – то, что Р верит набору инструкций, тогда и только тогда, когда Р верит каждой индивидуальной инструкции отдельно. Это выражается следующими правилами:

Аналогичные правила могут быть введены и для других операторов в случае необходимости. Например, рассмотрим подобное правило для оператора

Но стоит обратить внимание, что если и , то из этого не следует так как это подразумевало бы, что эти две части X и Y были произнесены в одно и то же время.
Если участник видит формулу, то он также видит ее компоненты, при условии что он знает необходимые ключи:

Первое правило во второй строке имеет место в соответствии с неявным предположением, что если Р верит, что K является его открытым ключом, тогда Р знает соответствующий секретный ключ . Обратите внимание, что, если то из этого не следует так как это значило бы, что X и Y были произнесены в то одно и то же время.
Если одна часть формулы является свежей, то целая формула тоже является свежей:
Другие подобные правила могут быть также выведены. Например, если X является свежим, тогда является свежим.
Если один и тот же ключ используется между парой участников в обоих направлениях, то следующи е два правила отражают это:

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

С помощью приведенных правил производятся доказательства в BАN-логике. Основными считаются постулаты, приведенные в таблице 2.
Формула X доказуема из формулы Y, если есть последовательность формул может быть получен из предыдущих с помощью правил. Как обычно, это может быть обобщено для доказательства схем.

Идеализация протокола

Как уже было сказано, перед непосредственным анализом протокола его необходимо представить в идеализированной форме. Для этого необходимо записать шаги протокола в терминах BAN-логики.
Обычно в литературе каждый шаг протокола записывается в виде символьной строки:
сообщение.
Такая запись означает, что участник Р посылает сообщение участнику Q, а Q получает это сообщение. Сообщение представляет собой строчку, содержащую различные данные.
Сообщение в идеализированном протоколе – это формула. Например, в описании протокола может быть такая символьная запись:

которая означает, что В получил сообщение от А. Сообщение зашифровано ключом связи участника В и доверенного сервера S, и содержит имя участника протокола А, а также ключ для связи участников А и В. Этот шаг может быть идеализирован как:

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

Цели протокола

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

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

а также уверенности каждого из них в том, что другой участник также верит в этот ключ:
Такие утверждения называют подтверждением приёма ключа. Т.е. в

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

Примеры анализа протоколов передачи ключей

Рассмотрим два примера анализа протоколов передачи ключей. Для записи исходного вида протокола используем стандартную символьную запись следующего вида:

Такая запись означает, что участник протокола А посылает, а участник В принимает сообщение состоящее из имени участника А и нонса зашифрованного ключом Буквенные обозначения продублируем из обозначений объектов BАN-логики.