Security Protocol Analysis Based on Rewriting Approzimation

摘要：

TA4SP is a state-of-art tool of AVISPA that can automatically verify security protocol with unbounded number of parallel sessions. But it still has some limitations and cant verify hierarchy of authentication automatically. In this paper, we use an approximation-based model to define security protocol and design an algorithm close to the real implementation to calculate the fix-point tree automata based on the tool TA4SP. A method is proposed for analyzing hierarchy of authentication properties as extension of TA4SP. We illustrate the effectiveness of this model with the example of NSPK protocol.

关键词： security protocol approzimation fiz-point tree automata authentication

作者: Nan Liu Wen-ye Zhu Yue-fei Zhu

作者单位: Network Engineering Department, Zhengzhou Information Science and Technology Institute P.O.Box 1001-770, Zhengzhou, Henan 450002, China

会议类型: 国际会议

会议名称: Second International Symposium on Electronic Commerce and Security(第二届电子商务与安全国际研究大会)(ISECS 2009)

会议地点: 南昌

会议语种:英文

页码: 318-322

在线出版日期: 2009-05-22（万方平台首次上网日期，不代表论文的发表时间）