Research On Formal Verification Technology For Cryptographic Module's APIs

It has for a long time that the security of cryptographic module's API has not been paid sufficient attention to and been fully studied.But along with the API-level attack been continual discovered for most cryptographic module,the security of cryptographic module's API has been widely studied from 2000.With the study in a deep going way,how to build the formal model of cryptographic module's API exactly and effectively in order to use the formal verification tools for verified conveniently,which has been the focus of the field of formal verification of cryptographic module's API.The thesis took a widely used cryptographic module's API-PKCS#11 as an example,a deep investigation and study of formal verification technology for the security of cryptographic module's API has been made.The main works and contributions of the dissertation are summarized as follows:Introduced the cryptographic module's API and the formal analysis and verification technology and the achievement of the field,analyzed the hotspot and shortage of the field.Investigated a widely used cryptographic module's API-PKCS#11,analyzed the security mechanism of PKCS#11,studied the known API-level attacks of PKCS#11,and a formal description technique based "Alice-Bob" which is used to describe protocols has carried on,and summarized the security problem of PKCS#11.Investigated the both PKCS#11 model based on the first-order logic and based on the HLPSL,and the verification technique has been studied also,analyzed the flaws of the two kind of formal verification technique.Present a set of grammar and formalized semantics which is suitable in describing the PKCS#11,and established the formal model of the PKCS#11 core key management transaction, by introducing the concept of mode,we build the well-modedness rules,proved the existence of well-modedness derivation,and proven that the reachability of the model is decidable under the condition of well-modedness.Designed the technique and the strategy of the formal verification of PKCS#11,using the model checking tool NuSMV,we have verified the different configuration of the PKCS#11 as experiments,discussed the secure configuration of the PKCS#11,and compared the experimental result of the thesis and the others,which further proved that we not only can verify the known attacks,but also can find some new attacks by the method we used to verify the model of PKCS#11 proposed.