RPKI增量同步Delta协议的形式化检测与实现

现有RPKI体系中，RPKI资料库与RP服务器之间的数据同步使用开源工具Rsync，但由于RPKI体系中证书数据结构的特殊性，使用Rsync进行数据的同步不仅效率低下，而且Rsync会消耗过多的系统资源，从而使整个RPKI体系遭遇潜在的安全风险.因此，IETF针对RPKI资料库数据特征，提出增量同步Delta协议以替代Rsync在RPKI中的作用.本文详细介绍了Delta协议的工作逻辑和机制，从安全性和高效性两方面将之与Rsync进行全面对比，并使用Promela语言构建Delta协议模型，借助形式化验证工具SPIN对该模型进行验证，从而证明该协议具备较高的协议安全性和稳定性.最后，本文给出Delta协议的实现结构.

Formal Verification and Implementation of RPKI Incremental Synchronous Delta Protocol

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.