Flow logic for Dolev-Yao secrecy in cryptographic processes

被引：12
|
作者：
Bodei, C
Degano, P
Nielson, F
Nielson, HR
机构：
[1] Univ Pisa, Dipartimento Informat, I-56125 Pisa, Italy
[2] Tech Univ Denmark, DK-2800 Lyngby, Denmark
来源：
FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE | 2002年 / 18卷 / 06期
关键词：
cryptographic process calculi; static analysis; security; secrecy;
D O I：
10.1016/S0167-739X(02)00047-X
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We introduce the vspi-calculus that strengthens the notion of "perfect symmetric cryptography" of the spi-calculus by making encryption history dependent. We give our calculus an operational and a static semantics. The latter is a control flow analysis (CFA), defined in the form of a flow logic, and it is proved semantically correct. We then apply our CFA to check security properties; in particular, we show that secrecy A la Dolev-Yao can be expressed in terms of the CFA. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：747 / 756
页数：10
相关论文
共 36 条
  • [1] Cryptographic protocol logic: Satisfaction for (timed) Dolev-Yao cryptography
    Kramer, Simon
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2008, 77 (1-2): : 60 - 91
  • [2] Symmetric encryption in a simulatable Dolev-Yao style cryptographic library
    Backes, M
    Pfitzmann, B
    17TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2004, : 204 - 218
  • [3] Extending Dolev-Yao with Assertions
    Ramanujam, R.
    Sundararajan, Vaishnavi
    Suresh, S. P.
    INFORMATION SYSTEMS SECURITY (ICISS 2014), 2014, 8880 : 50 - 68
  • [4] Satisfiability of Dolev-Yao Constraints
    Mazare, Laurent
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (01) : 109 - 124
  • [5] A computational interpretation of Dolev-Yao adversaries
    Herzog, J
    THEORETICAL COMPUTER SCIENCE, 2005, 340 (01) : 57 - 81
  • [6] A Dolev-Yao Model for Zero Knowledge
    Baskar, Anguraj
    Ramanujam, R.
    Suresh, S. P.
    ADVANCES IN COMPUTER SCIENCE - ASIAN 2009: INFORMATION SECURITY AND PRIVACY, PROCEEDINGS, 2009, 5913 : 137 - +
  • [7] Decision and Complexity of Dolev-Yao Hyperproperties
    Rakotonirina, Itsaka
    Barthe, Gilles
    Schneidewind, Clara
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
  • [8] DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing
    Ammann, Max
    Hirschi, Lucca
    Kremer, Steve
    45TH IEEE SYMPOSIUM ON SECURITY AND PRIVACY, SP 2024, 2024, : 1481 - 1499
  • [9] A structured operational semantic modelling of the Dolev-Yao threat environment and its composition with cryptographic protocols
    Mao, W
    COMPUTER STANDARDS & INTERFACES, 2005, 27 (05) : 479 - 488
  • [10] Dolev-Yao Theory with Associative Blindpair Operators
    Baskar, A.
    Ramanujam, R.
    Suresh, S. P.
    IMPLEMENTATION AND APPLICATION OF AUTOMATA (CIAA 2019), 2019, 11601 : 58 - 69
1234