Deciding Recognizability under Dolev-Yao Intruder Model

被引：0

作者：

Li, Zhiwei ^{[1
]}

Wang, Weichao ^{[1
]}

机构：

[1] UNC Charlotte, Dept SIS, Charlotte, NC 28262 USA

来源：

INFORMATION SECURITY | 2011年 / 6531卷

关键词：

Security; Verification; Formal Methods; SECURITY;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

The importance of reasoning about recognizability has recently been stressed in finding type flaw attacks, in which a protocol message may be forged from another message. However, the problem of deciding recognizability has never been fully exploited. To fill this gap, we present a terminating procedure to decide recognizability under the standard Dolev-Yao model. By incorporating the proposed procedure with Athena, a well-know security protocol verifier, our experiments succeed in finding potential type flaw attacks.

引用

页码：416 / 429

页数：14

共 32 条

[21] Limits of the BRSIM/UC soundness of Dolev-Yao models with hashes
Backes, Michael
Pfitzmann, Birgit
Waidner, Michael
[J]. COMPUTER SECURITY - ESORICS 2006, PROCEEDINGS, 2006, 4189 : 404 - 423
[22] CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions
Rocchetto, Marco
Tippenhauer, Nils Ole
[J]. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2016, 2016, 10009 : 175 - 192
[23] Bridging Dolev-Yao Adversaries and Control Systems with Time-Sensitive Channels
Groza, Bogdan
Minea, Marius
[J]. CRITICAL INFORMATION INFRASTRUCTURES SECURITY, CRITIS 2013, 2013, 8328 : 167 - 178
[24] A cryptographically sound Dolev-Yao style security proof of an electronic payment system
Backes, M
Dürmuth, M
[J]. 18TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2005, : 78 - 93
[25] A cryptographically sound Dolev-Yao style security proof of the Otway-Rees protocol
Backes, M
[J]. COMPUTER SECURITY ESORICS 2004, PROCEEDINGS, 2004, 3193 : 89 - 108
[26] Dolev-Yao攻击者模型的形式化描述
唐郑熠
李祥
[J]. 计算机工程与科学, 2010, 32 (08) : 36 - 38
[27] A structured operational semantic modelling of the Dolev-Yao threat environment and its composition with cryptographic protocols
Mao, W
[J]. COMPUTER STANDARDS & INTERFACES, 2005, 27 (05) : 479 - 488
[28] Key-dependent message security under active attacks - BRSIM/UC-soundness of Dolev-Yao-style encryption with key cycles
Backes, Michael
Pfitzmann, Birgit
Scedrov, Andre
[J]. JOURNAL OF COMPUTER SECURITY, 2008, 16 (05) : 497 - 530
[29] Correctness of Self-stabilizing Algorithms under the Dolev Model When Adapted to Composite Atomicity Models
[J]. Chen, C.-Y., 1600, Springer Science and Business Media Deutschland GmbH (21):
[30] The complexity of deciding stability under FFS in the Adversarial Queueing model
Alvarez, C
Blesa, M
Díaz, J
Fernández, A
Serna, M
[J]. INFORMATION PROCESSING LETTERS, 2004, 90 (05) : 261 - 266

← 1 2 3 4 →