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