Криптографические протоколы: определения, запись, свойства, классификация, атаки

[saipr]

Честно говоря, мало что понятного и для чего?
И чем Клара или Боб понятнее чем Отправитель и Получатель?
И почему в таблице есть TLS и TLS-v1.1, но нет TLS-v1.2 и TLS-v1.3?
Что этим автор хотел сказать или показать?

[vlsergey]

Алиса, Боб и Клара лучше Отправителя и Получателя по нескольким причинам:

• Использование «Отправитель» в общем случае некорректно вообще, так как на каждом проходе протокола отправитель и получатель различны. Можно было бы заменить «Инициатором», а как назвать второго? Проще для всех протоколов заменить их какими-то общими обозначениями. Но вместо использования «участник 1», «участник 2» фактически используют обозначения «участник A», «участник B» и так далее (по порядку букв в алфавите).
• Буквы A, B, C, как стоящие в начале латинского алфавита, наименее конфликтуют с другими обозначениями (Encrypt, Message, Key, etc.)

[shuhray]

Программа ProVerif для проверки протоколов, пример. Общаются между собой клиент и сервер, подключается хакер и пытается кого-нибудь обмануть. На первой картинке записан протокол (словечки вроде senc и aenc означают разные виды шифрования, symmetric encription, asymmetric encription и т.д.) Запускаем программу ProVerif и она находит способ взлома, который изображён на второй картинке. Вертикальные линии обозначают клиента, сервер и хакера, а горизонтальные стрелки — сообщения, которые они друг другу посылают (обычно шифрованные). Хакер, выдавая себя за клиента, получает от сервера зашифрованный секрет, а потом ловко обманывает клиента, чтобы тот его расшифровал. Взлом ищется перебором (в том числе есть интерактивный инструмент), а вот верификация (подтверждение, что взломать нельзя) доказывается. Используется так называемое пи-исчисление (исчисление процессов). Представьте простые программы (в духе функционального программирования), которые вычисляются параллельно, обмениваясь сообщениями через открытые и приватные каналы. Посылают друг другу зашифрованные сообщения, ключи и т.п. Предполагается, что все сообщения через открытые каналы доступны хакеру. Криптография предполагается надёжной, подбирать пароли не пытаемся, ищем логические ошибки в протоколах. Выписываются формулы типа «если хакер может узнать A, значит, он смог сделать B». Формулы простые в некотором техническом смысле (хорновские формулы). Дальше используется некоторый «проверяльщик выводимости для хорновских формул», на соответствующую математику есть ссылки в документации
prosecco.gforge.inria.fr/personal/bblanche/proverif
prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
Вместе с программой ProVerif скачивается папка с большим числом примеров (папка proverifdoc2.00, в других папках тоже есть, файлы с расширением .pv). Сейчас их читаю (удобно читать в редакторе Atom, к нему есть плагин для proverif) и постепенно разбираюсь.

[pae174]

Табличка сравнения протоколов странная — в части TLS.
TLS 1.1 вообще в следующем году будет уже deprecated.
TLS 1.3 содержит всякие полезные штуки, для которых в табличке вроде бы есть клетки, но там нет крестиков потому что всё там заканчивается на TLS 1.1.

[vlsergey]

В TLS 1.3 «по табличке» стало только обязательным использование PFS (G9), или что-то ещё?

[pae174]

G15 еще. В 1.3 появилось Zero RTT.

В табличке, кстати, все заканчивается на колонке 15 а по тексту там 20 свойств протоколов для сравнения.

[vlsergey]

Под G15 понимается не просто исправление багов, связанных с возможностью DOS-атак, а доказательство того, что целые классы DDOS-атак становятся невозможны для данного протокола. Например, сразу все атаки, связанные с переполнением буфера. Насколько мне известно, пока что в TLS такого не делалось, т.е. никакого формального анализа на отсутствие брешей для DOS не делалось. Или есть какие-то работы на эту тему?

Свойства 16-20 для приведённых протоколов просто неактуальны. G1 уже подразумевает G16, G17-G19 на формальном уровне не закреплено (то есть никто не сертифицировал данные протоколы на эти задачи), ну а G20 это цель прикладного уровня. Хотя в каком-то смысле TLS можно отнести к выполняющим одну задачу по G20 (предъявление сертификата => установление связи), но это всё-таки не совсем бизнес-задача.

[uvelichitel]

Доходчивое изложение. А почему, интересно, весь материал строится а англоязычном лексиконе? Русская школа криптографии вообще существует?

[vlsergey]

Русская школа криптографии существует, но вот с придумыванием своей терминологии у неё не очень. Вплоть до того, что появляются термины вроде «дешифровать», который, с точки зрения некоторых специалистов, вовсе не «расшифровать» (а провести успешную атаку на шифртекст).

Были и попытки использовать Андрея / Бориса в качестве экземплификантов, но не прижились.

[yotec]

Эти «некоторые специалисты» даже составили Словарь криптографических терминов.

[VAE]

Словарь-то составили, но авторам статей иногда перед созданием текстов его следовало бы открывать. Все, что им не подходит — критиковать.
А — то, не прижилось.