Crypto-proofing programs are special software tools modeled on the basis of formal models (for example, the Dolev-Yao model ) using standard tools and process algebra, and also bringing philosophical theories about knowledge to mathematical logic in order to prove the crypto-resistance of protocols , and -the ability to find flaws in security.
Content
Classification
Taking into account the definition and analysis of cryptographic programs, the following classification is singled out, or the so-called modeling and formalization techniques:
- an approach that uses the knowledge and abstractions of identical logic presented at a particular point in time or at a specific event;
- an agent-based approach that simulates the operation of protocols using multiple sets of substitutions ;
- an approach based on algebra of processes ;
- strand space based approach.
Programs
- CPN Tools
- ProVerif
- AVISPA Tool
- Span
- SpecExplorer
- Spin