Постулаты BAN-логики
         

Формальный анализ протокола


Объект 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 его аутентифицировал.



Содержание раздела