Существуют ли современные (после Второй мировой войны) и известные протоколы, которые доказали свою безопасность (в любой модели: игровой, UC...), но чьи доказательства были ошибочными и могли привести к атакам в реальном мире?

Обратите внимание, что:

• Меня не особенно беспокоят атаки на сами математические предположения (которые, кажется, находятся в центре внимания эта тема, и не могут считаться ошибками в доказательстве: это «просто» неудачные предположения). Но, конечно, я хотел бы услышать о протоколах, которые утверждали, что они безопасны, как только предположение X было верным, хотя на самом деле они были взломаны, несмотря на то, что X не был взломан.
• Под «атакой в ​​​​реальном мире» я бы предпочел атаки, которые нарушают протоколы, используемые на практике конечными пользователями-неспециалистами, но я также согласен с хорошо известными протоколами, которые в основном известны и используются в академическом мире.

В идеале я хотел бы узнать, действительно ли «ошибка» в доказательстве была ошибкой или, вероятно, была создана намеренно (лазейка АНБ...).

РЕДАКТИРОВАТЬ

Не могли бы вы также быть точны, когда это возможно, если атака вызвана ошибкой в ​​самом доказательстве или если модель безопасности выбрана неправильно?

Возможно "Атаки с восстановлением открытого текста против SSH"подходит?

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

Тогда см. "Избыток наборов шифров SSH"для продолжения.

Возможно, мы можем рассчитывать на первый международный стандарт цифровой подписи, ИСО/МЭК 9796:1991, в котором указана подпись RSA и Рабина с использованием избыточного заполнения сообщения для подписи. Безопасность была оправдана тогдашним современное обоснование, опубликовано в разбирательства Eurocrypt 1990. В нем указаны свойства заполнения подписи стандарта. необходимый для безопасности, несмотря на мультипликативное свойство необработанной функции RSA $x\mapsto x^d\bmod n$, нравиться:

• Смещение или дополнение репрезентативных элементов не приводит к другим.
• Произведение любого репрезентативного элемента на любую константу, отличную от 1, не является репрезентативным элементом.

Эти свойства соответствуют действительности. Но они не являются доказательством безопасности в современном понимании этого слова. Они лишь доказывают невозможность некоторый нападения, а не Любые атака.

И в 1999 году был найден¹ недорогой в вычислительном отношении метод, показывающий большие классы сообщений, так что подпись одного из них можно найти, отправив другое (иногда сначала три) для подписи RSA; или закрытый ключ найден (полный разрыв) путем отправки двух сообщений на подпись Рабина. Год спустя стандарт был отменен.

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

Аналогичный пример ИСО/МЭК 9796-2:1997 подпись (но с еще меньшими требованиями безопасности). Сломлено атакой: Жан-Себастьян Корон, Давид Наккаш, Мехди Тибуши, Ральф-Филипп Вайнманн Практический криптоанализ подписей ISO 9796-2 и EMV, в Журнал криптологии (2015), а ранее в материалы Crypto 2009. Эта схема широко используется в банковских смарт-картах с параметрами, позволяющими вычислить несколько сотен тысяч сообщений, так что должен противнику удается получить подписи всех, кроме одной, что позволяет найти подпись последнего сообщения. Но она не может выродиться в практическую эксплуатацию.

¹ Справочный документ по атакам Дон Копперсмит, Жан-Себастьян Корон, Франсуа Грие, Шай Халеви, Чаранджит Ютла, Дэвид Наккаш, Жюльен П. Стерн: Криптоанализ ISO/IEC 9796-1, в Журнал криптологии (2007). Он перегруппировывает более ранние атаки:

• Новая стратегия подделки подписи, применимая к ISO 9796–1/2, ECASH–, PKCS#1 V2.0, ANSI X9.31, SSL-3.02., доклад эксперта ISO/IEC JTC1/SC27 (1999), который показал путь атаки, который оказался неприменимым напрямую к стандарту из-за однобитовой детали.
• ISO 9796-1 и новая стратегия борьбы с подделкой документов (рабочий проект) улучшает эту стратегию, чтобы соответствовать полному стандарту, но требует много избранных сообщений.
• Атака выбранных сообщений на схему подписи ISO/IEC 9796-1 (слайды) использует другую стратегию, которая работает с небольшим количеством сообщений и делает их поиск недорогим.

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

• Атаки с переустановкой ключа: принудительное повторное использование одноразового номера в WPA Мэти Ванхуф и Фрэнк Писсенс

С их сайта

Было математически доказано, что четырехстороннее рукопожатие безопасно. Как возможна ваша атака?

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

Более длинный ответ упоминается во введении к нашему исследованию: наши атаки не нарушают свойств безопасности, доказанных в формальном анализе четырехэтапного рукопожатия. В частности, в этих доказательствах указано, что согласованный ключ шифрования остается закрытым и что личность клиента и точки доступа (AP) подтверждена. Наши атаки не приводят к утечке ключа шифрования. Кроме того, хотя обычные кадры данных могут быть подделаны, если используется TKIP или GCMP, злоумышленник не может подделать сообщения рукопожатия и, следовательно, не может олицетворять клиента или точку доступа во время рукопожатия. Следовательно, свойства, доказанные при формальном анализе четырехэтапного рукопожатия, остаются в силе. Однако проблема в том, что пруфы не моделируют установку ключа. Иными словами, формальные модели не определяли, когда следует устанавливать согласованный ключ. На практике это означает, что один и тот же ключ может быть установлен несколько раз, тем самым сбрасывая одноразовые номера и счетчики воспроизведения, используемые протоколом шифрования (например, WPA-TKIP или AES-CCMP).

Клипер Чип с Скипджек Шифр

Это может оказаться менее вероятным, чем вы предполагали, поскольку «вектор атаки в реальном мире» может оказаться не очень полезным для атаки, так как только AT&T TSD-3600-E было известно, что устройство реализовало это для этого, и большинство других устройств, по-видимому, было куплено только Министерством юстиции США. Тем не менее, это может помочь уточнить комментарий @Kevin о том, как побочные каналы чаще становятся векторами атаки для указанных алгоритмов, учитывая наиболее известную причину, по которой они больше не используются.

Чип Clipper и поле доступа для правоохранительных органов (LEAF)

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

Позже были обнаружены 2 основные проблемы:

1.) Мэтт Блейз в 1994 году обнаружил, что можно использовать тот факт, что Системе LEAF требуется 16-битный хэш для ключа шифрования, чтобы убедиться, что это действительное сообщение для шифрования. (чтобы его можно было расшифровать), можно было в течение ~ 30-50 минут подобрать новую 16-битную контрольную сумму для другого ключа шифрования, отличного от того, который использовался для шифрования сообщения, эффективно обходя шаг «Расшифровать при необходимости». .

2.) Яир Франкель и Моти Юнг в 1995 году обнаружили, что можно использовать Устройство с поддержкой LEAF для создания проверки, прикрепленной к сообщениям, зашифрованным на другом устройстве., тем самым минуя шаг «Расшифровывается при необходимости» в режиме реального времени.

В конечном счете, именно эти проблемы, скорее всего, приведут к отказу от использования этого метода, поскольку правительство США является наиболее заметным крупнейшим покупателем AT&T TSD-3600-E. Я не знаю, сколько из них было фактически использовано в результате, поскольку, как сообщается, большинство коробок остались неоткрытыми. Что оставляет нас относительно фактического шифра Skipjack.

Скипджек

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

Труднее доказать, что он был признан безопасным, учитывая, что изначально он был засекречен, но ... Ученые-исследователи были привлечены для оценки Skipjack и обнаружили, что «Таким образом, нет значительного риска того, что SKIPJACK будет взломан исчерпывающим поиском в ближайшие 30-40 лет».

25 июня 1998 года, когда Skipjack был рассекречен, Эли Бихам и Ади Шамир обнаружил, что при Skipjack уменьшается до 16 вместо 32 патронов, его можно было взломать с помощью обнаруженного в то время вектора атаки. Позже, в 1999 году, с Алексеем Бирюковым они смогли увеличить его до 31 из 32 раундов.

По-видимому, по состоянию на 2009 год полный прорыв всех 32 раундов не был полностью нарушен, но это, по-видимому, указывает на то, что первоначальное доказательство могло быть неверным, учитывая, что первые 31 раунд 32-раундового Скипджека полагались в первую очередь на классификация алгоритма того времени.

Как сказал @Kevin в своем комментарии к вопросу выше, в первую очередь боковые каналы были бы способом сломать его - и в этом случае чип Clipper и сам его протокол LEAF оказались более слабым звеном - взлом протокола, который мог бы использовался для расшифровки базовых зашифрованных сообщений, когда это было оправдано.

В 2019 году в Zcash была обнаружена уязвимость для подделки денег [см. здесь].

До исправления злоумышленник мог создать поддельный Zcash, не будучи обнаруженным!

При текущей рыночной капитализации в $1,7 млрд кажется, что Zcash, по крайней мере сегодня, пользуются широким распространением за пределами нескольких пользователей-специалистов. Уязвимость связана с тонкой криптографической уязвимостью в [БКТВ14], в котором описывается конструкция zk-SNARK, использовавшаяся при первоначальном запуске Zcash. Уязвимость настолько незаметна, что не подвергалась многолетнему анализу со стороны экспертов по криптографии. Более того, некоторые последующие работы известных исследователей также унаследовали тот же недостаток.

Важно отметить, что [БКТВ14] конструкция не имела специального доказательства безопасности, как указано в [Парно15], и полагался в основном на [PGHR13] доказательство безопасности и сходство между двумя схемами. Команда компании Zcash действительно пыталась написать доказательство безопасности в [БГГ17], но не обнаружил эту уязвимость. Zcash с тех пор перешел на новую систему доказывания [Грот16] который имеет несколько независимые доказательства и значительно лучший анализ.

Для подавляющего большинства современных криптографических алгоритмов нет строгого математического доказательства их безопасности. Чаще всего, когда такое доказательство публикуется или обсуждается, оно основывается на предположения которые просто считаются истинными. Если эти предположения не выполняются, доказательство разваливается, даже если в нем нет ошибок. Например, безопасность тройного DES была основана на предположении, что обычный DES безопасен (хотя и с размером ключа, недостаточным для предотвращения атак грубой силы). Если бы в DES была обнаружена серьезная уязвимость, это, вероятно, также поставило бы под угрозу безопасность 3DES.

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

Вышеуказанные два пункта добавляются к банальным ошибкам в логике доказательства.

Таким образом, в зависимости от уровня доказательства, который вы считаете достаточным, вы можете сказать, что никто из известных протоколов реального мира когда-либо были признаны безопасными, или что те протоколы, которые позже были взломаны, в какой-то момент были «доказаны» безопасными (иначе они не использовались бы), но доказательство не состоялось.