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

Классификация

С учетом определения и анализа криптодоказующих программ выделяют следующую классификацию, или так называемые приемы моделирования и формализации:

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

Программы

• CPN Tools
• AVISPA Tool
• SPAN
• SpecExplorer
• SPIN

Ссылки

• (недоступная ссылка)