Extending the Dolev-Yao intruder for analyzing an unbounded number of sessions

被引：0
|
作者：
Chevalier, Y [1 ]
Küsters, R
Rusinowitch, M
Turuani, M
Vigneron, L
机构：
[1] Univ Nancy 2, INRIA, LORIA, F-54506 Vandoeuvre Les Nancy, France
[2] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA
来源：
COMPUTER SCIENCE LOGIC, PROCEEDINGS | 2003年 / 2803卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We propose a protocol model which integrates two different ways of analyzing cryptographic protocols: i) analysis w.r.t. an unbounded number of sessions and bounded message size, and ii) analysis w.r.t. an a priori bounded number of sessions but with messages of unbounded size. We show that in this model secrecy is DEXPTIME-complete. This result is obtained by extending the Dolev-Yao intruder to simulate unbounded number of sessions.
引用
收藏
页码：128 / 141
页数：14
相关论文
共 29 条
  • [1] Extending Dolev-Yao with Assertions
    Ramanujam, R.
    Sundararajan, Vaishnavi
    Suresh, S. P.
    [J]. INFORMATION SYSTEMS SECURITY (ICISS 2014), 2014, 8880 : 50 - 68
  • [2] Deciding Recognizability under Dolev-Yao Intruder Model
    Li, Zhiwei
    Wang, Weichao
    [J]. INFORMATION SECURITY, 2011, 6531 : 416 - 429
  • [3] A Game Of Drones: Extending the Dolev-Yao Attacker Model With Movement
    Cook, Andrew
    Vigano, Luca
    [J]. 2020 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (EUROS&PW 2020), 2020, : 280 - 292
  • [4] An extension of typed MSR for specifying esoteric protocols and their Dolev-Yao intruder
    Balopoulos, T
    Gritzalis, S
    Katsikas, SK
    [J]. COMMUNICATIONS AND MULTIMEDIA SECURITY, 2005, 175 : 209 - 221
  • [5] Satisfiability of Dolev-Yao Constraints
    Mazare, Laurent
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (01) : 109 - 124
  • [6] 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
  • [7] A computational interpretation of Dolev-Yao adversaries
    Herzog, J
    [J]. THEORETICAL COMPUTER SCIENCE, 2005, 340 (01) : 57 - 81
  • [8] A Dolev-Yao Model for Zero Knowledge
    Baskar, Anguraj
    Ramanujam, R.
    Suresh, S. P.
    [J]. ADVANCES IN COMPUTER SCIENCE - ASIAN 2009: INFORMATION SECURITY AND PRIVACY, PROCEEDINGS, 2009, 5913 : 137 - +
  • [9] Decision and Complexity of Dolev-Yao Hyperproperties
    Rakotonirina, Itsaka
    Barthe, Gilles
    Schneidewind, Clara
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
  • [10] Dolev-Yao Theory with Associative Blindpair Operators
    Baskar, A.
    Ramanujam, R.
    Suresh, S. P.
    [J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA (CIAA 2019), 2019, 11601 : 58 - 69
123