Обобщенные компиляторы для обмена ключами с аутентификацией

Материал из Национальной библиотеки им. Н. Э. Баумана
Последнее изменение этой страницы: 10:11, 28 июня 2016.
Generic Compilers for Authenticated Key Exchange
Generic Compilers for Authenticated Key Exchange.png
Авторы Tibor Jager, Florian Kohlar, Sven Schäge, and Jörg Schwenk
Опубликован 2010 г.
Сайт International Association for Cryptologic Research
Перевели Sergei Perfilyev
Год перевода 2015 г.
Скачать оригинал
Аннотация. До настоящего времени все решения для обмена ключами с аутентификацией объединяли согласование ключей и аутентификацию в одном криптографическом протоколе. Однако, во многих важных сценариях использования согласование ключей и аутентификация — безусловно, разделенные протоколы. Этот факт делает возможным проведение эффективной атаки на наивное объединение этих протоколов. В этой статье мы предлагаем новые компиляторы для двустороннего обмена ключами с аутентификацией, которые доказуемо безопасны в соответствии с моделью Беллара-Роджея. Эти конструкции обобщенны: согласование ключей выполняется в первую очередь, в результате чего (без вмешательства противника) имеем секретный ключ сессии на обеих сторонах. Этот ключ (или производный от него) вместе со стенограммой всех сообщений согласования ключей в протокол аутентификации, где это объединяется со случайной задачей, полученной в ходе аутентификации.
Ключевые слова: обмен ключами с аутентификацией, компилятор протокола, TLS

Введение

Согласование ключа с аутентификацией (AKE) — основной строительный элемент в современной криптографии. Многие безопасные протоколы для двустороннего и для группового согласования ключей были предложены, включая обобщенные компиляторы, которые превращают простой протокол соглашения о ключе в протокол с аутентификацией, с множеством дополнительных свойств безопасности. Однако, все известные конструкции (включая, например, модульное применение[1] и компилятор Каца и Юна[2]) представлены в виде одного криптографического протокола несмотря на то, что многие реальные приложения, требующие серьезной безопасности, включают два или более совершенно разделенных протоколов:

  1. Аутентификация и SSL/TLS. Самый знаменитый пример — SSL/TLS. Несмотря на то, что и сервер, и браузер могут быть аутентифицированы доказуемо безопасным путем [3][4] с использованием одного криптографического протокола (TLS), почти всем известны веб приложения, аутентифицирующие клиента через другой протокол поверх TLS канала. Безопасность этих протоколов основана на предположении, что пользователь может аутентифицировать сервер на основе индикатора безопасности в браузере, который, как было показано[5], можно обойти. Мы не полагаемся на это предположение. Вместо этого, мы рассматриваем SSL/TLS просто как протокол соглашения о ключе, который не может быть изменен ввиду огромного числа реализаций, используемых по всему миру. Мы можем, однако, изменить протокол аутентификации, так как протокол аутентификации часто реализуется в HTML/Javascript [прим. 1].
  2. Технология единого входа (SSO), встроенная в браузер. Этот сценарий, возможно, является самым сложным, и его формализация выходит за рамки этой статьи. Однако, это может служить иллюстрацией того, как криптографические протоколы объединяются сегодня для реализации обмена ключами и аутентификации. В SSO-протоколах два протокола обмена ключами и два различных протокола аутентификации объединяются для достижения желаемой цели. Криптографически безопасные SSO-протоколы были описаны, например, в [6].

В этой работе мы представляем новый компилятор, который обрабатывает эти сценарии. Более того, мы можем использовать наш компилятор, чтобы объединить существующие протоколы аутентификации в новый облик с протоколами обмена ключами. Это включает в себя следующее:

  1. Аутентификация с нулевым разглашением. Протоколы с нулевым разглашением были разработаны для того, чтобы аутентифицировать сущности. Однако, во всех известных компиляторах, они не могут быть объединены с соглашением о ключе, за исключением тех, которые преобразуются в схему цифровой подписи, используя эвристику Фиата-Шамира. С нашим вторым компилятором, эти протоколы могут использоваться напрямую, что делает возможным многие новые интересные протоколы.
  2. Аутентификация с сохранением конфиденциальности. С нашим компилятором, мы можем легко объединять протоколы с сохранением конфиденциальности, например, Direct Anonymous Attestation с различными протоколами согласования ключей.


Атака посредника (MITM)

Сценарий атаки. Атака посредника.

Реальный сценарий атаки следующий: враг ("Ева") действует как активный человек посередине между и во время обмена ключами, а затем действует как пассивный “провод” во время аутентификации. В результате успешно аутентифицирован как "" для и как "" для , и обменялся (различными) ключами с и . Для предотвращения этой атаки необходимо, конечно, применить стандартный криптографический примитив для превращения протокола обмена ключами в протокол обмена ключами с аутентификацией (AKE) [1], но это невозможно в вышеизложенных случаях, потому что реализация протокола обмена ключами (KE) не может быть изменена или желаемые цели безопасности (например, конфиденциальность) не могут быть достигнуты с использованием стандартных компиляторов. Наш компилятор превращает объединение этих двух протоколов в доказуемо безопасный протокол обмена ключами с аутентификацией. Во время компиляции немного изменится только протокол аутентификации.


Атаки с неизвестным сеансовым ключом (UKS)

Сценарий атаки. Атака с неизвестным сеансовым ключом.

Для того чтобы доказать безопасность в соответствии со стандартной моделью Беллара-Роджея (BR), полученный протокол должен быть безопасен против атак с неизвестным сеансовым ключом [7][8], которые непосредственно не приводят к проведению атак в реальном мире, но являются важным критерием в доказательстве модели. Интересно отметить, что в нашем случае это является перпендикулярной атакой к атаке посредника: враг действует как человек посередине в протоколе аутентификации. Для обеспечения безопасности против обеих атак, обычно необходимо два компилятора: один компилятор, который добавляет аутентификаторы в каждое сообщение [1], и второй, который включает полное состояние сессии в вычисленном ключе сессии [9]. Наши компиляторы справляются с этой задачей в один шаг, потому что мы заставляем врага доказать знание сессионного ключа через доставленный ключ dk во время аутентификации. Таким образом противник не может ни , ни без знания , и ни , ни не принимают ключ.


Протоколы для обмена ключами с аутентификацией, применяемые на практике

Если две стороны принимают ключи, они обмениваются общим состоянием. Это состояние состоит из секретного ключа и стенограммы всех полученных и отправленных сообщений. Эти стенограммы играют важную роль в модели Беллара-Роджея, так как это определяет возможные атаки противника. В протоколах, применяемых на практике, хэш этих стенограмм включён в последнее сообщение, защищённое с использованием имитовставки (MAC) для защиты от атаки посредника.


A&KE компиляторы

Для защиты от атаки посредника в нашем обобщенном сценарии достаточно просто включить стенограмму протокола согласования ключей в протокол аутентификации. (Многие протоколы аутентификации предлагает возможность для аутентификации произвольных строк, выбранных или , например, протокол аутентификации, основанные на цифровых подписях или MAP2 протокол[10].) Такие компиляторы защищают от атак посредника, потому что (а) любые изменения в сообщениях протокола обмена ключами автоматически влияют на изменения в сообщениях протокола аутентификации (так как описание включено), что приводит к прерыванию протокола аутентификации, если этот протокол соответствует модели Беллара-Роджея. Таким образом, (б) противник ограничен принятием только пассивной роли, атакуя протокол обмена ключами, но этот протокол по определению защищен от пассивных противников. К сожалению, этот простой компилятор не может быть доказан в соотвествии с моделью Беллара-Роджея, потому что противник так же может получить доступ к стенограмме протокола и может использовать это в обоих примерах протокола аутентификации. Чтобы избежать этой атаки, секретное значение, известное только и (то есть ключ сессии ) должен использоваться протоколе аутентификации в обобщенном виде. Существует как минимум два способа добиться этого:

  1. Дополнительная пара сообщений может быть отправлена после обмена ключами и аутентификацией. Эти сообщения содержат криптографическую контрольную сумму стенограммы обоих протоколов, используя ключ полученный из ключа , полученного из протокола обмена ключами и некоторой псевдослучайной функции . Действительный ключ сессии , полученный скомпилированным протоколом (то есть значение, возвращенное Reveal- или Test-запросом в модели Беллара-Роджея) также получен из как . В третьей части мы опишем, как компилятор это выполняет более детально, и докажем его безопасность в стандартной модели.
  2. Или иначе, мы можем изменить значение, которое присутствует во всех защищенных протоколах аутентификации, в этом случае это не измени свойства протокола: В обобщенных протоколах аутентификации, случайная задача , гарантирующая актуальность сообщения(-ий), должна быть отправлена от отправителя к получателю , который отправляет ответ от . Идеально, эта задача выбирается из большого пространства сообщений с равномерным распределением. Мы предполагаем, что выбирается случайно из для некоторого безопасного параметра . Ответ вычисляется используя секретный долговечный ключ для и задачи . Наш компилятор немного изменяет вычисление . Вместо использования задачи напрямую, мы используем полученной значение из того же распределения: , , где — некоторая хэш функция, смоделированная как случайный оракул. Пожалуйста, заметьте, что никогда не передаётся, но должно быть вычислено и . Таким образом, противник не узнает . Эта конструкция не изменяет свойства безопасности аутентификационного протокола. В 4 части мы дадим доказательство безопасности для этого компилятора в соответсвии с моделью случайного оракула.


Связанные работы

В своих работах предыдущих работах был рассмотрен обмен ключами с аутентификацией между двумя сторонами [1][10], Беллар и др. начали серию исследований, которые расширились в двух направлениях: групповом соглашении о ключе [11][12][13][2], и некоторых моделях для покрытия различных типов атак [14][15][16]. Все эти модели охватывают выполнение протокола с искажением несвязанных сеансовых ключей. Все модели грубо могут быть разделены на две группы: модели, требующие знания уникального ID сессии до начала протокола, и модели, которые генерируют этот ID. [14] это прототип первой из этих моделей: доказательство и определения просты, но непонятно, как ID сессии может быть определен для практических приложений. (Например, в случае атаке посредника на SSL браузер и сервер не обмениваются общим состоянием.) Такие современные модели, как [15] или [16], таким образом избегают эти допущения и генерируют идентификатор сессии из сообщений, отправленных и полученных предполагаемыми партнерами.

Атаки с неизвестным сеансовым ключом в реальном мире не угрожают безопасности криптографических протоколов, но сводят на нет доказательства безопасности в формальных моделях [10]: Если противник сможет заставить двух участников протокола принять один и тот же ключ сессии без согласования общения, Reveal-запрос к одному из участников поможет пройти Test-игру против другого. Чу, Бойд и Хичкок показали, как свести на нет доказательства безопасности различных протоколов в различных моделях [7][8] и как решить проблему включением всей информации о сессии в вычисление ключа сессии[9]. Они смогли сравнить относительные преимущества различных моделей, предполагая, что идентификаторы сессий построены в виде конкатенации обмениваемых сообщений. Канетти и Кравчук в [17] рассмотрели практически важный протокол (IPSec IKE), в котором аутентификация происходит после обмена ключами. Кроме того, он является одиночным протоколом обмена ключами с аутентификацией и, таким образом, не сравним с нашей конструкцией. В 2008 Моррисси и другие изучили безопасность соглашения о ключах TLS [4] и предоставили модульное и обобщенное доказательство безопасности для установленных ключей приложений.

Кац и Юн представили в своей работе[2] первый масштабируемый компилятор, который преобразует любой пассивно безопасный протокол обмена ключами в активно безопасный протокол обмена ключами с аутентификацией. Их компилятор добавляет один раунд и фиксированный размер (на пользователя) к исходной схеме с помощью добавления в конец дополнительной подписи к каждому сообщению протокола.


Наш вклад

В этой статье мы описали два новых компилятора, которые позволяют нам объединить протоколы соглашения о ключах (которые в модели Беллара-Роджея должны быть безопасны только против пассивных противников) с произвольными протоколами аутентификации в форме протокола для обмена ключами с аутентификацией в смысле [10].

Эти компиляторы позволяют нам формально доказать безопасность реальных протоколов согласно модели Беллара-Роджея, что ранее было невозможно. Наиболее важным случаем здесь является TLS с протоколом аутентификации поверх TLS канала, который может быть доказуемо безопасным, если протокол аутентификации безопасен согласно модели Беллара-Роджея. Это возможно, так как мы считаем, что TLS — только протокол соглашения о ключах и не является протоколом обмена ключами с аутентификацией, и, вполне вероятно, безопасность (некоторых шифров) TLS против пассивных противников может быть доказана.

К тому же, компиляторы позволяют использовать модульные конструкции для новых протоколов для обмена ключами с аутентификацией, используя существующие протоколы (например, TLS, IPSec IKE) или новые (например, аутентификация с неизвестным сеансовым ключом, групповые подписи). Формальное доказательство безопасности значительно упрощается, так как безопасность соглашений о ключах и протоколов аутентификации могут быть доказаны по отдельности, и наши теоремы обеспечивают безопасность комбинированного протокола.

Определения

В этом разделе описан синтаксис и определения из области безопасности основных строительных блоков наших компиляторов протоколов.


Схема цифровой подписи

Схема цифровой подписи — тройка , состоящая из алгоритма генерирования ключей генерирующий (открытый) ключ подтверждения и секретный ключ для подписи , принимающий на вход в качестве параметра , подписывающий алгоритм , генерирующий подпись для сообщения , и подтверждающий алгоритм , возвращающий 1, если — действительная подпись для при ключе , и 0 в противном случае.

Рассмотрим следующий эксперимент по безопасности, проведенный между криптографом и криптоаналитиком :

  1. Криптограф генерирует пару из открытого и закрытого ключей , криптоаналитик получает в качестве входных данных.
  2. Криптоаналитик может запросить подпись произвольного сообщения . Криптограф подписывает каждое сообщение цифровой подписью . Здесь — индекс, причем , а — некоторый полином . Запросы могут быть адаптированы.
  3. В конечном счете, криптоаналитик выдаёт пару сообщение/подпись .
TemplateDifinitionIcon.svg Определение «Определение 1»
Мы говорим, что экзистенциально защищена от адаптивных атак выбранного сообщения (EUF-CMA), если для всех возможных за полиномиальное время (для параметра ) криптоаналитиков , где — это некоторая незначительная функция.

Коды аутентификации сообщения

Код аутентификации сообщения (имитовставка) — алгоритм . Этот алгоритм реализует детерминированную функцию , которая принимает на вход (симметричный) ключ и сообщение и возвращает строку .

Рассмотрим следующий эксперимент по безопасности, проведенный между криптографом и криптоаналитиком :

  1. Криптограф выбирает случайным образом.
  2. Криптоаналитик может запросить произвольное сообщение . Криптограф отвечает на каждое сообщение строкой . Здесь — индекс, причем , а — некоторый полином . Запросы могут быть адаптированы.
  3. В конечном счете, криптоаналитик выдаёт пару .
TemplateDifinitionIcon.svg Определение «Определение 2»
Мы говорим, что — защищенный код аутентификации сообщения, если для всех возможных за полиномиальное время (для параметра ) криптоаналитиков , где — это некоторая незначительная функция.

Псевдослучайные функции

Псевдослучайная функция — алгоритм . Этот алгоритм реализует детерминированную функцию , которая принимает на вход ключ и некоторую битовую строку и возвращает строку .

Рассмотрим следующий эксперимент по безопасности, проведенный между криптографом и криптоаналитиком :

  1. Криптограф выбирает случайным образом.
  2. Криптоаналитик может запросить произвольное сообщение . Криптограф отвечает на каждое сообщение строкой . Здесь — индекс, причем , а — некоторый полином . Запросы могут быть адаптированы.
  3. В конечном счёте, атакующий выдает значение и специальный символ . Криптограф вычисляет и выбирает случайным образом. Затем он подбрасывает монетку и возвращает криптоаналитику.
  4. Наконец, криптоаналитик выдаёт предположение о значении параметра .
TemplateDifinitionIcon.svg Определение «Определение 3»
Мы говорим, что — защищенная псевдослучайная функция, если для всех возможных за полиномиальное время (для параметра ) криптоаналитиков , где — это некоторая незначительная функция.

Протоколы обмена ключами

Протокол двустороннего обмена ключами — протокол, выполняемый между двумя сторонами и . В результате выполнения протокола и , и получают один и тот же ключ .

TemplateDifinitionIcon.svg Определение «Определение 4»
Мы говорим, что протокол обмена ключами пассивно защищен, если для любого врага за полиномиальное время выполняется для некоторой незначительной функции в следующем эксперименте:
  1. Криптограф генерирует открытые параметры протокола (например, генератор, описывающий группу, и т.п.).
  2. Криптоаналитик получает и может отправлять запросы криптографу. С этой целью он отправляет символ . Затем криптограф запускает протокол и получает стенограмму всех сообщений, полученных в результате работы протокола, и ключ . Криптограф возвращает .
  3. В итоге, криптоаналитик выдаёт специальный символ . Получив , криптограф запускает протокол, получающий стенограмму и ключ , выбирает из равномерного распределения пространства ключей протокола и подбрасывает монетку . После чего возвращает криптоаналитику.
  4. Криптограф может продолжать выполнять -запросы.
  5. Наконец, криптограф выдаёт бит .
Мы говорим, что криптограф выигрывает, если .

Простые компиляторы, удовлетворяющие приведенному выше определению, называются протоколом Диффи-Хеллмана (в предположении, DDH) или протоколом транспортировки ключей, использующий схему безопасного шифрования IND-CPA (т.е. сторона выбирает случайный ключ , шифрует ключ открытым ключом стороны и передает шифротекст обратно стороне ).


Защищенный обмен ключами с аутентификацией

В то время как модель безопасности для пассивно защищенных протоколов обмена ключами является очень простой, более сложная модель требует моделировать возможность наличия активных врагов для определения безопасного обмена ключами с аутентификацией. Мы должны описать тонкости выполнения, которые мы ожидаем от реализаций протокола, атак, против которых должен быть защищен наш протокол, и какой результат мы ожидаем в результате выполнения протокола с определенным противником. В соответствии с серией исследований [18][14][19][16], начатых Белларом и Роджеем [10], мы моделируем нашего противника, обеспечивая "среду выполнения", что позволяет эмулировать возможности противника в реальном мире. То есть враг имеет полный контроль над сетью, таким образом может перенаправить, изменить или выбросить любой из пакетов, отправленных участниками или вставить новые сообщения.

Execution model. Пусть и два многочлена от некоторого безопасного параметра . Наша модель характеризуется набором оракулов . Оракул представляет собой сущность , запустившая протокол с сущностью , для времени S. Каждый оракул имеет своё собственное внутреннее состояние (например, текущее время), все оракулы, представляющие некоторую сущность , используют одни и те же секреты сущности . Более того, каждый оракул имеет переменную , в которой хранится упорядоченный список всех полученных и отправленных сообщений к этому времени.

Оракул завершает свою работу, если он получает сообщение, которое не соответствует спецификации протокола, или отправлено/получено последнее сообщение в соответствии со спецификацией протокола. Когда процесс завершается, он выдаёт "принять" или "отклонить" и, возможно, ключ .

Противник может взаимодействовать с этими оракулами путем выполнения различных типов запросов. Перед первым запросом генерируется пара секретный/открытый ключ для каждого субъекта . Противник получает в качестве входных данных открытые ключи , и затем, возможно, выполнить следующий запрос:

  • : Противник может использовать этот запрос, чтобы передать любое сообщение оракулу . Оракул отвечает в соответствии со спецификацией протокола. Если , где обозначает пустую строку, то оракул отвечает первым сообщением в соответсвии с протоколом.

Безопасные протоколы аутентификации. Протокол аутентификации — протокол, запущенный между двумя процессами и или двумя сторонами и , где оба процесса выдают либо "принять", либо "отклонить" в результате выполнения протокола. Мы определяем корректность и защищенность протокола аутентификации на основании идеи о согласовании (matching conversation), описанном Белларом и Роджеем[10].

В дальнейшем, пусть обозначает стенограмму всех полученных и отправленных сообщений процессом . Интуитивно, мы хотели бы сказать, что протокол корректен, если процесс выдаёт "принять", если существует такой процесс , что . Кроме того, мы хотели бы сказать, что протокол является безопасным, если процесс выдаёт "принять" тогда и только тогда, когда существует такой процесс , что .

Как и в [10], мы сталкиваемся с небольшими техническими трудностями здесь, которые присущи протоколам аутентификации. Предположим, что посылает последнее сообщение протокола (таким образом, протокол инициировал , если число раундов четное, и , если число раундов нечетное). Сторона не получает никакого ответа после последнего его сообщения, таким образом, должен "принять", не зная, получил ли последнее сообщение.[прим. 2] Решить эту проблему можно, взяв усеченную стенограмму (без последнего сообщения), правда, тогда мы должны определить корректность и безопасность немного более сложном образе.

TemplateDifinitionIcon.svg Определение «Определение 5»
Мы говорим, что два процесса и согласованы, если либо
  • посылает последнее сообщение в соответствии со спецификацией и , либо
  • посылает последнее сообщение в соответствии со спецификацией и .
TemplateDifinitionIcon.svg Определение «Определение 6»
Мы говорим, что протокол аутентификации корректен, если для любого процесса утверждается, что "принимает", если существует процесс такой, что и согласованы.
TemplateDifinitionIcon.svg Определение «Определение 7»
Мы говорим, что протокол аутентификации корректен в соответствии с моделью Беллара-Роджея, если для любого противника из класса P (работающего за полиномиальное время), взаимодействующего с черным ящиком , как описано выше, выполняется следующее:
  • Каждый процесс черного ящика "принимает" тогда и только тогда, когда существует процесс такой, что и согласованы.

Безопасные протоколы обмена ключами с аутентификацией. Протокол обмена ключами с аутентификацией — протокол аутентификации, где дополнительно обе стороны получают ключ после "принятия". Интуитивно, мы хотели бы сказать, что протокол обмена ключами с аутентификацией является безопасным, если

  • протокол является безопасным протоколом аутентификации и
  • противник не может отличить ключ , вычисленный в результате выполнения протокола, от случайного значения из пространства ключей. Это должно выполняться даже в том случае, если противник сможет узнать, как вычисляется ключ.

Мы формализуем это за счёт добавления ещё двух типов запросов, которые противник может выполнять:

  • : Этот запрос может быть выполнен только один раз на протяжении всей игры. Если процесс (пока) не "принят", черный ящик выдаёт некоторый символ провала . В противном случае, черный ящик подбрасывает монетку . Если , возвращается случайный элемент из пространства ключей. Если , то возвращается сессионный ключ , вычисленный в процессе .
  • : Противник может узнать ключ , вычисленный в процессе , задавая этот тип запроса. Противник отправляет в черный ящик. Если процесс "принимается", черный ящик выдает ключ для процесса . Иначе — возвращается символ провала .
TemplateDifinitionIcon.svg Определение «Определение 8»
Пусть будет противником из класса P, взаимодействующим с черным ящиком , описанном выше (обозначим как ).

Мы говорим, что протокол обмена ключами с аутентификацией защищен в соответствии с моделью Беллара-Роджея, если

  1. является безопасным протокол аутентификации согласно определению 7, и
  2. для любого .

Согласно Шоапу[20], мы не должны явно моделировать Corrupt-запрос, так как можно свести модель Беллара-Роджея к модели без Corrupt-запросов (см. также [21]).

Компилятор обмена ключами с аутентификацией в стандартной модели

Протокол AKE.

Опишем теперь наш универсальный компилятор AKE. Компилятор принимает в качестве входных данных следующие блоки (которые были описаны в предыдущем разделе):

  • протокол обмена ключами KE,
  • схема цифровой подписи ,
  • код аутентификации сообщения MAC,
  • псевдослучайная функция PRF.

Скомпилированный протокол выполняется между двумя сторонами и следующим образом (см. также рисунок):

  1. и запускают протокол обмена ключами. К примеру, обе стороны могут запустить хорошо известный протокол Диффи-Хеллмана [22]. В ходе выполнения протокола обе стороны вычисляют ключ и записывают стенограммы и , где состоит из всех сообщений, переданных и полученных стороной .
  2. Ключ , вычисленный на предыдущем этапе, используется для доставки двух других ключей: и , где и — некоторые случайные фиксированные константы такие, что [прим. 3].
  3. Затем выбирает случайную величину и отправляет , который, в свою очередь, выбирает и отправляет .
  4. Сторона вычисляет подпись с помощью своего закрытого ключа , где — стенограмма всех принятых и отправленных сообщений к этому времени. Затем вычисляет подпись для стенограммы всех принятых и отправленных сообщений. Пусть — подписи, отправленные и полученные стороной , а — подписи, отправленные и полученные стороной .
  5. отправляет для стенограммы , используя ключ , вычисленный на втором шаге. отвечает сообщением .
  6. Сторона "принимает", если и , то есть если — действительная подпись для и проверочного ключа и если — действительный для при ключе . "принимает", если верно, что и . Наконец, если обе стороны "принимают", возвращается ключ .

Заметим, что подписи и имитовставки проверяются с помощью внутренних стенограмм сторон и . Смысл встраивания стенограмм в протокол в том, чтобы определить любые изменения, которые активный противник сделает в сообщениях, отправляемых сторонами и . Неформально, в двухслойной аутентификации, состоящей из схемы подписи и имитовставки, подпись используется для аутентификации пользователей и срыву атаки посредника на протокол обмена ключами, в то время как имитовставка используется как неявный шаг "подтверждения ключа", для противодействия атаке неизвестного сеансового ключа[7][8].

Это позволяет нам доказать безопасность, требуя безопасности используемых блоков, а именно, мы требуем, чтобы KE был защищен только от пассивных противников, цифровые подписи были экзистенциально защищены от адаптивных атак выбранного сообщения и MAC и PRF удовлетворяли своим стандартным требованиям безопасности.

Замечание 1. Цифровые подписи, отправленные в первом раунде после запуска KE является лишь конкретной реализацией tag-based схема аутентификации как показано в [23]. Можно обобщить определенный выше протокол, заменив цифровые подписи на tag-based схему аутентификации без существенных изменений в протоколе или доказательстве, приведенном ниже.

Анализ безопасности

TemplateTheoremIcon.svg Теорема Теорема 1
Если протокол обмена ключами, схема подписи, код аутентификации сообщения и псевдослучайная функция безопасны в соответствии с определениями, приведенными в разделе 2, то приведенный выше протокол является безопасным протоколом обмена ключами с аутентификацией согласно определению 8.
Доказательство

Мы докажем эту теорему с помощью двух лемм. Лемма 1 утверждает, что AKE протокол удовлетворяет первому свойству определения 8, а Лемма 2 — второму.

TemplateTheoremIcon.svg Теорема Лемма 1
Если протокол обмена ключами (КЕ), схема подписи (SIG), код аутентификации сообщения (MAC) и псевдослучайная функция (PRF) безопасны в соответсвии с определениями, приведенными в разделе 2, то выполняется 1 часть определения 8.
Доказательство

Доказательство приводится в виде серии игр, следуя [24][25]. Первая игра — реальный эксперимент по безопасности. По предположению, существует противник , который нарушает безопасность этого протокола. Затем мы опишем несколько промежуточных игр, которые поэтапно изменяют оригинальную игру. Далее мы покажем, что в финальной игре по безопасности противник имеет всего лишь незначительное преимущество в нарушении безопасности протокола. Наконец, докажем, что (при сделанных предположениях безопасности) противник не может отличить ни одну из игр от её предшественника . Пусть будет событием, в котором выигрывает игру , и пусть будет некоторой незначительной функцией для безопасного параметра k.

Игра 0. Это оригинальная игра по безопасности с , то есть противник всегда получает "реальный" ключ. По предположению, может отличить от случайного ключа (т.е. корректный ответ на запрос), когда получает доступ к оракулам и , в то время как и "принимают".

Игра 1. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор останавливается, если и "принимают" и .

Утверждение 1. Мы утверждаем, что согласно определению EUF-CMA защищённой схемы цифровой подписи. Доказательство этого утверждения основывается на том, что с точки зрения стороны стенограмма является в подавляющем большинстве случаев уникальной (с условием честного выбора ) и с точки зрения аналогичным образом также является уникальным.

Игра 2. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор теперь случайным образом выбирает ключ для получения и как и .

Утверждение 2. Мы утверждаем, что ввиду безопасности KE против пассивных противников. В доказательстве мы используем тот факт, что должно выполняться , если или "принимает", так как в противном случае мы останавливаемся согласно Игре 1.

Игра 3. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор теперь выбирает случайным образом ключ (вместо ) для вычисления и как и .

Утверждение 3. Мы утверждаем, что ввиду безопасности псевдослучайной функции PRF. В доказательстве мы используем тот факт, что мы сменили "реальный" ключ вычисленный в KE на "случайный" ключ в Игре 2.

Заметим здесь, что, поскольку пространство выходного ключа KE должно соответствовать пространству входного ключа PRF и PRF считается безопасной, то отсюда неявно следует, что пространство выходного ключа KE должно быть супер-полиномиально большим.

Игра 4. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор останавливается, если и "принимают" и .

Замечание 4. Мы утверждаем, что . Напомним, что в Игре 4 мы имеем ввиду условия остановки из Игры 1, и что мы заменили ключ , вычисленный в KE, на случайно выбранный ключ в Игре 3 для вычисления MAC-a. Таким образом, если мы имеем , то противник должен подделать MAC, чтобы или "приняли".

Игра 5. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор останавливается, если или "принимают" и , где состоит из кодов MAC, принятых и отправленных стороной , и для стороны .

Утверждение 5. Мы имеем . Это следует из того факта, что мы определили MAC как детерминированную функцию, (из Игры 1) и (из Игры 4).

Объединяя вероятности Игр от 0 до 5, получаем, что обе стороны и "принимают" только если они согласованы, за исключением незначительной вероятности ошибки.
TemplateTheoremIcon.svg Теорема Лемма 2
Если KE, SIG, MAC и PRF безопасны в соответствии с определениями, приведенными в разделе 2, то для описываемого протокола выполняется второе свойство определения 8.
Доказательство

Опять мы проведем последовательность игр. Первые 5 игр в доказательстве идентичны последовательности из доказательства Леммы 1. Мы лишь добавим еще одну игру.

Игра 6. Эта игра протекает так же, как и предыдущая за исключением того, что симулятор теперь выбирает случайным образом из пространства ключей.

Утверждение 6. Мы утверждаем, что . Это опять же следует из безопасности PRF и того, что выбирается равномерно случайным и независимым образом (сравните с Игрой 2).

В Игре 6 противник получает произвольный ключ из равномерного распределения. Однако, объединяя вероятности Игр от 0 до 6, получаем, что Игра 6 (вычислительно) неотличима от Игры 0, что и доказывает неразличимость "реальных" и "случайных" ключей. Таким образом, протокол безопасен в смысле Определения 8.


Альтернативный компилятор для практических протоколов

Схема стандартного протокола аутентификации (слева) и версия, модифицированная нашим компилятором (справа).

Наш второй компилятор предназначен для практических применений, где мы не можем изменить ключ сессии по протоколу KE[9], или там, где хотим избежать дополнительного раунда сообщений после завершения протокола аутентификации. В этом компиляторе мы непосредственно интегрируем стенограмму протокола обмена ключей и секретное значение в протокол аутентификации. Чтобы сделать это, мы должны сначала определить "универсальную" схему протокола аутентификации. У нас есть только минимальные требования к протоколам аутентификации. Сторона (проверяющий), которая хочет аутентифицировать другую сторону (доказывающий), должна включить высокое значение энтропии в один из своих протоколов. (В противном случае противник может просто отвечать различными ответами на наиболее вероятные задачи для повышения преимущества.) Доказывающий должен ответить значением, вычисленным с использованием своего долговременного ключа , и, тем самым, проверить себя. Следующие протоколы отвечают нашим требованиям:

  • AKEP1 и AKEP2 [10]
  • Протоколы Сигма и Шнорра [26],
  • Протоколы аутентификации с нулевым разглашением [27],
  • Парольные протоколы с нулевым разглашением [28],
  • Протоколы аутентификации, основанные на схеме подписи.

В этом отношении, наш компилятор может даже повысить безопасность протокола аутентификации. Это относится к аутентификации как обеих сторон, так и только одной из них.

Пусть будет протоколом аутентификации, как показано на рисунке. Тогда обозначим через значение (задачу), которая отправляется от к , и через — значение (ответ), возвращенный стороне и позволяющий проверить подлинность стороны . Значения и определены аналогично. Основная идея в конструкции измененного протокола аутентификации — передать и в соответствии со спецификацией протокола , но вычислить ответ, основываясь на полученном сообщении, стенограмме протокола соглашения о ключе и секретном значении . Это выполняется с помощью случайного оракула . Наш компилятор , принимающий на вход протокол соглашения о ключе , защищенный от пассивных противников, и безопасный протокол аутентификации , возвращает протокол обмена ключами с аутентификацией , работающий следующим образом:

A&KE-2 компилятор: Пусть и будут двумя парами оракулов для и .

  1. выполняется оракулами и без каких-либо изменений. Полученное в результате секретное значение — для и для . (Идеально — , но мы должны брать в расчет действия противника.) Ключ сессии (, соотв.) используется для шифрования и проверки целостности, а секретный ключ (, соотв.) отправляется локально процессам и вместе со стенограммой сообщений протокола . (Значения и вычисляются как показано в разделе 3.)
  2. Теперь выполняется оракулами и со следующим изменением: в вычислении и значения и заменяются и , и, таким образом, мы получаем и , где — случайный оракул. Если "принимает", локально возвращается (, соотв.)
TemplateTheoremIcon.svg Теорема Лемма 3
Если - протокол соглашения о ключе защищен от пассивных врагов, то невозможна такая ситуация, при которой три различных оракула "принимаю" с одинаковым (секретным) состоянием , где - секретное значение, полученное протоколом , а - стенограмма всех сообщений протокола.
Доказательство
Если бы это было так, то , и (активный) противник могли бы вычислить , но противник не изменил ни одно сообщения обмена между и (так как стенограммы идентичны). Таким образом, , действующий как пассивный противник, может вычислить , противоречие.


TemplateTheoremIcon.svg Теорема Лемма 4
В любые два согласованные оракула и имеют доступ к уникальному случайному оракулу, который определяется как . Ни , ни любой другой оракул не имеет доступа к этому случайному оракулу.
Доказательство
Так как пара уникальна для любой пары оракулов, тоже уникален.


TemplateTheoremIcon.svg Теорема Теорема 2
Если - безопасный протокол аутентификации, то , как показано на рисунке, также является безопасным протоколом аутентификации.
Доказательство

Пусть и - два процесса (оракула) для и для протокола . Должно быть очевидно, что если и согласованы, то оба оракула "принимают".

Мы должны показать, что вероятность того, что и "принимают" без согласования, незначительна. Теперь предположим, что, напротив, существует противник такой, что может заставить и принять без согласования с непренебрежимой вероятностью . Тогда мы можем определить противника , который достигает той же цели в протоколе : так как не имеет доступа к случайному оракулу , он может толко предположить значений (, соотв.). Теперь , игнорируя задачу , просто выбирает случайную задачу и пытается вычислить для этой задачи. Эта стратегия успешна для непренебрежимой вероятности , поэтому мы получаем противоречие с нашим предположением, что - безопасный протокол.


TemplateTheoremIcon.svg Теорема Теорема 3
Если - протокол соглашения о ключе, защищенный от пассивных противников и - безопасный протокол аутентификации, то - безопасный протокол обмена ключами с аутентификацией.
Доказательство
и принимают в тогда и только тогда, когда они имеют доступ к одному и тому же случайному оракулу . (В противном случае они могут только делать предположения о задаче , что возможно лишь с незначительной вероятностью.) Если они имеют доступ к одному и тому же случайному оракулу, то и завершаются с одним и тем же состоянием . Если и принимают, и , и завершаются одними и теми же конечными точками и . Это исключает возможность активных атак на (так как стенограмма неизменна), и UKS атак на . Таким образом, может провести только пассивную атаку на , вероятность успеха которой пренебрежем мала.


Примечания

  1. На первый взгляд, кажется, что безопасность TLS в качестве протокола согласования ключа может быть легко доказана в модели Беллара-Роджея, поскольку мы должны рассмотреть только пассивных противников, и набор TLS, например, включает в себя эфемерный ключ обмена Диффи-Хеллмана. Тем не менее, есть некоторые тонкости с Reveal-запросом и с тем фактом, что финальное сообщение рукопожатия TLS уже зашифровано. Поэтому до сих пор неясно, вписывается ли TLS в нашу теоретическую базу.
  2. Напротив, протокол может быть разработан таким образом, что сторона, принимающая последнее сообщение "принимает", только если было получено корректное сообщение в соответствии со спецификацией протокола.
  3. Обратите внимание, что здесь мы неявно предполагаем, что пространство возвращенного протоколом KE ключа совпадает с пространством входного ключа для PRF. Этот факт важен не только для правильности, но также для доказательства безопасности.

Реквизиты

Перфильев Сергей Сергеевич, МГТУ им. Н.Э. Баумана, ИУ-8, e-mail:s.perfilev@bmstu.net

Литература

  1. 1,0 1,1 1,2 1,3 Mihir Bellare,Ran Canetti, and Hugo Krawczyk. A moduler approach to the design and analysis of authentication and key exchange protocols (extended abstract). In STOC, pages 419–428, 1998
  2. 2,0 2,1 2,2 Jonathan Katz and Moti Yung. Scalable protocols for authenticated group key exchange. In CRYPTO, pages 110–125. Springer, 2003
  3. Sebastian Gajek, Mark Manulis, Olivier Pereira, Ahmad-Reza Sadeghi, and Jo ̈rg Schwenk. Universally composable security analysis of TLS. In ProvSec, pages 313–327. Springer, 2008
  4. 4,0 4,1 Paul Morrissey, Nigel P. Smart, and Bogdan Warinschi. A modular security analy- sis of the TLS handshake protocol. In ASIACRYPT, pages 55–73. Springer, 2008
  5. Rachna Dhamija, J. D. Tygar, and Marti A. Hearst. Why phishing works. In Rebecca E. Grinter, Tom Rodden, Paul M. Aoki, Edward Cutrell, Robin Jeffries, and Gary M. Olson, editors, CHI, pages 581–590. ACM, 2006
  6. Sebastian Gajek, Tibor Jager, Mark Manulis, and J ̈org Schwenk. A browser-based kerberos authentication scheme. In ESORICS, pages 115–129. Springer, 2008
  7. 7,0 7,1 7,2 Kim-Kwang Raymond Choo, Colin Boyd, and Yvonne Hitchcock. Errors in computational complexity proofs for protocols. In ASIACRYPT, pages 624–643. Springer, 2005
  8. 8,0 8,1 8,2 Kim-Kwang Raymond Choo, Colin Boyd, and Yvonne Hitchcock. Examining indistinguishability-based proof models for key establishment protocols. In ASIACRYPT, pages 585–604. Springer, 2005
  9. 9,0 9,1 9,2 Kim-Kwang Raymond Choo, Colin Boyd, and Yvonne Hitchcock. On session key construction in provably-secure key establishment protocols. In Mycrypt, pages 116–131. Springer, 2005
  10. 10,0 10,1 10,2 10,3 10,4 10,5 10,6 10,7 Mihir Bellare and Phillip Rogaway. Entity authentication and key distribution. In CRYPTO, pages 232–249. Springer, 1993
  11. Emmanuel Bresson, Olivier Chevassut, David Pointcheval, and Jean-Jacques Quisquater. Provably authenticated group Diffie-Hellman key exchange. In ACM Conference on Computer and Communications Security, pages 255–264, 2001
  12. Emmanuel Bresson, Olivier Chevassut, and David Pointcheval. Dynamic group Diffie-Hellman key exchange under standard assumptions. In EUROCRYPT, pages 321–336. Springer, 2002
  13. Emmanuel Bresson and Mark Manulis. Securing group key exchange against strong corruptions. In Masayuki Abe and Virgil D. Gligor, editors, ASIACCS, pages 249– 260. ACM, 2008
  14. 14,0 14,1 14,2 Ran Canetti and Hugo Krawczyk. Analysis of key-exchange protocols and their use for building secure channels. In EUROCRYPT, pages 453–474. Springer, 2001
  15. 15,0 15,1 Hugo Krawczyk. HMQV: A high-performance secure Diffie-Hellman protocol. In CRYPTO, pages 546–566. Springer, 2005
  16. 16,0 16,1 16,2 Brian A. LaMacchia, Kristin Lauter, and Anton Mityagin. Stronger security of authenticated key exchange. In ProvSec, pages 1–16. Springer, 2007
  17. Ran Canetti and Hugo Krawczyk. Security analysis of IKE’s signature-based key-exchange protocol. In CRYPTO, pages 143–161. Springer, 2002
  18. Simon Blake-Wilson and Alfred Menezes. Unknown key-share attacks on the station-to-station (STS) protocol. In Public Key Cryptography, pages 154–170, 1999
  19. Cas J. F. Cremers. Session-state reveal is stronger than ephemeral key reveal: Attacking the NAXOS authenticated key exchange protocol. In ACNS, pages 20–33, 2009
  20. V. Shoup. On formal models for secure key exchange. IBM Research Report RZ, 3120, 1999
  21. Colin Boyd and Anish Mathuria. Protocols for Authentication and Key Establishment. Springer, 1 edition, September 2003
  22. Whitfield Diffie and Martin Hellman. New directions in cryptography. IEEE Transactions on Information Theory, 22:644–654, 1976
  23. Tibor Jager, Florian Kohlar, Sven Scha ̈ge, and Jo ̈rg Schwenk. Generic compilers for authenticated key exchange. Full version. To appear on eprint http://eprint.iacr.org/, 2010
  24. Mihir Bellare and Phillip Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In EUROCRYPT, pages 409–426. Springer, 2006
  25. Victor Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, Nov 2004
  26. Claus P. Schnorr. Efficient identification and signatures for smart cards. In CRYPTO, pages 239–252. Springer, 1989
  27. J. Brandt, I. B. Damg ̊ard, P. Landrock, and T. Pedersen. Zero-knowledge authen- tication scheme with secret key exchange. In CRYPTO, pages 583–588. Springer, 1990
  28. Steven M. Bellovin and Michael Merritt. Encrypted key exchange: Password- based protocols secure against dictionary attacks. In IEEE SYMPOSIUM ON RESEARCH IN SECURITY AND PRIVACY, pages 72–84, 1992