Formal model for cryptographic protocols based on problem-solving theory

This paper proposed a problem-solving theory based formal model, introduced the basic syntax and ρ-calculus based semantics of the model, and presented some pivotal concepts and propositions in the deduction of the model. The model has some properties as follows: can give accurate formal specifications for cryptographic protocols; has provable semantics which is reasonable and sound; can define the security properties precisely and reasonably; is easy to realize automatic deductions. All of those aforementioned make sure that the security analysis of cryptographic protocols based on this model is reasonable and efficient, and provide a dependable basis for analyzing the security of cryptographic protocols correctly.