<< Предыдущая

стр. 27
(из 82 стр.)

ОГЛАВЛЕНИЕ

Следующая >>


6.2.5. Цербер
Закончим параграф рассмотрением Цербера, системы аутентифи­
кации, основанной на симметричном шифровании с помощью цен­
тра аутентификации. В его основу легли идеи протокола Нидхейма-
Шредера. Цербер разработан в Массачуссетском технологическом
институте (MIT) в 1987 г. как часть проекта «Афина». Модифици­
рованная версия этого протокола используется в операционной си­
стеме Windows 2000.
Предполагается, что компьютерная сеть состоит из клиентов и
сервера, причем клиентами могут быть пользователи, программы
или специальные службы. Цербер хранит центральную базу данных,
включающую как клиентов, так и их секретные ключи. Таким обра­
зом, если в систему входит п клиентов, размер пространства ключей
должен иметь порядок 0{п), Цель Цербера состоит в идентифика­
ции клиентов и генерировании для них сеансовых ключей.
Кроме того. Цербер может служить системой предоставления
доступа к различного вида услугам и ресурсам. Разделение функ­
ций идентификации и предоставления доступа — хорошая идея, с
которой мы будем разбираться позже, знакомясь с SPKL Такое
разделение отражает обычное положение д,ел в реальных фирмах.
Действительно, персонал одного отдела, например, устанавливает
Вашу личность, в то время как другой отдел проверяет Ваш уро­
вень доступа к ресурсам компании. Такое же разделение функций
присутствует и в системе Цербер, где имеется центр идентифика­
ции и сервер генерирования сертификатов (TGS — ticket generation
server), который выдает сертификаты (разрешения) на доступ к ре­
сурсам: файлам, принтерам, и т. д.
Глава 6. Распределение симметричных ключей

Предположим, клиент А хочет воспользоваться ресурсами кли­
ента В, Тогда он заходит на сервер аутентификации, используя свой
пароль. Сервер выдает ему сертификат, зашифрованный с помощью
этого пароля. Сертификат, в частности, содержит сеансовый ключ
kas- Клиент А применяет ключ kas А,л.я получения следующего сер­
тификата, разрешающего доступ к ресурсам клиента В. Последний
сертификат состоит из ключа каь^ времени его жизни / и временной
метки tg. Выданный сертификат используется для «удостоверения
личности» А в последующем обращении к В. Обмен информацией в
системе Цербер представлен ниже (рис. 6.4):

3:{ts,l,kab.aL,fa,ta}. 1:А,В
доверенное
Боб Алиса
' лицо
4:{ta+n 2: {ts,l.kab,b,{ts.l,kab,a}kjk.


Р и с . 6 . 4 . Цербер

А —>S:A,B,
^ >Л: {ts^^kab-^O^ \^si4kab^CL\kbs\kas'>

А —> В : {ts,l,kab,a}kbs, {(^^ta}kab^
В-^А: {ta^l}kab-
- в первом обращении клиент А сообщает 5, что он хотел бы
связаться с В.
- Если S разрешает эту связь, то создает сертификат {t^, /, каЬ', «j^
зашифрованный ключомfc^^,и отсылает его А для передачи В,
Пользователь А получает копию этого ключа в той форме,
которую он может прочесть.
- Клиент Л, желая проверить действенность сертификата и свою
возможность воспользоваться ресурсами 5 , посылает заши­
фрованную временную метку ta участнику В,
- Клиент В отсылает назад зашифрованную величину ^а + 1,
проверив, что временная метка является свежей, показывая
тем самым, что он знает сеансовый ключ и готов к связи.
В этом протоколе устранены недостатки, присущие протоколу Нид-
хейма - Шредера, но за счет обязательной синхронизации часов.


6.3. Формальные методы проверки протоколов
Из обсуждения протоколов в предыдущем параграфе можно сделать
вывод, что они весьма запутанны, и выявление их недостатков ока-
6.3. Формальные методы проверки протоколов

зывается довольно тонким делом. Чтобы подойти к этой задаче с
научной точки зрения, необходимо разработать соответствующий
аппарат. Наиболее сильный из них — БЛТУ-логика, изобретенная
Барроузом, Абади и Нидхеймом.
БЛЛГ-логика, как и любая формальная логика, имеет ряд недо­
статков, но она была в свое время очень полезна при проектиро­
вании и анализе протоколов распределения симметричных ключей
типа Цербер и Нидхейма-Шредера. В настоящее время она вытесне­
на более сложной техникой и формальными методами, но сохраняет
свое значение как с исторической, так и с учебной точек зрения.
Основная идея ВАМ-лотжки. состоит в том, что при анализе про­
токолов в первую очередь стоит обратить внимание на восприятие
сторонами поступающей информации — что они принимают на ве­
ру, а что им доподлинно известно или может быть выведено логи­
ческим путем из достоверных для них фактов. Даже при современ­
ных подходах к моделированию инфрасруктуры открытых ключей
{PKI) берут на вооружение эту идею, в связи с чем мы сейчас ис­
следуем BAN-лотшау более подробно.
Введем обозначения.
˜ Р\ = X означает, что участник Р верит в (или имеет право
брать на веру) высказывание X, т.е. Р станет действовать
так, как будто X — истинная информация.
- Р <Х подразумевает, что Р видит X, т.е. кто-то послал со­
общение пользователю Р , в котором содержится X, Так что
Р может прочесть и воспроизвести X.
- Р\ г^ X означает, что Р однаэюды высказал X и в тот момент
верил в его истинность. Заметим, что здесь мы не уточняем
время этого события.
- Р\ =^ X означает, что X входит в юрисдикцию Р , т. е. Р обла­
дает властью над X и по этому вопросу Р можно доверять.
- # Х означает, что высказывание X получено недавно. Этот
символ используется обычно для числовых вставок.
к
- Р -*—• Q означает, что Р и Q используют для общения разде­
ленный ключ к. Предполагается, что ключ достаточно стоек
и не может быть раскрыт никем из посторонних, если это не
предусмотрено протоколом.
- Обозначение {Х}^ обычно подразумевает, что данные X за­
шифрованы ключом к. Шифрование считают совершенным, в
частности X останется засекреченным до тех пор, пока од-
Глава 6, Распределение симметричных ключей


на из сторон сознательно не раскроет его в какой-то другой
части протокола.
Кроме того, вместо обычной логической операции «И» употребляет­
ся запятая, а запись
А, В
С
означает, что из истинности утверждений АиВ следует истинность
высказывания^ С. Такой способ символьного изображения сложных
конструкций принят во многих формальных логиках.
BAN-логика, опирается на множество постулатов или правил вы­
вода. Мы разберем лишь главные из них.
Правило о значении сообщения:

А\ =АЛ^В,А<{Х}К
А\ =В\ г^Х
Эквивалентная словесная формулировка: из предположений о том,
что А верит в совместное использования ключа К с В^ и А видит
сообщение X, зашифрованное ьслючом К^ мы делаем вывод: А верит,
что В в какой-то момент высказал X. Заметим, что здесь неявно
предполагается, что сам А никогда не высказывал X,
Правило проверки уникальности числовых вставок:
А\ = # Х , А\=В\^Х
А\ =В\ =Х
т.е. если А верит в новизну X и в то, что В когда-то высказал X,
то А верит, что В по-прежнему доверяет X,
Правило юрисдикции
А\ =В\ =>Х,А\ =В\ =Х
А\=Х
говорит, что если А верит в полномочия В относительно X, т. е. А
полагается на 5 в деле с X, и Л верит в то, что и В верит X, то А
должен верить в X.
Другие правила. Оператор доверия («=») и запятая, разделяю-
ш;ая высказывания, рассматриваемые совместно, подчиняются сле­
дующим соотношениям:
Р\ =Х,Р\ =Y Р\ ={X,Y) Р\ =Q\ ={X,Y)
P\={X,Y) ' Р\=Х ' P\=Q\=X '
^ Часто в литературе можно встретить эквивалентное обозначение: Л И Б => С,
которое читается так: высказывания АиВ влекут С. — Прим, перев.
6.3. Формальные методы проверки протоколов

Оператор «однажды высказал» удовлетворяет аналогичному соот­
ношению:
Р\ ^Q\ ^ ( Х , У )
Р\ =Q\ ^Х *
Заметим, что предположения Р\ = Q ˜ Х и Р | = Q ˜ У н е влекут
утверждения Р | = Q ˜ (X, У), поскольку последнее означает, что Q
произнес X и У в одно и то же время. Наконец, если какая-то часть
высказывания получена недавно, то это же можно утверждать и про
всю конструкцию:

р\ =#{х,уу
Попытаемся теперь проанализировать протокол выбора ключа
для А VL В^ опираясь на БЛАГ-логику. Прежде всего сформулируем
цели протокола, которые как минимум состоят в следующем:

A\=AJ^B И В\=А^В,
т. е. оба участника должны поверить в то, что они нашли секретный
ключ для обмена друг с другом закрытой информацией.
Однако можно было бы потребовать и большего, например,

А\=В\=АЛ^В И B\=A\˜AJUB,
что обычно называют подтверэюдением приема ключа. Иначе го­
воря, можно считать, что в результате работы протокола А будет
уверен в знании В о том, что он разделяет секретный ключ с Л, а
В верит в то, что и А знает об их обш;ем ключе.
Перепишем протокол в символьной форме согласно правилам
BAN-ЛОГИКИ. Этот процесс называется идеализацией и наиболее
уязвим для ошибок, поскольку его невозможно автоматизировать.
Кроме того, нам необходимо сделать предположения или сформули­
ровать постулаты, которые считаются истинными в начале работы
протокола.
Для наглядности, чтобы понять, как это все работает «в реаль­
ной жизни», подвергнем анализу протокол широкоротой лягушки,
использующий синхронизацию часов.

6.3.1. Анализ п р о т о к о л а пгирокоротой лягухпки
Напомним, что он состоит из обмена двумя сообщениями:
А—>S: A,{ta,b,kab}kas^
S—>В: {ts,a,kab}kbs'
178 Глава 6. Распределение симметричных ключей

При идеализации это выглядит так:


S-^B: {ts,A\ =Л^ВЬ,,.
Идеализированное первое сообщение говорит 5, что
- ta — временная или числовая вставка,
˜ каЬ — ключ, который прсдлагастся использовать для комму­
никации с В,
Итак, какие предположения сделаны в начале работы протокола?
Ясно, что А^ В и S используют секретные ключи для обмена ши­
фрованными сообщениями друг с другом, что на языке БЛЛ^-логики
может быть выражено как

A\˜A^S, S\=A^S
В\=В^ S, B\=Ai^S,
Есть пара предположений о временных вставках:
S\ = Ща ^ В\= #ts
И еще три предположения:
- В полагается на Л в выборе хорошего ключа:
В\ ={А\ ^А^В),
- В доверяет S передать ключ от А:
f^ab
В\ ={S\ ^Л| =Л^^Б),
- А верит, что сеансовый ключ принят:
А\=А^В,
Обратите внимание на то, как последние предположения обнажают
проблемы, связанные с протоколом, о которых мы говорили ранее.
Опираясь на сделанные предположения, мы можем проанализи­
ровать протокол. Посмотрим, какой вывод можно сделать из пер­
вого сообщения
A^S: {t,,A^Bh^,.
- 5, ВИДЯ сообщение, зашифрованное ключом Kas-) может сделать
вывод о том, что оно было послано клиентом А,
- Наличие свежей временной вставки ta позволяет участнику S
заключить, что и все сообщение написано недавно.
6.3. Формальные методы проверки протоколов 179

- Из свежести всего сообщения S выводит, что клиент А верил
в то, что послал.
- Следовательно,
S\=A\=A^B,
т.е. S подготовлен к посылке второго сообщения протокола.
Обратимся к следующему этапу:
S^B: {t,,a\ =AJ^B}k,,.
- Увидев послание, зашифрованное ключом кьз-, клиент В пони­
мает, что оно было отправлено S.
˜ Временная вставка ts доказывает 5 , что все сообщение было
послано только что.
- Ввиду свежести сообщения, В заключает, что S доверяет все­
му посланному.
- В частности, В верит в то, что S доверяет второй части со­
общения.
- Но В верит и в то, что в юрисдикцию S входит выяснить,
знает ли его партнер А секретный ключ, и поэтому В вверяет
А полномочия по генерированию ключа.
Из этих рассуждений можно сделать вывод:
В\ ^ А ^ В и В\ =А\ =А^В.
Комбинируя это с исходным предположением: А| = А -*-^ Б , полу­
чаем, что анализируемый протокол распределения ключей обосно­
ван. Единственное, чего мы не встретили в нем, это
А\ =В\=А^В,
т. е. А не добился подтверждения тому, что В получил нужный ключ.
Обратите внимание на то, что применение BAN-логики к ана­
лизу формализовало все этапы протокола, так что их стало легче
сравнивать с предположениями, необходимыми любому протоколу
А^ля работы. Кроме того, этот формализм проясняет точки зрения
на работу протокола всех его участников.

Краткое содержание главы

<< Предыдущая

стр. 27
(из 82 стр.)

ОГЛАВЛЕНИЕ

Следующая >>