Research On Computational Soundness Of Symbolic Approach For Cryptographic Protocols

The formal methods of Cryptographic protocol are categorized as two classes: the computational approach and the symbolic approach. The symbolic approach assumes the cryptographic scheme is perfect, But the correctness of the perfect assumption has not been proved. Considering the Cryptanalysis ability of the adversary, the computational approach, close to the actual protocol implementation, can attain sound result. At present, people engage in establishing the computational soundness of symbolic approach under the framework of the computational approach.Micciancio and Warinschi have developed a general method for establishing the computational soundness of symbolic method. But their method only considers asymmetry encryption, authentication property, without considering the randomicity of perfect cryptographic algorithms, and can't analyze the protocols including the messages with the type of {{m}_k}_k'. This thesis extends the Micciancio-Warinschi symbolic method and proves the computational soundness of extended method under the framework of computational approach.The main work and creations are summarized as follows:1. Remove some limitations of Micciancio-Warinschi method, establish the extended label-based symbolic model and the extended computational model, and prove the computational soundness of the extended label-based symbolic model. This is the focus and the difficult part of the paper.2. The manual analyses for NS protocol and NSL protocol show the validity of the extended Micciancio-Warinschi method.3. In order to make the extended label-based symbolic model easy to be analyzed by the machine, present the random transform of the extended label-based symbolic model, and prove the correctness of random transform.4. Present the principle, architecture and work flow for verifying the computational soundness of the extended label-based symbolic model, and realize it by existing tools.