Time-based Messages Derivation and Symbolic Trace Analysis of Security Protocol
Zhou Ming-tian · Journal of China Academy of Electronics and Information Technology · 2010
How to accurately depict the protocol model run in the hostile environment and analyze multiple security properties under a unified framework are the two key problems of the formal analysis of security protocols.Time-based message derivation is presented,which can be used to deduce the knowledge of principals,and then a generic model of the protocol run is proposed.The deductive relationships among the messages are used to unify the formal expressions of various security properties,and the corresponding satisfaction conditions are defined.A generic framework is proposed for the analysis of security protocols.Finally a case study as well as future directions is given.