Верификация протоколов паспортно-визовых документов нового поколения средствами FDR/Casper.

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

Стандарт Международной организации гражданской авиации (ИКАО) Doc 9303 определяет обязательные для достижения глобальной совместимости и факультативные механизмы защиты. Так, протокол пассивной аутентификации обеспечивает подлинность и целостность данных владельца ПВД НП. Использование пассивной аутентификации не предотвращает копирование данных, подмену микросхемы, скимминг, а также неавторизованный доступ к электронному паспорту. Для обеспечения защиты более высокого уровня ИКАО рекомендует реализацию таких механизмов защиты, как активная аутентификация (для предотвращения копирования данных и подмены микросхемы) и базовый контроль доступа (Basic Access Control, BAC) (для предотвращения скимминга и перехвата информации в коммуникационном канале между электронным паспортом и считывающим устройством).

Для ПВД второго поколения разработаны спецификации расширенного контроля доступа (Extended Access Control, EAC). EAC состоит из четырех этапов: базовый контроль доступа, аутентификация микросхемы, пассивная аутентификация и аутентификация терминала.

В спецификации ПВД третьего поколения введен протокол PACE. PACE позиционируется в качестве более защищенной замены протокола базового контроля доступа BAC и является одним из т. н. «усовершенствованных механизмов безопасности».

Протоколы электронных паспортов подвержены различным угрозам. Среди таких угроз можно выделить: пассивное считывание, активное считывание, повторное записывание, клонирование и др. Проверка протоколов на возможные угрозы представляет собой трудоемкий процесс, для упрощения которого разработаны различные средства автоматической верификации, такие как FDR, Scyther, Avatssar, ProVerif. В настоящей работе рассмотрены некоторые особенности автоматической верификации криптографических протоколов ПВД НП с использованием средств FDR/Casper.

FDR/Casper

FDR [1] представляет модель проверки, основанную на теории параллелизма и построенную вокруг алгебры CSP (communicating sequential process).

Основные особенности модели (описываемой и компилируемой) FDR:

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

Метод тестирования программ, написанных на CSP, с помощью FDR признается успешным и позволяет выявить множество возможных атак [3]. При этом написание программы с помощью CSP занимает много времени и даже опытные специалисты часто допускают ошибки, которые обычно трудно обнаружить.

Средство Casper [2] упрощает процесс моделирования протоколов для FDR. Пользователь описывает протокол, используя более абстрактные обозначения, подобные обозначениям, используемым в учебной литературе. Casper компилирует этот код в CSP, в результате чего он подходит для проверки с использованием FDR.

Исходный скрипт для Casper имеет расширение «spl» (имя_файла.spl). В результате исполнения скрипта получается файл с расширением «csp» (имя_файла.csp).

Предусматривается два способа использования Casper:

• посредством компиляции написанной программы с использованием программы Сasper. В результате этого получится файл с расширением «csp». В дальнейшем необходимо запустить программу FDR, результатом исполнения которой будут сведения о возможных атаках;
• с помощью инструмента CasperFDR с графическим интерфейсом, входящего в пакет программ Casper. С его помощью можно не только скомпилировать файл (получить файл с расширением «csp», пригодный для запуска в FDR), но и запустить его на исполнение (произвести проверку на возможные атаки) без дополнительного использования пакета программ FDR.

Время исполнения программы зависит от возможного количества состояний данной модели. Исполнение некоторых программ может потребовать больших системных и временных ресурсов.

Особенности использования FDR/Casper для верификации криптографических протоколов ПВД НП

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

Особенностью FDR является то, что поиск возможных атак производится путем анализа всех возможных состояний, в которых может находиться проверяемая модель. Поэтому от реализуемого протокола, данных, которыми может обладать нарушитель, напрямую зависит время анализа и необходимые системные ресурсы (ОЗУ, частота процессора компьютера, на котором производится анализ).

Программа на языке Casper должна определять не только работу протокола, но и конкретную систему, которую необходимо проверить. Таким образом, входной файл состоит из двух основных частей.

Первая часть входного файла включает:

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

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

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

Программа на языке Casper состоит из нескольких разделов/секций:

1. #Free variables. В данной секции описываются типы переменных и функций, используемые в описании протокола.
2. Каждый участник системы представлен процессом CSP и описан в секции #Processes.
3. В секции #Protocol description описывается последовательность сообщений, передаваемых между участниками протокола.
4. Требования к протоколу определены в разделе #Specification.
5. Типы переменных, используемых в конкретной проверяемой системе, определены таким же образом, как и в определении типов свободных переменных, и располагаются в секции #Actual variables.
6. Самая важная часть определения системы распространяется на участников, которые должны присутствовать в проверяемой системе - реализуется посредством перечисления участников с назначением соответствующих параметров в секции #System.
7. Нарушитель определяется путем представления в секции #Intruder Information его идентификационной информации и множества известных ему изначально параметров.

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

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

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

В результате выполнения автоматической верификации протоколов ПВД НП (BAC, активной и пассивной аутентификации) средствами FDR и Casper получены следующие результаты:

• протоколы электронного паспорта не удовлетворяют цели аутентификации источника данных, поскольку возможна атака на воспроизведение и «гроссмейстерская» атака;
• конфиденциальность данных также нарушается, поскольку нарушитель имеет возможность получения ключей шифрования и кода аутентификации сообщения (message authentification code, MAC), хранящихся в микросхеме электронного паспорта, с использованием информации, представленной в МСЗ.

Список литературы:

1 «Formal Systems (Europe) Ltd, Failuers-divergence refinement, FDR2 user manual», 2003, Available from www.fsel.com

2 Lowe G. Casper - a compiler for the analysis of security protocols, user manual and tutorial, ver 1.3. 1999.

3 Pasupathinathan V. Hardware-based Identification and Authentication Systems. 2009.

Автор: Староверов М. М.

Дата публикации: 01.01.2012

Библиографическая ссылка: Староверов М. М. Верификация протоколов паспортно-визовых документов нового поколения средствами FDR/Casper // Комплексная защита информации. Безопасность информационных технологий. Материалы XVII Международной конференции 15–18 мая 2012 года, Суздаль (Россия). М., 2012. С. 223–224.

---