微信服务号

微信订阅号

2025-4-8- 4
Home > Archive>Volume 32, Issue 6, 2021 >1581-1596. DOI:10.13328/j.cnki.jos.006238
PDF HTML XML Export Cite reminder
C2P: Formal Abstraction Method and Tool for C Protocol Code Based on Pi Caculus
Author:
Affiliation:

Fund Project:

National Key Research and Development Program of China (2019QY1302)

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Formal method provides a theoretical tool for security protocol analysis, but the theoretical security is not equivalent to the actual security. A verified protocol standard may not meet the required security properties when converted into a concrete program. Hence, a formal verification method for detecting semantic logic errors in security protocol code is proposed. By automatically abstracting the C source code of the protocol into Pi calculus model, protocol security properties are verified based on the Pi calculus. Finally, the correctness of the scheme transformation is proved and the validity of the method is verified by a Kerberos protocol instance code. C2P tools implemented can help protocol developers to detect semantic logic errors in code.

    Reference
    Related
    Cited by
Get Citation

张协力,祝跃飞,顾纯祥,陈熹. C2P:基于Pi演算的协议C代码形式化抽象方法和工具.软件学报,2021,32(6):1581-1596

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 29,2020
  • Revised:December 19,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063