Freshness analysis of security protocol based on GSPM
基于GSPM的安全协议新鲜性分析

Formal methods can be used to verify security protocols by specification and illation. GSPM is a generic formal model of security protocols. A new definition named freshness was added to GSPM, which formally described a special security property. A case study was given on the Andrew Secure RPC protocol with the renewed model.