A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model

摘要

Security protocols and cryptographic primitive play a very important role in information security world. People have paid a serious attention to the methods to verify security properties in security protocols and cryptographic primitives. From 1980's two distinct approaches: Symbolic approach and computational approach have been proposedd for it. Recently, significant advances have been made in verification on security properties in security protocols and cryptographic primitives and these two approaches. In this study we survey the existing results on the fields including symmetric encryption, public key encryption, digital signature , hush function, secrecy, key cycles, information flow, secrecy, automatic proof, deniable authentication protocol, electronic payment protocol and internet voting protocol in symbolic model and computational model. The survey processes in two lines: One line follows the trace of emergence and developments of verification on security properties in security protocols and cryptographic primitives. The other line is to discuss what methods are usedd and how to verify these security properties during the developments. Finally we give the existing results on verification on security properties in security protocols and cryptographic primitives in symbolic model and computational model.