Криптодоказующие программы — специальные программные средства, смоделированные на основе формальных моделей (например, модель Долева-Яо) с использованием штатных средств и алгебры процессов, а также с приведением к математической логике философских теорий о знании, с целью доказать криптостойкость протоколов, и, по возможности, найти недостатки в безопасности.
Классификация С учетом определения и анализа криптодоказующих программ выделяют следующую классификацию, или так называемые приемы моделирования и формализации:
подход, использующий знания и абстракции тождественной логики, представленные в конкретный момент времени или в конкретное событие; подход, основанный на «агентах», моделирующий деятельность протоколов при помощи мультимножественных подстановок; подход, основанный на алгебре процессов; подход, основанный на пространстве стрендов.
Программы CPN Tools ProVerif AVISPA Tool SPAN SpecExplorer SPIN
Ссылки https://web.archive.org/web/20100306082814/http://www.proverif.ens.fr/ http://www.dagstuhl.de/de/programm/kalender/semhp/?semnr=01391 https://web.archive.org/web/20160922202730/http://www.avispa-project.org/ http://wiki.daimi.au.dk/cpntools http://msdn.microsoft.com/en-us/devlabs/ee692301.aspx
Категория:Криптография