10.4.1. Формальный анализ криптографических протоколов
Криптографические протоколы, предназначенные для аутентификации и обмена ключами, играют очень важную роль в обеспечении надежного функционирования современных компьютерных систем.
Криптологами было создано много таких протоколов, однако по прошествии времени выяснилось, что не все из них позволяют должным образом защитить компьютерную систему от несанкционированного доступа и предотвратить компрометацию ключей. Причем для некоторых протоколов этот временной промежуток оказался довольно значительным и растянулся на несколько лет.
Как следствие, возникла настоятельная потребность в разработке формальных методов, которые позволили бы находить изъяны в криптографических протоколах в более короткие сроки. И, хотя большинство из этих методов являются универсальными и могут быть использованы для анализа произвольных криптографических протоколов, особое внимание изначально стало уделяться именно протоколам, позволяющим производить аутентификацию пользователей и обмен ключами.
К настоящему времени имеется четыре основных подхода к анализу криптографических протоколов. Первый из них применяет верификационные методы, которые не были специально разработаны для анализа криптографических протоколов. Некоторые из этих методов представляют протоколы в виде конечных автоматов, другие распространяют на них теорию исчисления предикатов первого порядка.
Второй подход заключается в использовании экспертных систем, позволяющих определить, возникают ли в ходе выполнения шагов протокола такие нежелательные события, как компрометация ключа или разглашение пароля. Этот подход дает возможность эффективнее находить в криптографических протоколах конкретные изъяны, однако никоим образом не гарантирует полного отсутствия таковых.
Авторами третьего подхода являются американские криптологи М. Бэрроуз. М. Абади, Р. Нидхэм (М. Burrows, M. Abadi, R. Needham). Они разработали формальную логическую модель, названную по первым буквам их фамилий БАН-логикой (BAN-logic).
Составить с ее помощью общее представление о надежности криптографического протокола нельзя. Однако основное преимущество БАН-логики перед другими подходами заключается в том, что она состоит из набора простых логических правил, которые легко применяются на практике и весьма полезны при обнаружении отдельных изъянов в анализируемых протоколах.
При четвертом подходе используется моделирование шагов протокола с помощью алгебраической системы, которая строится исходя из знаний, имеющихся у участников протокола относительно этого протокола. Затем построенная алгебраическая модель подвергается формальному анализу на предмет достижимости некоторых из ее состояний.
В целом формальный анализ криптографических протоколов пока является довольно новой и до конца не сформировавшейся областью криптологии, и поэтому делать далеко идущие выводы о преимуществе какого-то одного из перечисленных четырех подходов еще рано.
Вопросы к главе 10
Какие требования предъявляются к криптографическим протоколам?
Что понимается под открытыми системами и чем регламентируется их взаимодействие?
Кроме наличия злоумышленника, какие еще предположения выдвигаются относительно участников криптопротокола?
Каковы основные классы прикладных криптографических протоколов?
Чем протокол с арбитражем отличается от протокола с судейством?
Что такое самодостаточный протокол?
Каковы основные виды атак на криптопротоколы?
На чем основана стойкость абстрактного протокола Диффи-Хэллмана согласования ключей?
Каким образом можно скомпрометировать на практике протокол Диффи-Хэллмана с помощью атаки типа «агент посредине»?
В чем состоит задача о разделении секрета?
В чем заключается основное свойство
-пороговой
схемы Шамира по отношению к восстановлению
секрета?Каким образом для схемы Шамира гарантируется невозможность восстановления секрета злоумышленником?
Почему группа в количестве менее
легальных участников не в состоянии
восстановить секрет, защищенный
-пороговой
схемой Шамира?Для чего предназначены протоколы типа SSL?
Какими криптографическими методами обеспечивается конфиденциальность и целостность данных в SSL?
Какого типа сертификаты используются SSL для организации взаимодействия с инфраструктурой открытых ключей?
Каково предназначение системы протоколов безопасных электронных транзакций SET?
Какие основные требования по защите операций электронной коммерции обеспечивает протокол SET?
Для чего предназначен протокол IPsec и влияют ли на его роботу связные протоколы, действующие в сети?
Каковы основные преимущества обеспечения безопасности информации на основе IPsec?