Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol
CSTR:
Author:
Affiliation:

Clc Number:

Fund Project:

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

    In the existing RPKI system, the open source tool Rsync is used to synchronize data between the RPKI databases and the RP servers. However, due to the particularity of the certificate data structure in the RPKI system, data synchronization using Rsync not only is inefficient, but also consumes too much system resources, so that the entire RPKI system suffers potential security risks. Therefore, the IETF proposes an incremental synchronization Delta protocol to replace Rsync's role in RPKI. This paper introduces the working logic and mechanism of Delta protocol in detail, compares it with Rsync in terms of security and efficiency, constructs the Delta protocol model by using Promela language, and verifies the model with formal verification tool SPIN. It proves that the protocol has high protocol security and stability. Finally, this paper presents the Delta protocol implementation structure, in order to offer reference and communication.

    Reference
    Related
    Cited by
Get Citation

司昊林,马迪,毛伟,王伟,邵晴. RPKI增量同步Delta协议的形式化检测与实现.计算机系统应用,2018,27(11):1-8

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:February 09,2018
  • Revised:March 07,2018
  • Adopted:
  • Online: September 30,2018
  • Published:
Article QR Code
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address:4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code:100190
Phone:010-62661041 Fax: Email:csa (a) iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063