Формальный анализ криптографических протоколов

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

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

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

Авторами третьего подхода являются американские криптологи М. Бэрроуз, М. Абади, Р. Нидхэм (М. Burrows, M. Abadi, R. Needham). Они разработали формальную логическую модель, названную по первым буквам их фамилий БАН-логикой (BAN-logic). Составить с ее помощью общее представление о надежности криптографического протокола нельзя. Однако основное преимущество БАН-логики перед другими подходами заключается в том, что она состоит из набора простых логических правил, которые легко применяются на практике и весьма полезны при обнаружении отдельных изъянов в анализируемых протоколах.

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

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