5. В an-логика

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

Существует четыре основных подхода к анализу криптографических протоколов [233]:

1) моделирование и проверка работы протокола с использованием языков описания и средств проверки, не разработанных специально для анализа криптографических про­токолов;

2) создание экспертных систем, позволяющих разработчику протокола исследовать раз­личные сценарии;

3) выработка требований к семейству протоколов, используя некую логику для анализа понятий «знание» и «доверие»;

4) разработка формальных методов, основанных на записи свойств криптографических систем в алгебраическом виде.

Первый из подходов пытается доказать правильность протокола, рассматривая его как обычную компьютерную программу. Ряд исследователей представляют протокол как конеч­ный автомат [203,204], другие используют расширения методов исчисления предиката пер­вого порядка [205], а третьи для анализа протоколов используют языки описания [206]. Од­нако доказательство правильности отнюдь не является доказательством безопасности, и этот подход потерпел неудачу при анализе многих уязвимых протоколов. И хотя его применение поначалу широко изучалось, с ростом популярности третьего из подходов работы в этой обла­сти были переориентированы. Во втором подходе для определения того, может ли протокол перейти в нежелательное состояние (например, потеря ключа), используются экспертные системы. Хотя этот подход дает лучшие результаты, он не гарантирует безопасности и не предоставляет методик разработки атак. Он хорош для проверки криптостойкости протоко­ла по отношению к конкретной атаке, но не более. Примеры такого подхода можно найти в [48,207], а в [208] обсуждается экспертная система Interrogator. Третий подход гораздо популярнее. Он был впервые введен Бэрроузом (М. Burrows). Абади (М. Abadi) и Нидхэмоы (R.M. Needham). Они разработали формальную логическую модель для анализа знания и доверия, названную BAN-логикой [209,210]. BAN-логика широко используется при анализе протоколов аутентификации. Она рассматривает подлинность как функцию от целостности и новизны, используя логические правила для отслеживания состояния этих атрибутов на протяжении всего протокола. Хотя были предложены различные варианты, большинство разработчиков протоколов до сих пор обращаются к оригинальной работе. BAN-логика не предоставляет доказательство безопасности, она может только рассуждать о проверке под­линности. Она является простой, прямолинейной логикой, легкой в применении и полезной при поиске уязвимых мест в протоколе. Вот некоторые положения BAN-логики:

• Алиса верит X (Алиса действует, как если бы X являлось истиной.);

• Алиса знает X (Кто-то послал сообщение, содержащее X, Алисе, которая может про­читать и снова передать X — возможно, после дешифрования.);

• Алиса выдает X (В некоторый момент времени Алиса послала сообщение, которое со­держит предложение X. Не известно, как давно было послано сообщение и было ли оно послано в течение текущего исполнения протокола. Известно, что Алиса доверяла Х_} когда выдавала Х.)

• X ново (X никогда не было послано в сообщении до текущего выполнения протокола.).

BAN-логика также предоставляет правила для рассуждения о доверии протоколу. Для доказательства чего-либо в протоколе или для ответа на какие-то вопросы к логическим предложениям о протоколе можно применить эти правила. Например, одним из правил яв­ляется правило о значении сообщения (конструкция вида ЕСЛИ ..., ТО ... ):

• ЕСЛИ Алиса верит, что у Алисы и Боба общий секретный ключ К и Алиса знает X, зашифрованное на К, но при этом Алиса не шифровала X с помощью К, ТО Алиса верит, что Боб выдал X.

Другое правило — правило подтверждения метки времени:

• ЕСЛИ Алиса верит, что X могло быть выдано только недавно и что Боб когда-то выдал X, ТО Алиса верит, что Боб верит X.

BAN-анализ делится на четыре этапа:

1) использование положений и правил BAN-логики для приведения описания протокола к стандартной форме:

2) добавление всех положений о начальном состоянии протокола;

3) присоединение логических формул к положениям с целью получения утверждений о состоянии системы;

4) применение логических постулатов к утверждениям и положениям для раскрытия со­стояние доверия участников протокола.

Авторы утверждают, что BAN-логика позволяет получить ясное и полное описание прак­тического протокола. Другие исследователи не так оптимистичны и пытаются показать, что BAN-логика может привести к получению неправильных характеристик протоколов |211,212). Несмотря на критику, при помощи BAN-логики удалось доказать уязвимость некоторых про­токолов, включая первичную версию протоколов стандарта Х.509 |213], а также избыточность ряда практических протоколов аутентификации, например Kerberos. Во многих опубликован­ных работах BAN-логика используется для заявления претензии на безопасность предлагае­мых протоколов [214-216]. Были опубликованы и другие логические системы, некоторые из них разрабатывались как расширения BAN-логики (217-220).

Четвертый подход к анализу криптографических протоколов предлагает моделировать протокол как алгебраическую систему, выразить знания участников о протоколе и затем про­анализировать достижимость определенных состояний. Этот подход пока не привлек столько внимания, как формальная логика, но положение дел постепенно меняется. Анализатор протоколов Исследовательской лаборатории ВМС (Navy Research Laboratory, NRL), возможно, является наиболее успешным применением этих методов [228-231]. Он был использован для проверки множества протоколов [201,232,233]. Анализатор протоколов определяет следующие действия:

- принять (Боб, Алиса, М, N) (Боб принимает сообщение М как пришедшее от Алисы в течение локального раунда N.);

- узнать (Ева, М} (Ева узнает М.);

- послать (Алиса, Боб, Q, М) (Алиса посылает М Бобу в ответ на запрос Q.)

- запросить (Боб, Алиса, Q, N) (Боб посылает Q Алисе в течение локального раунда N.). Используя эти действия, можно задать требования. Например:

- если Боб принял сообщение М от Алисы в какой-то прошедший момент времени, то Ева не знает М в какой-то прошедший момент времени;

- если Боб принял сообщение М от Алисы в течение локального раунда N, то Алиса послала М Бобу в ответ на запрос Боба в течение локального раунда N.

Для анализа при помощи NRL исследуемый протокол должен быть описан в терминах приведенных конструкций. Затем выполняется четыре фазы анализа: определение правил перехода для честных участников, описание операций, возможных и для полностью чест­ных, и для нечестных участников, описание базовых блоков протокола и описание правил преобразования. Смысл всего этого заключается в том, чтобы показать, что данный прото­кол удовлетворяет необходимым требованиям. Использование инструментов, подобных NRL, в итоге могло бы привести к созданию протокола, который был бы обоснованно признан безопасным. Хотя формальные методы в основном применяются к уже существующим про­токолам, наметилась тенденция их использования и при проектировании протоколов. Ряд предварительных шагов в этом направлении уже сделан в [200].