关键词: 安全协议，形式化验证，时间模型，时间戳

Abstract: Security protocols arc used to provide secure communication over open network. I}imcstamp can make sure the freshness of the message in the protocol,but it is not enough to research the time sensitive protocols,and there are no effective methods that can verify these protocols.So it's very difficult to verify all aspects of those huge and complex protocols in formal ways. This paper described why using time-stamp and researching it,and discussed several popular methods in this field which are MSR method,induction method CSP method and BAN logic method in werification of time sensitive security protocols. This paper gave out their estimations. Finally we also strated the possible new directions of time sensitive security protocols verification.

Key words: Security protocols, Formal verification, Timed model, Time-stamp