Formal Verification of Crytographic Algorithms
(finished)The Verisoft project is a long-term research project funded by the German Federal Ministry of Education and Research (bmb+f). It aims at verifying five concrete application tasks, one from academic and four from industrial background. The verification will be formal and pervasive, i.e. computer-aided verification tools will be used throughout all layers of abstractions. This way, human errors are excluded, full coverage is achieved, and the results are based on a well-known small set of assumptions. Hence, the verified systems are of extreme quality as required in many industrial sectors, such as automotive engineering, security, and medical technology. Additionally, productivity is expected to increase, with all tools being specifically developed and enhanced for this task.
Our research group is working in subproject 1 (tools and methods). In this part the tools and methods, with which the verification tasks from the other subprojects should be accomplished, are to be (further-)developed. As a result, the mathematical gaps in the foundations should be formally solved. We are developing a tool box for the formal verification of cryptographic primitives and are connecting the methods for formal protocol analysis with the complexity theoretic view of the cryptographic primitives. Our work ranges from formalising basic tools like Big-O Notation, Probability theory, Probabilistic Polynomial Time etc. to the formal specification of cryptographic methods like AES and RSA-PSS as well as correctness and/or security proofs for these.
The following persons are working on the project
Staff
Students
- Taylan Kücük
- Tao Wei
- Guy Mauger
Software
Different Isabelle Theories
