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

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

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

• Соглашение о ключах или установление
• Entity аутентификация
• Симметричное шифрование и аутентификация сообщений материальная конструкция
• Защищенная передача данных на уровне приложения
• Сохранение авторства методы
• Совместное использование секретов методы
• Безопасные многосторонние вычисления

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

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

• 1 Расширенные криптографические протоколы
• 2 Формальная проверка
  • 2.1 Понятие абстрактного протокола
• 3 Примеры
• 4 См. Также
• 5 Ссылки
• 6 Дополнительная литература
• 7 Внешние ссылки

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

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

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

• логика Барроуза – Абади – Нидхема (логика BAN)
• Модель Долева – Яо
• π-исчисление
• Состав протокола логика (PCL)
• Strand space

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

• Автоматическая проверка протоколов и приложений безопасности в Интернете (AVISPA) и последующий проект AVANTSSAR
  • Средство поиска атак на основе логических ограничений (CL-AtSe)
  • Средство проверки моделей с фиксированной точкой с открытым исходным кодом (OFMC)
  • Средство проверки моделей на основе SAT (SATMC)
• Casper
• CryptoVerif
• Анализатор форм криптографического протокола (CPSA)
• Знание в протоколах безопасности (KISS)
• Анализатор протокола Maude-NRL (Maude-NPA)
• ProVerif
• Scyther
• Тамарин Прувер

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

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

$A\; \to \; B:\; \{X\}\; KA,\; B\; \{\backslash \; displaystyle\; A\; \backslash \; rightarrow\; B:\; \backslash \; \{X\; \backslash \}\; \_\; \{K\_\; \{A,\; B\}\}\}$

Это означает, что Алиса $A\; \{\backslash \; displaystyle\; A\}$предполагает сообщение для Боба $B\; \{\backslash \; displaystyle\; B\}$, состоящее из сообщения $X\; \{\; \backslash \; displaystyle\; X\}$зашифровано с использованием общего ключа $KA,\; B\; \{\backslash \; displaystyle\; K\_\; \{A,\; B\}\}$.

• Internet Key Exchange
• IPsec
• Kerberos
• Обмен сообщениями без записи
• Протокол точка-точка
• Secure Shell (SSH)
• Протокол сигнала
• Безопасность транспортного уровня
• ZRTP

• Защищенный канал
• Открытый репозиторий протоколов безопасности

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

• Открытый репозиторий защищенных протоколов