On the formal modeling of inductive verification for cryptographical protocols

被引：1
|
作者：
Li, Yongjian [1 ,3 ]
Song, Xiaoyu [2 ]
Li, Xiaojuan [4 ]
机构：
[1] State Key Lab Comp Sci, Portland, OR 97207 USA
[2] Portland State Univ, Portland, OR 97207 USA
[3] State Key Lab Informat Secur, Kanas, MO USA
[4] Capital Normal Univ, Coll Informat Engn, Beijing, Peoples R China
来源：
2012 13TH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS, AND TECHNOLOGIES (PDCAT 2012) | 2012年
基金：
中国国家自然科学基金;
关键词：
D O I：
10.1109/PDCAT.2012.104
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper addresses a formal modeling issue in the inductive verification approach for cryptographical protocols. In the formalization of the inductive semantics of a protocol, the knowledge of an agent over a trace is not faithful to the intuition of the inductive approach to formally model a protocol. We find that the agent does not know the fresh items which he originates if the item is encrypted by a public key which he doe not hold. We present a novel formal characterization of traces to solve the problem.
引用
收藏
页码：201 / 206
页数：6
相关论文
共 50 条
  • [1] Modeling and Formal Verification of Communication Protocols for Remote Procedure Call
    Halder, Nilimesh
    Islam, A. B. M. Tariqul
    Bin Song, Ju
    [J]. INTERNATIONAL JOURNAL OF COMPUTER SCIENCE AND NETWORK SECURITY, 2007, 7 (07): : 63 - 71
  • [2] Formal verification and testing of protocols
    Avresky, DR
    [J]. COMPUTER COMMUNICATIONS, 1999, 22 (07) : 681 - 690
  • [3] Automated formal verification of protocols
    Avresky, DR
    Vassilaras, S
    [J]. SIXTH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 1997, : 166 - 169
  • [4] Automated inductive verification of parameterized protocols
    Roychoudhury, A
    Ramakrishnan, IV
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2001, 2102 : 25 - 37
  • [5] Inductive verification of smart card protocols
    Bella, Giampaolo
    [J]. Journal of Computer Security, 2003, 11 (01) : 87 - 132
  • [6] Formal verification of mobile robot protocols
    Béatrice Bérard
    Pascal Lafourcade
    Laure Millet
    Maria Potop-Butucaru
    Yann Thierry-Mieg
    Sébastien Tixeuil
    [J]. Distributed Computing, 2016, 29 : 459 - 487
  • [7] Formal verification of dependable distributed protocols
    Sinha, P
    Ren, DQ
    [J]. INFORMATION AND SOFTWARE TECHNOLOGY, 2003, 45 (12) : 873 - 888
  • [8] An Approach for Formal Verification of Authentication Protocols
    A. M. Mironov
    [J]. Lobachevskii Journal of Mathematics, 2022, 43 : 443 - 454
  • [9] Formal automatic verification of security protocols
    Xiao, Meihua
    Xue, Jinyun
    [J]. 2006 IEEE INTERNATIONAL CONFERENCE ON GRANULAR COMPUTING, 2006, : 566 - +
  • [10] Formal verification of mobile robot protocols
    Berard, Beatrice
    Lafourcade, Pascal
    Millet, Laure
    Potop-Butucaru, Maria
    Thierry-Mieg, Yann
    Tixeuil, Sebastien
    [J]. DISTRIBUTED COMPUTING, 2016, 29 (06) : 459 - 487
12345