ЛОГИЧЕСКИЕ МЕТОДЫ АНАЛИЗА ПРОТОКОЛОВ РАСПРЕДЕЛЕНИЯ КЛЮЧЕЙ

ВВЕДЕНИЕ 3
1. ФОРМАЛИЗМ 6
§ 1.1 Основные обозначения 6
§ 1.2 Логические постулаты и операции с кванториями 7
§ 1.3 Идеализация и анализ протоколов 11
§ 1.4 Формализация протоколов 15
§ 1.5 Семантика 15
2. ПРОТОКОЛ ЦЕРБЕР В2 И В5 20
§ 2.1 Спецификация и идеализация протокола Цербер В2 20
§ 2.2 Анализ протокола Цербер В2 22
§ 2.3 Спецификация и идеализация протокола Цербер В5 25
§ 2.4 Анализ протокола Цербер В5 28
3. ПРОТОКОЛЫ ЯХАЛОМ 35
§ 3.1 Спецификация и идеализация протокола Яхалом ВЗ 35
§ 3.2 Анализ протокола Яхалом ВЗ 37
§ 3.3 Спецификация и идеализация протокола Яхалом В4 40
§ 3.4 Анализ протокола Яхалом В4 42
ЗАКЛЮЧЕНИЕ 47
СПИСОК ЛИТЕРАТУРЫ
Купить

Вопросы убеждения имеют важное значение при анализе протоколов для проверки подлинности участников в распределенных вычислительных системах. Одним из первых логических методов для этой цели был предложен М. Барроузом, М. Абади, Р. Нидхеймом [1]. Ими был разработан формальный метод анализа протоколов, в настоящее время получивший названия BAN-логика. В своей работе, они применили эту логику для анализа различных протоколов. Они показали, как различные протоколы тонко отличаются относительно требуемых первоначальных предположений участников и их окончательных убеждений. Данный формализм позволяет выделить и точно выразить эти различия.
Проблема заключается в следующем. В распределенных вычислительных системах и других подобных сетях компьютеров необходимо иметь процедуры, с помощью которых различные пары участников (люди, компьютеры, услуги и т.п.) могут установить идентичность друг друга. Обычным способом решения этой проблемы является использование секретов, обычно это ключи шифрования. В самых общих чертах, протокол аутентификации гарантирует тройники, что если участники на самом деле, те кто они говорят, то они будут в конечном итоге владеть одним или несколькими общими секретами, или по крайней мере, они станут способны распознавать использование секретов других участников. Например, некоторые протоколы аутентификации совместно устанавливают ключи шифрования, которые участники могут использовать в последующем сообщении. Другие протоколы аутентификации основанные на криптографии с открытым ключом, сначала распространяют открытые ключи участников, а затем используют их, чтобы установить общие секреты.
Протоколы с участием совместного использования ключей шифрования (протоколы с симметричными ключами) используются серверы аутентификации, которые имеют ключи с каждым участником и как правило генерируют новые ключи сеанса для связи между участниками. Протоколы с открытым ключом используют центр сертификации, который имеет хорошо известный открытый ключ и является доверенным, чтобы передать открытые ключи участникам. Оба сервера аутентификации и сертификационных центров доверены обеспечить надлежащее использование данных, они держат при выполнении протоколов аутентификации; серверам идентификации часто также доверяют,
чтобы создавать новые тайны надлежащим способом, например, не создавать тот же самый ключ каждый раз.
Аутентификация проста в достаточно благоприятных условиях. Такое обычно нельзя предполагать и особенно необходимо принять меры предосторожности против путаницы, вызванной переизданием старых сообщений. В частности, необходимо обеспечить, что переигровка не может принудительно использовать старый и возможно скомпрометированный секрет. Значительная часть работ в литературе посвящена обеспечению того, чтобы информация, на которую протоколы действуют, была своевременной. Такие меры предосторожности вызывают, то что мы имеем дело с вопросами веры, доверия и делегирования полномочий. Тем не менее, это не было четко изложено до работы Барроуз М., Абади, М., Нидхейм, Р.М [1]. В результате разнообразных дизайнерских решений соответствующих различным обстоятельствам, существуют различные протоколы аутентификации. Таким образом, существует понимание необходимости эксплицировать их формально, чтобы понять в какой степени они действительно достигают предполагаемых результатов. Они тонко отличаются в своих конечных состояниях, а иногда и может быть показано, что протокол зависит от предположений, которых должным образом не заботились. Определим логику аутентификации для объяснения шаг за шагом протоколов, со всеми явно сделанными исходными допущениями и с четко изложенными конечными состояниями. С введением в теорию формалинных доказательств можно ознакомиться в [1].
Цель работы: Проанализировать некоторые протоколы и сравнить их. А именно, мы проанализируем протокол Цербер В5 и сравним его с Цербер В2 проанализированным в статье [1]. Интерес к этому протоколу обусловлен его широкой распространенностью на практике. В частности этот протокол является одним из основных протоколов использующихся в операционной системе Windows.
Так же были проанализированы несколько версии протокола Yalialom (2001 годы). Описания протоколов взяты из [7].
Анализ протоколов на основе формальных методов помогает ответить на следующие вопросы:
Чего достигает этот протокол?
Нужно ли для этого протокола больше предположений, чем для другого?
Является ли этот протокол избыточным?
Шифрует ли этот протокол что-нибудь, что можно было бы отправить в открытом виде, не ослабляя его?
Опишем вкратце содержание работы:
В первой главе приводятся основные правила формального метода. В этом разделе описаны синтаксис и семантика BAN-логики, её правила, и преобразования, которые применяют к протоколам для их формального анализа. Эта глава содержит основные обозначения для протоколов, логические постулаты (основные свойства и правила), методы идеализации протоколов, схему анализа, формализованных протоколов.
Во второй главе приводим протоколы спецификации Цербер В2 [1] и Цербер В5. Идеализируем и анализируем их согласно правилам BAN-логики, и сравниваем полученные результаты.
В главе 3 аналогичным образом рассматривается протоколы Яхалом ВЗ и В5 [7].

Купить