Authentication primitives for secure protocol specifications

被引：2
作者：
Bodei, C
Degano, P
Focardi, R
Priami, C
机构：
[1] Univ Pisa, Dipartimento Informat, I-56125 Pisa, Italy
[2] Univ Ca Foscari Venezia, Dipartimento Informat, I-30173 Venice, Italy
[3] Univ Trent, Dipartimento Informat & Telecomunicaz, I-38050 Povo, TN, Italy
来源：
FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE | 2005年 / 21卷 / 05期
关键词：
cryptographic process calculi; security; authentication;
D O I：
10.1016/j.future.2004.05.004
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We use two authentication primitives proposed recently as a linguistic support for enforcing authentication. They offer a way of abstracting from various specifications of authentication and of obtaining idealized protocols "secure by construction". Consequently, they help in proving that a cryptographic protocol correctly implements its corresponding abstract version; when the implementation is incorrect, suggestions on how to fix it may come from reasoning on the abstract specification. (c) 2004 Elsevier B.V All rights reserved.
引用
收藏
页码：645 / 653
页数：9
相关论文
共 26 条
  • [1] A calculus for cryptographic protocols: The spi calculus
    Abadi, M
    Gordon, AD
    [J]. INFORMATION AND COMPUTATION, 1999, 148 (01) : 1 - 70
  • [2] Secrecy by typing in security protocols
    Abadi, M
    [J]. JOURNAL OF THE ACM, 1999, 46 (05) : 749 - 786
  • [3] Primitives for authentication in process algebras
    Bodei, C
    Degano, P
    Focardi, R
    Priami, C
    [J]. THEORETICAL COMPUTER SCIENCE, 2002, 283 (02) : 271 - 304
  • [4] Names of the π-calculus agents handled locally
    Bodei, C
    Degano, P
    Priami, C
    [J]. THEORETICAL COMPUTER SCIENCE, 2001, 253 (02) : 155 - 184
  • [5] Authentication via localized names
    Bodei, C
    Degano, P
    Focardi, R
    Priami, C
    [J]. PROCEEDINGS OF THE 12TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, 1999, : 98 - 110
  • [6] TESTING EQUIVALENCE FOR MOBILE PROCESSES
    BOREALE, M
    DENICOLA, R
    [J]. INFORMATION AND COMPUTATION, 1995, 120 (02) : 279 - 303
  • [7] BURROWS M, 1990, ACM T COMPUT SYST, V8, P18, DOI [10.1145/77648.77649, 10.1145/74851.74852]
  • [8] Data Encryption Standard, 1977, FIPS PUBL
  • [9] Non-interleaving semantics for mobile processes
    Degano, P
    Priami, C
    [J]. THEORETICAL COMPUTER SCIENCE, 1999, 216 (1-2) : 237 - 270
  • [10] DEGANO P, ACM COMPUT SURVEYS, V33, P135
123