Формальный анализ протокола
Объект B получает сообщение 1: B
Ta,Na,
, откуда по формуле
получают:
B
Ta, Na; B
.
Учитывая предположения B
и B
, по правилу значения сообщений для общих секретов получают:
B
A
H(Ta, Na).
Откуда по правилу
получают:
B
A
Ta, Na.
Используя полученный результат и предположение B
#Ta, по правилу проверки нонсов получают:
B
A
Na.
Отсюда, используя правило полномочий и предположение B
A
Na, получают:
B
Na.
Таким образом, B аутентифицирует A.
Получив сообщение 2, A узнаёт, что B
Na, поэтому в идеализированном протоколе его следует изменить следующим образом: A
Na, Nb,
.
Из сообщения 2 по формуле
, получают:
A
Na, Nb; A
.
Учитывая предположения A
и A
, по правилу значения сообщений для общих секретов получают:
A
B
(H(Na, Nb), B
Na).
Откуда по правилу
. получают:
A
B
(Na, Nb, B
Na).
Используя полученный результат и предположение A
#Na, по правилу проверки нонсов получают:
A
B
Nb; A
B
Na.
Из выражения A
B
Na и предположения A
B
Nb по правилу полномочий получают:
A
Nb.
Последнее выражение фактически означает аутентификацию объекта B объектом A. Выражение A
B
Nb означает, что объект A узнаёт, что объект B его аутентифицировал.
Получив сообщение 3, B узнаёт, что A
Nb поэтому сообщение 3 в идеализированном протоколе следует изменить следующим образом: B
Nb,
.
Из сообщения 3 по формуле
, получают:
A
Nb; B
.
Учитывая предположение A
, по правилу значения сообщений для общих секретов получают:
B
A
(H(Nb, Na), A
Nb).
Откуда по правилу
получают:
B
A
(Nb, A
Nb).
Используя полученный результат и предположение B
#Nb, по правилу проверки нонсов получают:
B
A
Nb.
Последнее выражение означает, что объект B узнаёт, что объект A его аутентифицировал.
Содержание раздела
