Нотация криптографической стековой машины версии один

Хорошая спецификация криптографического протокола должна легко восприниматься человеком (быть декларативной и лаконичной), быть исполнимой и пройти процедуру формальной верификации в некоторой адекватной модели. Нацеливаясь на эти требования, в статье предложена нотация CMN.1, предназначенная для описания сообщений криптографических протоколов и основанная на вычислительной абстракции под названием криптографическая стековая машина (CSM). Статья описывает синтаксис и семантику CMN.1, а также представляет результаты разработки языка спецификаций криптографических протоколов, построенного на основе данной нотации и встроенного в язык Haskell. В авторской реализации вся обработка сообщений инкапсулирована внутри базового библиотечного модуля, в то время как спецификация должна лишь дать декларативные определения этих сообщений. При формировании исходящего сообщения протокола базовый модуль берет описание данного сообщения в нотации CMN.1 и возвращает фрагмент данных, сгенерированный по этому описанию. При обработке входящего сообщения базовый модуль берет поступивший фрагмент данных и описание ожидаемого сообщения в нотации CMN.1 и возвращает вердикт об их соответствии друг другу, извлекая и запоминая при этом все содержащиеся в сообщении данные, необходимые для формирования или верификации следующих сообщений протокола. Процесс верификации является полным: базовый модуль осуществляет расшифрование, проверку кодов аутентификации сообщений и значений цифровой подписи и т.д. Текущая реализация языка включает функции трансляции спецификаций в исполняемый код, совместимый с существующими программными реализациями протоколов, а также функции конвертации спецификаций в программы на входном языке анализатора протоколов ProVerif. В качестве иллюстрации приводятся выдержки из CMN.1-спецификации протокола TLS и соответствующей ей автоматически сгенерированной программы для ProVerif.