Исследователь лаборатории криптографии компании «Криптонит» Кирилл Царегородцев (@kirtsar) сравнил разные подходы к оценке безопасности криптографических протоколов. В качестве примера он использовал протокол 5G-AKA, применяемый для аутентификации в современных сетях мобильной связи.
Представим, что наша задача – разработать протокол связи для мобильного телефона, то есть – описать интерактивный алгоритм его взаимодействия с базовыми станциями в домашней сети. Казалось бы, очевидно, что этот протокол должен быть безопасен для использования и вместе с тем позволять выполнять обычные функции телефона, такие как регистрация в сети, звонки, работа в роуминге и так далее.
Сразу же можно задать вопрос: а что значит «безопасный»? Чего мы хотим добиться? Какие у нас есть для этого изначальные возможности и ресурсы, которыми мы располагаем? От кого именно мы защищаемся – от любопытного соседа, который просто пассивно прослушивает радиоэфир, или от некоторой могущественной спецслужбы, в распоряжении которой могут быть огромные вычислительные мощности и специализированное оборудование? Все эти вопросы не так просты, как может показаться на первый взгляд, и под ними прячется огромное количество подводных камней, на которые легко налететь, если предварительно не ответить (или хотя бы попытаться ответить) на каждый из таких вопросов.
В нашем выступлении на конференции «РусКрипто’2022» мы коснулись лишь одной части этой сложной задачи по обеспечению безопасной связи, а именно, алгоритма 5G-AKA.
Его двумя основными задачами являются выработка сеансового общего секретного ключа между пользователем и домашней сетью (т.н. Authenticated Key Exchange или AKE‑протокол [1]) и явная аутентификация сторон взаимодействия.
Исходными здесь являются следующие положения:
Между телефоном и домашней сетью уже распределен некоторый общий секретный ключ (например, он «зашит» в SIM-карту на этапе её производства, либо получен в результате работы алгоритмов, заложенных в технологии eSIM).
Телефон и домашняя сеть общаются при помощи посредника – обслуживающей сети. Эта сеть по итогу работы протокола также должна получить сеансовый ключ (это необходимо для обеспечения свойства т.н. «законного перехвата», которое явно закреплено в законодательствах разных стран). При этом обслуживающая сеть не должна иметь возможность самостоятельно (без легитимного пользователя) провести процесс выработки сеансового ключа.
Нам противодействует могущественный активный противник, который контролирует все сообщения в сети и может по своему усмотрению прерывать доставку сообщений, как-либо их видоизменять, присылать сообщения в неправильном порядке и т.д. (т.н. модель угрозы Долева — Яо [2]).
Самым сложным представляется вопрос о том, что же именно считать «безопасным» протоколом выработки сеансового ключа (или, следуя Канту: «На что я могу надеяться, если делаю то, что мне надлежит делать?»). Традиционным является экспертный подход, в ходе которого протокол изучается профессиональным сообществом на наличие конкретных «типичных» атак. При этом к протоколу выдвигается ряд некоторых полуформальных требований, описывающих, от чего именно мы пытаемся защититься. При обнаружении атаки, которая в каком‑либо смысле нарушает одно из требований, протокол модифицируется таким образом, чтобы противостоять подобной атаке в дальнейшем. Протокол признается безопасным, если на протяжении некоторого (относительно продолжительного) промежутка времени не было найдено новых атак.
Именно этому пути следует организация 3GPP, занимающаяся разработкой и стандартизацией протоколов, связанных с технологией 5G. Экспертами 3GPP в рамках различных сопроводительных документов выдвигаются различные полуформализованные требования к протоколу 5G‑AKA, составленные на основе предыдущих «типичных атак» на протокол и исходя из того, что именно эксперты считают угрозой для абонентов. Особенностью подобных требований является то, что они сформулированы на «простом» языке, который допускает множество интерпретаций. Как пример, можно привести фразу, которой описывается свойство user untraceability (неотслеживаемость пользователя) из документа TS133.102: “an intruder cannot deduce whether different services are delivered to the same user by eavesdropping”.
Уже в такой постановке задачи можно выделить некоторые потенциальные проблемы. Во-первых, по каким причинам рассматривается только пассивный противник (eavesdropping)? Во-вторых, более серьезное возражение: как именно дать какие-либо количественные (а не качественные) оценки (вероятности) выполнения или невыполнения свойства?
Проблема формализации
Современная криптография основана на сложных, но потенциально решаемых задачах – всё зависит от ресурсов противника. Так, например, он может, используя полный перебор ключей, найти общий секретный ключ пользователя и домашней сети (используя для отбраковки ключей ранее посланные сообщения) и затем нарушить любое из свойств протокола. Таким образом, количественные оценки должны брать в расчет как ресурсы противника, так и то, что по слепой случайности противнику может повезти, и он сразу же, ткнув пальцем в небо, найдет нужный ему секретный ключ. Помимо этих характеристик (вычислительных ресурсов и вероятностной природы задачи), на стойкость алгоритма могут влиять разнообразные параметры: количество проведенных сеансов связи, количество пользователей в сети, длина обрабатываемых сообщений, возможность получать коды ошибок и так далее. В постановке задачи, данной выше, такие количественные оценки невозможны, а значит — необходима дальнейшая работа по формализации задачи.
К сожалению, формализация указанного свойства не будет единственной. Так, можно предположить несколько (не исчерпывающих) «интерпретаций»:
Indistinguishability: все сообщения в протоколе неотличимы от случайных бит – в таком случае транскрипция протокола ничем не отличается от случайного шума, а значит в ней гарантированно нельзя выделить никакого полезного сигнала.
Zero knowledge: все сообщения в протоколе можно промоделировать, не зная долговременных секретов. В таком случае транскрипция протокола не дает никакой информации противнику, поскольку он сам в состоянии сгенерировать подобное распределение двоичных сообщений без необходимости взаимодействовать с реальными участниками.
Left-or-Right: противник не может определить, с каким из двух им выбранных участников он общается в данный момент времени. В таком случае противник не может понять, кому какая транскрипция протокола соответствует, а также являются ли две транскрипции записью протокола с одним и тем же участником или с различными.
Каждая из описанных выше интерпретаций может быть однозначно сведена к оценке вероятности некоторых событий во вполне однозначно определенных вероятностных пространствах, что как раз и даёт возможность количественной оценки безопасности протокола.
Плюсы и минусы подхода «доказуемой стойкости»
Сведение задачи к конкретным математическим моделям с дальнейшей оценкой вероятностей в явном виде (т.н. подход «доказуемой стойкости») имеет несколько плюсов по сравнению с предыдущим вышеозначенным экспертным подходом.
Так, экспертному подходу присущи следующие недостатки:
Не фиксируется общее в экспертной среде понимание ресурсов, возможностей противника и его целей применительно к изучаемому протоколу. Это может приводить к тому, что одни эксперты будут склонны считать, что свойство «бессмысленно», и его необходимо исключить из рассмотрения, в то время как другие будут предлагать решения, исходя из их специфического понимания свойства безопасности и угрозы.
Посредством сведения протокола к «общепризнанным» моделям появляется возможность переиспользовать опыт других экспертов в решении сходных задач: как правило, многие трудности, возникающие на практике, неявно «закодированы» в общепризнанных моделях. Ограничиваясь рассмотрением свойств безопасности для конкретного протокола без рассмотрения его в более общем контексте можно избыточно сузить рассматриваемые угрозы и упустить из виду новые атаки.
При этом стоит также отметить, что подход, фокусирующийся на математическом моделировании свойств безопасности, также имеет и некоторые серьезные ограничения. Обозначим лишь часть из них, лежащих «на поверхности»:
Интерпретация получаемых результатов в духе абсолютной стойкости даёт избыточно оптимистичные ожидания, которые могут приводить к конфузу. Так, в математических статьях, посвященных криптоанализу протоколов, часто утверждается, что авторами был взломан «доказуемо стойкий» протокол. Как правило, это либо означает то, что реальные условия функционирования протокола отличаются от зафиксированных в модели; либо что авторами криптоанализа была найдена какая-то ошибка в доказательстве (математика по большей части внутренне непротиворечива).
Возможно отклонение и в другую сторону. Так, ограничения в используемой «технике» и сложности доказательства могут давать избыточно пессимистичные результаты. Как пример тут может рассматриваться прием, используемый при доказательствах неподделываемости некоторых типов цифровых подписей, известный в фольклоре как «forking lemma» [6]. Он дает завышенную оценку вероятности успеха противника в силу невозможности доказать результат иным (не косвенным) методом на данном этапе развития науки.
Модели для свойств безопасности очень чувствительны к изначальным предположениям, вплоть до «незначительных» изменений: так, иногда возвращение кодов ошибок или замер времени выполнения операции дает противнику возможность полностью скомпрометировать протокол (см. «атаки по побочным каналам», а также [4] для примера подобных атак).
Протоколы, доказуемо стойкие в различных моделях, могут быть чувствительны к «композициям»: так, иногда «стойкий» протокол ????1 может быть скомбинирован со «стойким» протоколом ????2, но в итоге получится объединенный «нестойкий» протокол ????3 (см. например [5]).
Зачастую формальные модели довольно трудно понять человеку, не погруженному в тематику достаточно глубоко. Сложность математического доказательства безопасности протокола в исследуемой модели также не добавляет интерпретируемости полученным результатам. Как итог, на выходе после исследования получаются результаты, которые трудно «объяснить» тем, кто не специализируется на доказательстве подобных результатов, не говоря уже об «обычных» людях.
Ограничения в используемой технике приводят к тому, что иногда криптографам приходится прибегать к различным «идеализациям» в ходе доказательства. Так, например, хэш-функция часто заменяется на случайную, доступ к которой имеется только посредством некоторого оракула (черного ящика, устройство которого неизвестно, и которому на вход подается сообщение, а на выходе получается некоторая двоичная строка фиксированной длины) – т.н. random oracle model [7]. Разумеется, хэш-функции устроены «не так»: в частности, противник, имеющий описание хэш-функции или ее псевдокод, может вполне самостоятельно вычислять ее значение на различных входах, и для этого ему не нужно обращаться ни к какому «оракулу». Более того, существуют строго обоснованные теоремы, которые утверждают, что такое «упрощение» не только «несколько искажает» и размывает результаты (т.е. становится непонятно, что в итоге было доказано), но даже напрямую некорректно – существуют специфического вида криптосистемы, стойкие в модели с оракулом, но совершенно нестойкие при замене оракула на любую конкретную хэш-функцию [8] (т.е. детерминированную быстро вычисляемую функцию с относительно компактным описанием). Модель случайного оракула – не единственная используемая в доказательствах эвристика (упрощение).
Ранее упоминалось, что современная криптография опирается на сложные, но потенциально решаемые задачи. Основной целью криптографа в подходе «доказуемой стойкости» является сведение стойкости протокола к решению конкретных сложных задач. При этом возникают утверждения вида «если существует противник, с высокой вероятностью успешно атакующий протокол, то из него можно сконструировать другого противника, который решает некоторую сложную математическую задачу». То, на какие именно «сложные» математические задачи в итоге опирается доказательство, сильно зависит от дизайна протокола.
Существует некоторый пул «стандартных» вычислительно-сложных задач (см. также [9,10] для более подробного ознакомления), как пример можно привести следующие:
a. задача факторизации (разложения больших чисел на простые сомножители) и её частный случай — проблема RSA (вычисление корня е-й степени шифрованного текста c по составному целочисленному модулю);
b. задача дискретного логарифмирования (обратная операция возведению целого числа в степень по модулю простого числа) и её разновидность — вычислительная проблема Диффи‑Хеллмана (CDH problem);
c. задача поиска кратчайшего ненулевого вектора в решетке.
Для решения этих задач на сегодня неизвестны «быстрые» алгоритмы — то есть такие, у которых сложность решения полиномиально зависит от длины входных данных. Однако в сведениях часто возникают «нестандартные» задачи, которые в явном виде не сводятся ни к какой из стандартных. Иногда их «объявляют» сложными для удобства доказательств. Конечно, подобный подход не добавляет уверенности в стойкости исходного протокола [11].
Указанные проблемы, казалось бы, должны поставить под сомнение саму сущность метода – если он имеет такое количество ограничений и тонкостей, то зачем использовать подобный инструмент? Оказывается, что в некотором смысле подобные ограничения присущи любой сфере знаний, где применяется математическое моделирование.
Математические модели
Как было указано выше, подход «доказуемой стойкости» не является панацеей: его интерпретация может давать избыточно оптимистичные гарантии, либо наоборот — быть избыточно «пессимистичным». Это не является проблемой подхода per se: аналогичные замечания могут быть предъявлены практически к любой области знаний, где (совершенно на законных, и вовсе не на «птичьих» правах) используются математические модели.
Рассмотрим следующий жизненный цикл модели:
В реальном мире мы имеем дело с некоторой сложной системой, изучение которой в явном виде, во всей её сложности и многообразии, не представляется возможным. Мы можем на основании изучения этой системы выделить некоторые «сущностные» требования к системе в некотором полуформализованном виде, отбросив то, что на наш взгляд (как исследователей) является несущественным. На основании выделенных характерных черт мы можем построить математические модели системы, которые поддаются изучению в силу их простоты по сравнению с реальным миром. Изучая полученную модель, мы можем получать некоторые математические следствия из введенных нами понятий. Следствия предположений «сверяются» с реальностью: мы можем пытаться «прогнозировать» ещё не исследованные вещи и проверять, насколько хорошо наши прогнозы согласуются с реальностью. Либо, в духе «попперианства», пытаться опровергнуть модель.
Полуформализованные требования могут выглядеть как требование приватности (противник не может определить абонента), конфиденциальности (противник не может определить содержание пересылаемых сообщений), неподделываемости и т.д. Каждое из полученных требований может быть уточнено до конкретной математической модели. В рамках модели могут быть получены различные результаты (протокол нестойкий, т.е. существует атака в модели; стойкость протокола сводится к стойкости ряда задач и т.д.), которые затем можно «опробовать» на реальной системе. Интересный пример данного цикла в рамках статистических моделей рассмотрен в книге Рихарда Макелрета «Statistical rethinking» [12].
Вообще говоря, если проводить аналогии моделей безопасности со статистическими моделями, можно выделить следующие моменты:
Модели безопасности, как и статистические модели, не могут дать гарантий выполнения свойства на практике. По-видимому, правильнее всего (по аналогии с проверкой гипотез в статистике) говорить, что недостаточно свидетельств для того, чтобы опровергнуть гипотезу о том, что протокол безопасен.
Модели безопасности, как и статистические модели, могут давать «ложноположительные» результаты: не все атаки, описываемые в рамках формальной модели, могут быть переведены в атаки в «реальном мире». Так, один и тот же режим шифрования может быть стойким в одной модели атаки на основе неразличимости шифртекстов (LOR-CPA), но нестойким в модели отличимости шифртекста от случайных строк (IND-CPA), хотя обе основаны на интуитивном понятии о безопасности режима шифрования. Ведет ли это различие к каким-то последствиям на практике – априори сказать невозможно.
Модели безопасности, как и статистические модели, могут давать «ложноотрицательные» результаты, особенно если полученные результаты интерпретируются в рамках «абсолютной стойкости».
Модели безопасности, как и статистические модели, используют некоторые предположения, которые являются несомненным «упрощением реальности», но полезны для анализа. Вообще говоря, не существует такой вещи, как «правильная модель» – любая модель неверна просто по определению. Тем не менее какие-то из них оказываются чрезвычайно полезными.
При значительном отклонении «реальности» от «модели» мы, возможно, получаем гораздо больше «полезной» информации, которая может быть учтена в последующих уточнениях модели, чем при «хорошем соответствии».
Зачем же тогда нужны модели?
Подытоживая все рассуждения, мы можем выделить некоторые существенные плюсы от использования подхода доказуемой стойкости, которые перевешивают все озвученные минусы:
модели безопасности могут использоваться как инструмент коммуникации: в сжатом виде они содержат то, что другие «умные люди» посчитали важным учитывать для протоколов/криптосистем изучаемого типа;
модели безопасности, совместно с доказательством стойкости, могут давать более глубокое понимание задачи. Для этого они должны быть (насколько это возможно) понятными и относительно легко интерпретируемыми;
модели безопасности используются для получения более точных (количественных, а не качественных) выводов (с явным постулированием исходных предположений);
отклонение от модели даёт больше информации, чем близкое соответствие ей: это говорит о том, что есть какие-то существенные аспекты реальности, неучтённые в модели;
возможно, что модели, или совокупности моделей развиваются кумулятивно и неявно вбирают в себя всё лучшее, что было придумано ранее (см. п. 1).
При всём при этом не следует забывать, что, в то время как криптографы всё-таки верят в силу моделей, криптоаналитики работают в другой парадигме. Лучше всего её описал Пол Фейерабенд: «существует лишь один принцип, который можно защищать при всех обстоятельствах и на всех этапах человеческого развития, — всё дозволено».
Список литературы
1. Boyd, Colin, Anish Mathuria, and Douglas Stebila. Protocols for authentication and key establishment. Vol. 1. Heidelberg: Springer, 2003.
2. Мао, Венбо. Современная криптография: теория и практика. Издательский дом Вильямс, 2005.
3. Basin, David, Jannik Dreier, Lucca Hirschi, Saša Radomirovic, Ralf Sasse, and Vincent Stettler. "A formal analysis of 5G authentication." In Proceedings of the 2018 ACM SIGSAC conference on computer and communications security, pp. 1383-1396. 2018.
4. Vaudenay, Serge. "Security flaws induced by CBC padding—applications to SSL, IPSEC, WTLS..." In International Conference on the Theory and Applications of Cryptographic Techniques, pp. 534-545. Springer, Berlin, Heidelberg, 2002.
5. Canetti, Ran. "Security and composition of cryptographic protocols: A tutorial." Secure Multi-Party Computation (2013): 61-119.
6. Bellare, Mihir, and Gregory Neven. "Multi-signatures in the plain public-key model and a general forking lemma." In Proceedings of the 13th ACM conference on Computer and communications security, pp. 390-399. 2006.
7. Bellare, Mihir, and Phillip Rogaway. "Random oracles are practical: A paradigm for designing efficient protocols." In Proceedings of the 1st ACM Conference on Computer and Communications Security, pp. 62-73. 1993.
8. Canetti, Ran, Oded Goldreich, and Shai Halevi. "The random oracle methodology, revisited." Journal of the ACM (JACM) 51, no. 4 (2004): 557-594.
9. Oded, Goldreich. "Foundations of cryptography: volume 1, basic tools." (2008).
10. Katz, Jonathan, and Yehuda Lindell. Introduction to modern cryptography. CRC press, 2020.
11. Koblitz, Neal, and Alfred Menezes. "The brave new world of bodacious assumptions in cryptography." Notices of the American Mathematical Society 57, no. 3 (2010): 357-365.
12. McElreath, Richard. Statistical rethinking: A Bayesian course with examples in R and Stan. Chapman and Hall/CRC, 2020.