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

Применение формальных методов в разработке реализаций сетевых протоколов способствует повышению качества этих реализаций. Наибольший эффект даст изложение на формальном языке первичных спецификаций протоколов, публикуемых в документах RFC. В статье предлагается формальный язык описания криптографических протоколов, нацеленный на более полное, по сравнению с существующими языками первичных спецификаций, выполнение следующих требований: лаконичность, декларативность, выразительность, однозначность, исполнимость, возможность автоматического извлечения из спецификаций наборов тестов высокого качества. Основа языка – вычислитель, специально разработанный для предметной области криптографических протоколов, – т. н. C2-машина. В статье при изложении принципов построения и функционирования C2-машины используется метод последовательного уточнения модели: сначала вводится недетерминированный автомат, на котором в наиболее общем виде задается операционный контракт протокола, затем вводится машина C0, на которой демонстрируется предлагаемый подход к специфицированию недетерминизма протоколов, и далее – машина C1, на которой в формализованном виде задается семантика базовых инструкций C2-машины. Статья иллюстрирована примерами для протокола TLS.