Криптографический протокол

Криптографический протокол — это абстрактный или конкретный протокол , который выполняет функцию, связанную с безопасностью , и применяет криптографические методы, часто в виде последовательностей криптографических примитивов . Протокол описывает, как следует использовать алгоритмы , и включает подробную информацию о структурах и представлениях данных, после чего его можно использовать для реализации нескольких совместимых версий программы. ^[1]

Криптографические протоколы широко используются для безопасной передачи данных на уровне приложений. Криптографический протокол обычно включает в себя по крайней мере некоторые из этих аспектов:

Ключевое соглашение или учреждение
объекта Аутентификация
симметричного шифрования и аутентификации сообщений Конструкция материала
Защищенная передача данных на уровне приложений
неопровержения Методы
обмена секретами Методы
Безопасные многосторонние вычисления

Например, Transport Layer Security (TLS) — это криптографический протокол, используемый для защиты веб-соединений ( HTTPS ). ^[2] Он имеет механизм аутентификации объекта, основанный на системе X.509 ; этап установки ключа, на котором симметричный ключ шифрования формируется с использованием криптографии с открытым ключом; и функция транспортировки данных на уровне приложения. Эти три аспекта имеют важные взаимосвязи. Стандартный TLS не имеет поддержки неотказуемости.

Существуют и другие типы криптографических протоколов, и даже сам термин имеет различное прочтение; Протоколы криптографических приложений часто используют один или несколько основных методов согласования ключей , которые также иногда называют «криптографическими протоколами». Например, TLS использует так называемый обмен ключами Диффи-Хеллмана , который, хотя и является лишь частью TLS как таковой , Диффи-Хеллмана сам по себе можно рассматривать как полноценный криптографический протокол для других приложений.

Расширенные криптографические протоколы

Широкий спектр криптографических протоколов выходит за рамки традиционных целей конфиденциальности, целостности и аутентификации данных, а также обеспечивает множество других желаемых характеристик компьютерного сотрудничества. ^[3] Слепые подписи могут использоваться для цифровых денег и цифровых учетных данных, чтобы доказать, что лицо обладает атрибутом или правом, не раскрывая личность этого человека или личности сторон, с которыми это лицо совершало транзакции. Безопасную цифровую метку времени можно использовать для доказательства того, что данные (даже если они конфиденциальные) существовали в определенное время. Безопасные многосторонние вычисления могут использоваться для вычисления ответов (например, определения самой высокой ставки на аукционе) на основе конфиденциальных данных (например, частных ставок), так что после завершения протокола участники будут знать только свои собственные данные и ответ. Комплексные проверяемые системы голосования обеспечивают набор желаемых свойств конфиденциальности и проверяемости для проведения электронного голосования . Неоспоримые подписи включают интерактивные протоколы, которые позволяют подписавшему доказать подделку и ограничивают круг лиц, которые могут проверить подпись. Отклоняемое шифрование дополняет стандартное шифрование, делая невозможным для злоумышленника математически доказать существование простого текстового сообщения. Цифровые миксы создают трудно отслеживаемые коммуникации.

Формальная проверка

Криптографические протоколы иногда можно проверить формально на абстрактном уровне. Когда это будет сделано, возникает необходимость формализовать среду, в которой работает протокол, для выявления угроз. Это часто делается с помощью модели Долева-Яо .

Логика, концепции и расчеты, используемые для формального обоснования протоколов безопасности:

Логика Берроуза – Абади – Нидхэма (логика БАН)
Модель Долева – Яо
π-исчисление
Логика композиции протокола (PCL)
Прядное пространство ^[4]

Исследовательские проекты и инструменты, используемые для формальной верификации протоколов безопасности:

Автоматизированная проверка протоколов и приложений интернет-безопасности (AVISPA) и последующий проект AVANTSSAR. ^[5]^[6]
- Поиск атак на основе логики ограничений (CL-AtSe) ^[7]
- Средство проверки моделей с фиксированной точкой с открытым исходным кодом (OFMC) ^[8]
- Средство проверки моделей на основе SAT (SATMC) ^[9]
Каспер ^[10]
КриптоВериф
Анализатор форм криптографических протоколов (CPSA) ^[11]
Знания в протоколах безопасности (KISS) ^[12]
Анализатор протоколов Maude-NRL (Maude-NPA) ^[13]
ProVerif
Скайтер ^[14]
Образцы тамарина ^[15]

Понятие абстрактного протокола

Для формальной проверки протокола его часто абстрагируют и моделируют с использованием нотации Алисы и Боба . Простой пример:

A\rightarrow B:\{X\}_{K_{A,B}}

Это говорит о том, что Алиса $A$ намеревается передать сообщение Бобу $B$ состоящий из сообщения $X$ зашифровано общим ключом $K_{A,B}$ .

Примеры

См. также

Ссылки

^ «Обзор криптографического протокола» (PDF) . 23 октября 2015 г. Архивировано из оригинала (PDF) 29 августа 2017 г. Проверено 23 октября 2015 г.
^ Чен, Шан; Джеро, Сэмюэл; Ягельский, Мэтью; Болдырева Александра; Нита-Ротару, Кристина (01 июля 2021 г.). «Установление безопасного канала связи: TLS 1.3 (через TCP Fast Open) и QUIC» . Журнал криптологии . 34 (3): 26. дои : 10.1007/s00145-021-09389-w . ISSN 0933-2790 . S2CID 235174220 .
^ Берри Шонмейкерс. «Конспекты лекций по криптографическим протоколам» (PDF) .
^ Фабрега, Ф. Хавьер Тайер, Джонатан К. Херцог и Джошуа Д. Гуттман, Strand Spaces: Почему протокол безопасности правильный? {{citation}}: CS1 maint: несколько имен: список авторов ( ссылка )
^ «Автоматическая проверка протоколов и приложений интернет-безопасности (AVISPA)» . Архивировано из оригинала 22 сентября 2016 года . Проверено 14 февраля 2024 г.
^ Армандо, А.; Арсак, В; Аванесов Т.; Барлетта, М.; Кальви, А.; Каппай, А.; Карбоне, Р.; Шевалье, Ю.; +12 еще (2012). Фланаган, К.; Кениг, Б. (ред.). Платформа AVANTSSAR для автоматической проверки доверия и безопасности сервис-ориентированных архитектур . Том. 7214. ЛНТКС. стр. 267–282. дои : 10.1007/978-3-642-28756-5_19 . Проверено 14 февраля 2024 г. {{cite book}}: CS1 maint: числовые имена: список авторов ( ссылка )
^ «Поиск атак на основе логики ограничений (Cl-AtSe)» . Архивировано из оригинала 8 февраля 2017 г. Проверено 17 октября 2016 г.
^ Средство проверки моделей с фиксированной точкой с открытым исходным кодом (OFMC)
^ «Проверка моделей на основе SAT для протоколов безопасности и приложений, чувствительных к безопасности (SATMC)» . Архивировано из оригинала 3 октября 2015 г. Проверено 17 октября 2016 г.
^ Casper: компилятор для анализа протоколов безопасности
^ cpsa: Анализатор символьных криптографических протоколов.
^ «Знания в протоколах безопасности (KISS)» . Архивировано из оригинала 10 октября 2016 г. Проверено 7 октября 2016 г.
^ Анализатор протоколов Maude-NRL (Maude-NPA)
^ Скайтер
^ Образцы тамарина

Дальнейшее чтение

Ермошина, Ксения; Мусиани, Франческа; Халпин, Гарри (сентябрь 2016 г.). «Протоколы обмена сообщениями со сквозным шифрованием: обзор» (PDF) . В Баньоли, Франко; и др. (ред.). Интернет-наука . INSCI 2016. Флоренция, Италия: Springer. стр. 244–254. дои : 10.1007/978-3-319-45982-0_22 . ISBN 978-3-319-45982-0 .

[1] «Обзор криптографического протокола» (PDF) . 23 октября 2015 г. Архивировано из оригинала (PDF) 29 августа 2017 г. Проверено 23 октября 2015 г.

[2] Чен, Шан; Джеро, Сэмюэл; Ягельский, Мэтью; Болдырева Александра; Нита-Ротару, Кристина (01 июля 2021 г.). «Установление безопасного канала связи: TLS 1.3 (через TCP Fast Open) и QUIC» . Журнал криптологии . 34 (3): 26. дои : 10.1007/s00145-021-09389-w . ISSN 0933-2790 . S2CID 235174220 .

[3] Берри Шонмейкерс. «Конспекты лекций по криптографическим протоколам» (PDF) .

[4] Фабрега, Ф. Хавьер Тайер, Джонатан К. Херцог и Джошуа Д. Гуттман, Strand Spaces: Почему протокол безопасности правильный? {{citation}}: CS1 maint: несколько имен: список авторов ( ссылка )

[5] «Автоматическая проверка протоколов и приложений интернет-безопасности (AVISPA)» . Архивировано из оригинала 22 сентября 2016 года . Проверено 14 февраля 2024 г.

[TAP_1-6] Армандо, А.; Арсак, В; Аванесов Т.; Барлетта, М.; Кальви, А.; Каппай, А.; Карбоне, Р.; Шевалье, Ю.; +12 еще (2012). Фланаган, К.; Кениг, Б. (ред.). Платформа AVANTSSAR для автоматической проверки доверия и безопасности сервис-ориентированных архитектур . Том. 7214. ЛНТКС. стр. 267–282. дои : 10.1007/978-3-642-28756-5_19 . Проверено 14 февраля 2024 г. {{cite book}}: CS1 maint: числовые имена: список авторов ( ссылка )

[7] «Поиск атак на основе логики ограничений (Cl-AtSe)» . Архивировано из оригинала 8 февраля 2017 г. Проверено 17 октября 2016 г.

[8] Средство проверки моделей с фиксированной точкой с открытым исходным кодом (OFMC)

[9] «Проверка моделей на основе SAT для протоколов безопасности и приложений, чувствительных к безопасности (SATMC)» . Архивировано из оригинала 3 октября 2015 г. Проверено 17 октября 2016 г.

[10] Casper: компилятор для анализа протоколов безопасности

[11] sa: Анализатор символьных криптографических протоколов.

[12] «Знания в протоколах безопасности (KISS)» . Архивировано из оригинала 10 октября 2016 г. Проверено 7 октября 2016 г.

[13] Анализатор протоколов Maude-NRL (Maude-NPA)

[14] Скайтер

[15] Образцы тамарина

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]