New semantic model for authentication protocols in ASMs

被引：5

作者：

Xue, R ^{[1
]}

Feng, DG ^{[1
]}

机构：

[1] Chinese Acad Sci, Inst Software, State Key Lab Informat Secur, Beijing 100080, Peoples R China

来源：

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY | 2004年 / 19卷 / 04期

基金：

中国国家自然科学基金;

关键词：

cryptographic protocol; formal analysis; abstract state machine (ASM); authentication protocol;

D O I：

10.1007/BF02944758

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

A new semantic model in Abstract State Model (ASM) for authentication protocols is presented. It highlights the Woo-Lam's ideas for authentication, which is the strongest one in Lowe's definition hierarchy for entity authentication. Apart from the flexible and natural features in forming and analyzing protocols inherited from ASM, the model defines both authentication and secrecy properties explicitly in first order sentences as invariants. The process of proving security properties with respect to an authentication protocol blends the correctness and secrecy properties together to avoid the potential flaws which may happen when treated separately. The security of revised Helsinki protocol is shown as a case study. The new model is different from the previous ones in ASMs.

引用

页码：555 / 563

页数：9