Протокол Needham—Schroeder и атаки

Протокол Needham–Schroeder (1978) был одной из первых формальных попыток разработать протокол криптографической аутентификации с использованием доверенной третьей стороны (TTP). Цель состояла в том, чтобы позволить двум сторонам, Alice и Bob, взаимно аутентифицироваться и установить общий ключ сеанса с помощью доверенного сервера аутентификации (AS), который совместно использует долгосрочные ключи с каждым участником. Этот протокол появился до инфраструктуры открытых ключей, но ввёл такие понятия, как одноразовые значения для обеспечения свежести и распределение ключей через доверенный сервер, которые по-прежнему лежат в основе современных протоколов, например Kerberos. Понимание NS и его недостатков сформировало всю область анализа протоколов.

Протокол симметричных ключей NS выполняется в пять шагов. (1) Alice отправляет AS сообщение {A, B, Na}, запрашивая ключ сеанса для связи с Bob. (2) AS отвечает Alice сообщением {Na, B, Kab, {Kab, A}_Kb}_Ka — ключом сеанса Kab и билетом для Bob, причём всё сообщение зашифровано долгосрочным ключом Alice Ka. (3) Alice пересылает Bob билет {Kab, A}_Kb. (4) Bob расшифровывает билет, извлекает Kab и отправляет Alice {Nb}_Kab — испытание. (5) Alice отвечает {Nb-1}_Kab, доказывая, что владеет Kab. Одноразовое значение Nb предотвращает повторную передачу шага 4. В этом протоколе известна атака повторной передачи, описанная Denning и Sacco (1981).

Denning и Sacco (1981) обнаружили недостаток: ответ AS на шаге 2 не содержит новых данных — в нём нет временной отметки или одноразового значения, добавленных сервером. Злоумышленник Mallory, ранее перехвативший старый ключ сеанса Kab (скомпрометировав прошлый сеанс), может в любой момент повторно отправить Bob старый билет {Kab, A}_Kb. Получив билет, который выглядит как легитимный билет от Alice, Bob использует скомпрометированный ключ Kab для сеанса. Исправление Denning и Sacco состояло в добавлении временной отметки в ответ AS и билет. Этот подход был принят в Kerberos: временные отметки встраиваются в билеты, чтобы ограничить период их действия.

Протокол NS с открытым ключом (также разработанный в 1978 году) предназначен для взаимной аутентификации двух сторон с использованием криптографии с открытым ключом. (1) Alice отправляет Bob сообщение {Na, A}_PKb — одноразовое значение Na, зашифрованное открытым ключом Bob. (2) Bob отвечает {Na, Nb}_PKa — оба одноразовых значения, зашифрованные открытым ключом Alice. (3) Alice отвечает {Nb}_PKb, возвращая одноразовое значение Bob, зашифрованное его открытым ключом. После этого обмена обе стороны владеют обоими одноразовыми значениями (Na, Nb) и могут вывести ключ сеанса. Протокол считался безопасным в течение 17 лет — до атаки Lowe 1995 года.

Gavin Lowe (1995) обнаружил критический недостаток с помощью средства проверки моделей FDR (анализ отказов при композиционном рассуждении). Mallory может выдать себя за Bob перед Alice, одновременно пересылая сообщения настоящему Bob. Шаг 1: Alice отправляет {Na, A}_PKm Mallory, полагая, что общается с Bob. Mallory пересылает {Na, A}_PKb Bob. Шаг 2: Bob отвечает {Na, Nb}_PKa, а Mallory расшифровывает это сообщение и повторно шифрует его для Alice: {Na, Nb}_PKa. Alice расшифровывает сообщение и извлекает Nb. Шаг 3: Alice отправляет {Nb}_PKm, считая, что сообщение предназначено Bob. Mallory расшифровывает его и пересылает {Nb}_PKb Bob. Bob считает, что завершил взаимную аутентификацию с Alice, однако на самом деле Alice аутентифицируется с Mallory. Исправление: на шаге 2 Bob должен включить собственный идентификатор: {Na, Nb, B}_PKa.

Исправление Лоу в протоколе NSPK простое, но принципиально важное: ответ Боба на шаге 2 должен включать идентичность Боба B, то есть {Na, Nb, B}_PKa. Теперь, получив ответ, Алиса проверяет, что указанная идентичность B соответствует стороне, с которой она намеревалась связаться. Мэллори не может подменить этот ответ своим: ему потребовался бы закрытый ключ Алисы, чтобы сформировать корректное {Na, Nb, M}_PKa, которое прошло бы проверку Алисы. Этот подход обобщён в принципе Нидхэма—Абади: аутентификационные сообщения должны явно связывать идентичность отправителя с сообщением, а не полагаться при идентификации только на контекст.

Обнаружению уязвимости NSPK Лоу помогло средство проверки моделей FDR (уточнение по отказам и расхождениям), которое исчерпывающе исследует все возможные выполнения протокола, включая вмешательство злоумышленника. Это стимулировало развитие средств формального анализа протоколов: ProVerif (основанный на прикладном π-исчислении) может доказывать или опровергать свойства аутентификации и секретности в бесконечных сеансах. Средство проверки Tamarin использует переписывание мультимножеств и поддерживает сложные протоколы, такие как TLS 1.3 и Signal. AVISPA и Scyther — другие средства. Современные разработки протоколов (TLS 1.3, Signal, Noise) проходят формальную проверку до развертывания — прямое наследие эпизода с NS и Лоу.

Атаки NS прояснили различие между целями аутентификации. Аутентификация сущности: доказательство того, что сторона в данный момент активна и участвует в протоколе (важна свежесть). Аутентификация происхождения данных: доказательство того, что конкретное сообщение создано конкретной стороной (это не обязательно означает, что сторона активна). Атака Лоу нарушает аутентификацию сущности: Алиса считает, что проходит аутентификацию с Бобом, но фактически аутентифицируется с Мэллори, который пересылает сообщения Бобу. Современные спецификации протоколов точно формулируют цели: «Боб аутентифицировал Алису как инициатора этого сеанса». Расплывчатые цели приводят к неоднозначным спецификациям, которые проходят неформальную проверку, но не выдерживают формального анализа.

Ещё один класс атак, связанных с NS, — атака отражения: Мэллори повторно отправляет Алисе сообщения Алисы. Если протокол симметричен (обе стороны используют один и тот же ключ и формат сообщений), Алиса может принять собственный вызов за корректный ответ Боба. Защита: использовать отдельные ключи для разных направлений (разные ключи шифрования и расшифрования для каждого направления) или включать в сообщения маркеры роли (шифрующая сторона включает в сообщение «Я инициатор»). Современные протоколы, такие как TLS, включают в ключи, выведенные с помощью HKDF, строки меток для конкретной роли (используя «c e traffic» для клиента и «s hs traffic» для сервера), чтобы предотвратить отражение.

Атаки с перемежением объединяют сообщения из нескольких параллельных сеансов, чтобы подделать аутентификацию. Если Алиса ведёт два сеанса одновременно, Мэллори может смешать сообщения из обоих и создать согласованный, но недействительный объединённый сеанс, в котором Мэллори будет аутентифицирован. Защита: привязка к сеансу — каждое сообщение должно быть криптографически связано с контекстом своего сеанса (например, содержать идентификатор сеанса или использовать уникальный ключ для каждого сеанса). TLS предотвращает перемежение с помощью сообщения «Завершение», представляющего собой MAC, вычисленный по полной стенограмме текущего сеанса. Любое сообщение, вставленное из другого сеанса, изменяет стенограмму и делает значение «Завершение» недействительным.

Протоколы Нидхэма—Шрёдера напрямую повлияли на разработку Kerberos (метки времени для предотвращения повторной передачи, заимствованные из исправления Деннинга—Сакко), TLS (MAC по стенограмме в сообщении «Завершение» предотвращает перемежение и отражение), протокола Signal (привязка сеанса посредством состояния механизма храповика) и платформы протокола Noise (привязка идентичности в шаблонах установления соединения). Атаки NS показали, что неформальных аргументов безопасности недостаточно: каждый протокол необходимо анализировать с учётом активного злоумышленника, который контролирует сеть и может повторять, менять порядок и изменять сообщения. Эта модель злоумышленника (Долев—Яо) теперь является стандартной при формальной проверке протоколов.

Какое простое изменение Лоу предложил, чтобы исправить уязвимость протокола NS с открытым ключом?

Симметричный протокол Нидхэма—Шрёдера (1978) представил распределение ключей сеанса на основе TTP. Атака Деннинга—Сакко (1981) выявила уязвимость к повторной передаче — её исправили с помощью меток времени в Kerberos. Протокол NSPK с открытым ключом подвергся атаке MITM, обнаруженной Лоу (1995) с помощью проверки моделей, — её исправили включением идентичности отправителя в сообщения. Эти атаки сделали формальную проверку (ProVerif, Tamarin) обязательной частью проектирования протоколов. Основные уроки: сообщения должны связывать идентичность отправителя, сеансы должны быть изолированы друг от друга, атаки отражения предотвращаются выводом ключей с учётом направления, а атаки с перемежением — MAC по стенограммам обмена.