Formal verification and testing of protocols

被引:5
|
作者
Avresky, DR [1 ]
机构
[1] Boston Univ, Dept Elect Engn, Brookline, MA 02146 USA
关键词
protocols; reachability analysis; execution tree; formal verification;
D O I
10.1016/S0140-3664(99)00011-0
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We adopt a formalism to describe protocols that is close to the human way of thinking and can be easily used to perform reachability analysis of the described protocol in a state-transition format. This formalism allows for an execution tree (ET) to be generated from a set of assertions such that all paths from the root to the leaves are well-defined formulas. We then extend the formalism with regards to real-time properties. Finally, we present a software verification tool, that implements the aforementioned features in the analysis of protocols. (C) 1999 Elsevier Science B.V. All rights reserved.
引用
收藏
页码:681 / 690
页数:10
相关论文
共 50 条
  • [31] Formal verification of protocols based on short authenticated strings
    Delaune, Stephanie
    Kremer, Steve
    Robin, Ludovic
    2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 130 - 143
  • [32] Formal verification: an imperative step in the design of security protocols
    Coffey, T
    Dojen, R
    Flanagan, T
    COMPUTER NETWORKS-THE INTERNATIONAL JOURNAL OF COMPUTER AND TELECOMMUNICATIONS NETWORKING, 2003, 43 (05): : 601 - 618
  • [33] An improved method for formal security verification of cryptographic protocols
    Watanabe, H
    Fujiwara, T
    Kasami, T
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1996, E79A (07) : 1089 - 1096
  • [34] A Formal Specification and Verification Framework for Timed Security Protocols
    Li, Li
    Sun, Jun
    Liu, Yang
    Sun, Meng
    Dong, Jin-Song
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2018, 44 (08) : 725 - 746
  • [35] Security in Wireless Sensor Networks: A formal verification of protocols
    Nandi, Giann Spilere
    Pereira, David
    Vigil, Martin
    Moraes, Ricardo
    Morales, Analucia Schiaffino
    Araujo, Gustavo
    2019 IEEE 17TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2019, : 425 - 431
  • [36] ANALYZING ENCRYPTION PROTOCOLS USING FORMAL VERIFICATION TECHNIQUES
    KEMMERER, RA
    LECTURE NOTES IN COMPUTER SCIENCE, 1988, 293 : 289 - 305
  • [37] FORMAL TECHNIQUES FOR THE SPECIFICATION, VERIFICATION AND CONSTRUCTION OF COMMUNICATION PROTOCOLS
    CHOI, TY
    IEEE COMMUNICATIONS MAGAZINE, 1985, 23 (10) : 46 - 52
  • [38] A Framework for Formal Verification of Security Protocols in C plus
    Pradeep, R.
    Sunitha, N. R.
    Ravi, V
    Verma, Sushma
    INVENTIVE COMMUNICATION AND COMPUTATIONAL TECHNOLOGIES, ICICCT 2019, 2020, 89 : 163 - 175
  • [40] Formal verification of type flaw attacks in security protocols
    Long, BW
    ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2003, : 415 - 424