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

• 作者: 司昊林 毛伟 王伟 邵晴 马迪
• 来源期刊: 计算机系统应用
• 关键词: RPKI Delta SPIN 增量同步 形式化检测 模型检查 协议安全性
• 年，卷（期）: 2018,（11）
• 所属期刊栏目: 专论·综述
• 页码范围: 1-8
• 页数: 8页
• 字数: 3394字
• 语种: 中文
• DOI: 10.15888/j.cnki.csa.006562

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王伟		295	3192	30.0	44.0
2	毛伟		57	536	11.0	21.0
6	马迪		8	126	5.0	8.0
7	司昊林	中国科学院计算机网络信息中心	1	1	1.0	1.0
16	邵晴		2	1	1.0	1.0