Методы и средства автоматической верификации протоколов паспортно-визовых документов.

Россия, ОКБ САПР

• базовый контроль доступа ВАС (Basic Access Control) предназначен для предотвращения неавторизованного считывания;
• механизм пассивной аутентификации используется для проверки целостности данных, хранящихся в электронном паспорте;
• активная аутентификация как факультативный механизм защиты, использующий криптографию с открытым ключом, предназначена для противостояния атакам, связанным с модификацией и клонированием микросхемы;
• в дополнение к изображению лица Международная организация гражданской авиации (ИКАО) одобряет хранение в микросхеме ПВД НП цифровых изображений отпечатков пальцев и радужной оболочки глаза, которые представляют собой чувствительную информацию и требуют использования усиленных механизмов контроля доступа. Для удовлетворения данного требования используется расширенной контроль доступа ЕАС (Extended Access Control), который требует аутентификации системы проверки до раскрытия данных;
• протокол согласования ключей Диффи-Хеллмана с парольной аутентификацией (PACE), рекомендованный в [1] в качестве альтернативы BAC, обеспечивает безопасное соединение и основанную на пароле аутентификацию микросхемы ПВД НП и системы проверки [2]. PACE является улучшенной альтернативой BAC и позволяет микросхеме ПВД НП удостовериться, что система проверки авторизована для получения доступа к содержащимся в микросхеме данным.

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

Для анализа криптографических протоколов разработано множество различных методов. В общем случае все методы могут быть разделены на эвристические (неформальные) и формальные.

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

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

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

Можно выделить два основных подхода к верификации протоколов безопасности (и соответственно два класса формальных методов верификации):

1. логический вывод (на основе доказательства свойств);
2. проверка модели (model checking).

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

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

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

Средство автоматической верификации криптографических протоколов ProVerif, реализующее метод логического вывода, позволяет выполнять анализ неограниченного числа сеансов протокола с использованием верхней аппроксимации и представления протокола с помощью хорновских выражений [5],[6]. ProVerif позволяет в автоматическом режиме проверять свойство секретности (конфиденциальности), свойство аутентификации, обрабатывать множество различных криптографических примитивов, включая криптографию с разделяемым и открытым ключом (шифрование и подпись), хэш-функции, и согласование ключей Диффи-Хеллмана, заданное как в правилах перезаписи, так и в виде уравнений.

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

Средство автоматической верификации криптографических протоколов Scyther использует символический анализ в сочетании с обратным поиском, основанный на частично упорядоченных шаблонах, и верифицирует ограниченное и неограниченное число сеансов протокола [7], [8].

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

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

В средстве FDR2, основанном на методе проверки модели, для описания поведения участников протокола используется нотация CSP (Communicating sequential processes) [9]. Каждый участник протокола моделируется с помощью процесса CSP, который находится либо в состоянии ожидания сообщения, либо посылает сообщение. Каналы используются для взаимодействия между процессами и моделирования противника. Противник описывается как параллельная композиция нескольких процессов, по одному на каждый факт или сообщение, из которых он может получить какие-либо сведения о выполнении протокола. FDR2 использует подход, который называется уточняющей проверкой модели (refinement model checking). Он состоит в подтверждении того, что модель, описывающая поведение системы, которая реализует проверяемый протокол, эквивалентна модели, задающей требования безопасности для данного протокола. Специально разработанный компилятор CASPER (Lowe, 1997) позволяет автоматизировать конструирование противника [10], [11].

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

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

СПИСОК ЛИТЕРАТУРЫ:

1. Technical Report «Supplemental Access Control for Machine Readable Travel Documents», Version - 1.01, - November 11, 2010.
2. BSI TR-03110 v2.00 Technical Guideline Advanced Security Mechanisms for Machine Readable Travel Documents - Extended Access Control (EAC), Password Authenticated Connection Establishment (PACE) and Restricted Identification (RI), 2008.
3. Котенко И. В., Резник С. А., Шоров А. В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств // Труды СПИИРАН. 2009. Вып. 8. С. 292-310.
4. Косачев А. С., Пономаренко В. Н. Анализ подходов к верификации функций безопасности и мобильности. М.: Триумф, 2004. - 101 с.
5. Blanchet В. ProVerif. Automatic Cryptographic Protocol Verifier. User Manual. CNRS, Departement d'Informatique. Ecole Normale Sup.erieure, Paris. July 9, 2010.
6. http://www.proverif.ens.fr/.
7. Cremers C. J. F. Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement // Proc. of the 15th ACM conference on Computer and communications security, 2008. P. 119-128.
8. http://people.inf.ethz.ch/cremersc/scyther/.
9. Hoare C. A. R. Communicating sequential processes // Communications of the ACM, 1978. Vol. 21, № 8. P. 666-677.
10. Pasupathinathan V., Pieprzyk J., Wang H. Security Analysis of Australian and E.U. E-passport Implementation. Journal of Research and Practice in Information Technology. Vol. 40. No. 3. August 2008.
11. http://www.cs.ox.ac.uk/people/gavin.lowe/Security/Casper/.

Автор: Грунтович Д. В.

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

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

---