Анализ протоколов
Анализ протокола выполняется следующим образом:
1. Получение идеализированного протокола, производного от подлинника.
2. Написание предположений о начальном состоянии.
3. Добавление логических формул к утверждениям протокола, как суждений о состоянии системы после каждого утверждения.
4. Логические постулаты используют суждения и утверждения для обнаружения убеждений, полученных сторонами в ходе выполнения протокола.
Формальный анализ протокола
Объект B получает сообщение 1: B
B
Учитывая предположения B
B
Откуда по правилу
B
Используя полученный результат и предположение B
B
Отсюда, используя правило полномочий и предположение B
B
Таким образом, B аутентифицирует A.
Получив сообщение 2, A узнаёт, что B
Из сообщения 2 по формуле
A
Учитывая предположения A
A
Откуда по правилу
A
Используя полученный результат и предположение A
A
Из выражения A
A
Последнее выражение фактически означает аутентификацию объекта B объектом A. Выражение A
Получив сообщение 3, B узнаёт, что A
Из сообщения 3 по формуле
A
Учитывая предположение A
B
Откуда по правилу
B
Используя полученный результат и предположение B
B
Последнее выражение означает, что объект B узнаёт, что объект A его аутентифицировал.
Идеализация протокола
В идеализированной форме опускается часть сообщения, не относящаяся к доверию. Удаляются указатели, которые добавлены к реализации для своевременного выполнения процедур, но чье присутствие не затрагивает результата протокола, если каждый приёмник действует самопроизвольно. Например, можно опустить сообщение, использованное в качестве стартовой посылки, запускающей сеанс связи. Открытый текст опускается просто потому, что он может быть подделан.
Сообщение 1 A à B: Ta, Na,
Сообщение 2 B à A: Na, Nb,
Сообщение 3 A à B: Nb,
Описание протокола аутентификации
Описываемый протокол позволяет двум субъектам A и B аутентифицировать друг друга на основе общего секретного ключа аутентификации (СКА) и цифровых идентификаторов (DIa и DIb). До выполнения протокола участники должны знать значения цифровых идентификаторов друг друга и выработать общий секретный ключ аутентификации. Каждый субъект протокола должен иметь датчик случайных чисел для генерации нонсов, синхронизированные часы и алгоритм вычисления хэш-функции с ключом (H). Для защиты от атак повтора сообщений используются случайные последовательности – нонсы (Na и Nb). Отметка времени Ta
необходима для проверки приемлемости первого сообщения протокола. Символ úç в описании протокола означает операцию конкатенации.
1. Объект A:
- генерирует нонс Na;
- считывает с системных часов отметку времени Ta;
- вычисляет ha = HСКА(BúçAúçTaúçDIaúçNa);
- посылает B сообщение [BúçAúçTaúçNaúçha].
2. Объект B:
- получает от A сообщение [BúçAúçTaúçNaúçha];
- считывает отметку времени tb;
- проверяет условие |tb?Ta| < D;
- получает из базы данных цифровой идентификатор объекта A – DIa;
- проверяет условие ha
- если хотя бы одно из условий не выполняется, протокол разрывается; при выполнении этих условий B аутентифицирует A;
- генерирует нонс Nb;
- вычисляет hb = HСКА(AúçBúçDIbúçNaúçNb);
- посылает A сообщение [AúçBúçNaúçNbúçhb].
3. Объект A:
- получает от B сообщение [AúçBúçNaúçNbúçhb];
- сравнивает полученное значение нонса Na
с переданным;
- получает из базы данных цифровой идентификатор объекта B – DIb;
- проверяет условие hb
- если хотя бы одно из этих условий не выполняется, протокол разрывается; в случае выполнения этих условий A аутентифицирует B и узнаёт, что B аутентифицировал A;
- вычисляет ha2 = HСКА(BúçAúçNbúçNa);
- посылает B сообщение [BúçAúçNbúçha2].
4. Объект B:
- получает от A сообщение [BúçAúçNbúçha2];
- сравнивает полученное значение нонса Nb
с переданным;
- проверяет условие ha2
- если хотя бы одно из этих условий не выполняется, протокол разрывается; в случае выполнения этих условий B узнаёт, что A аутентифицировал B.
Постулаты BAN-логики
При анализе протоколов аутентификации следует различать два времени: прошлое и настоящее. Настоящее время начинается на старте работы изучаемого протокола. Все убеждения, имеющие место в настоящем, являются неизменными до завершения выполнения протокола; кроме того, допускается, что когда пользователь P заявляет X, то он действительно доверяет X.
Зашифрованное сообщение представляется как логическое утверждение, зашифрованное на ключе шифрования. Шифрованное сообщение не может быть расшифровано пользователем, не имеющим ключа. Ключ не может быть получен из шифрованного сообщения. Каждое шифрованное сообщение содержит избыточность достаточную, чтобы пользователь, расшифровывающий данное сообщение, имел возможность проверить, что он использовал правильный ключ. Кроме того, сообщения содержат информацию, необходимую пользователю, чтобы обнаружить и проигнорировать его собственные сообщения.
Правила значения сообщения имеют отношение к интерпретации сообщений. Два первых правила позволяют интерпретировать шифрованные сообщения, а третье правило позволяет интерпретировать сообщения с секретами. Они все объясняют процесс получения доверия о происхождении сообщений.
Для общих ключей формула выглядит следующим образом:
Если пользователь P верит, что ключ K есть только у него и Q, и получает сообщение X, шифрованное на ключе K, то P верит, что это Q прислал сообщение X. Чтобы данное правило имело смысл, необходимо гарантировать, что пользователь P не послал сообщение X сам себе.
Для общих секретов формула выглядит следующим образом:
Если пользователь P верит, что секрет Y есть только у него и у пользователя Q, и получает
Правило проверки нонсов:
Если пользователь P верит, что сообщение X является свежим и что его отправил пользователь Q, то P верит, что Q доверяет X. Для простоты, X должно быть открытым текстом и не должно включать никаких шифрованных подстрок.
Правило полномочий указывает, что если P верит, что Q создал утверждение X, и P доверяет Q, то P убеждён в истинности X:
Неизбежным свойством оператора доверия является то, что пользователь P верит ряду утверждений тогда и только тогда, когда он верит каждому отдельному утверждению. Это обосновывает следующие правила:
Другие аналогичные правила могут быть введены при необходимости.
Если пользователь получает сообщение, то он также получает все поля данного сообщения, если он знает необходимые ключи:
Предполагается, что пользователь P не послал сообщение X сам себе.
Если одна часть формулы является свежей, то целая формула тоже является свежей:
Можно написать и другие аналогичные правила. Например, можно показать, что если утверждение X является свежим, то
Для добавления понятия «хэш-функция» в BAN-логику вводится символ H для представления хэш-функций. Правило получения атрибутов авторства сообщения X из сообщения H(X) будет следующим:
Предположения
Для анализа протокола следует сделать следующие предположения.
A
A
A
A
A
B
Первые два предположения говорят о том, что объекты A и B доверяют общему ключу аутентификации СКА. Два следующих предположения описывают, что объекты A и B доверяют своим цифровым идентификаторам DIa и DIb соответственно. Следующие два предположения показывают, что объекты A и B доверяют цифровым идентификаторам других абонентов. Седьмое и восьмое предположения показывают, что объекты A и B сами генерируют свои нонсы. Девятое и десятое предположения говорят о том, что объекты A и B верят в свежесть сгенерированных ими нонсов. Последнее предположение предполагает использование синхронизированных часов, так как каждый объект должен проверять свежесть меток времени, сгенерированных другим объектом.
Проанализированный протокол аутентификации обеспечивает аутентификацию
1. Проанализированный протокол аутентификации обеспечивает аутентификацию объекта B объектом A и аутентификацию объекта A объектом B в ходе выполнения протокола.
2. Протокол содержит некоторую избыточность. В своей работе он использует следующие общие секреты:
- общий ключ аутентификации объектов – СКА;
- цифровой идентификатор объекта A – DIa;
- цифровой идентификатор объекта B – DIb.
Достаточно использовать лишь один из трёх перечисленных секретов. Использование одного секрета вместо трёх не ослабляет протокол, что можно показать с помощью логики. Значение хэш-функции в сообщении 3 вычисляется от нонсов Na и Nb. Достаточно вычислять значение хэш-функции только от Nb, что можно показать с помощью логики.
