Formal modelling and verification of MCAC router architecture in ICN

Junya Xu, Huibiao Zhu, Lili Xiao, Jiaqi Yin, Yuan Fei, Gang Lu

科研成果: 书/报告/会议事项章节会议稿件同行评审

摘要

As Information Center Network (ICN) becomes a candidate for the future Internet architecture, its security and privacy issues have aroused extensive attention. Mandatory Content Access Control (MCAC) router architecture, which extends the existing mainstream ones with hardware-rooted trust, is proposed to implement MCAC protocol to protect privacy. Therefore, it is necessary to study the security of this architecture from the perspective of formal methods. In this paper, we use the process algebra Communicating Sequential Processes (CSP) to model and analyze MCAC router architecture in ICN. By adopting model checking tool Process Analysis Toolkit (PAT), we verify five important properties, namely Deadlock Freedom, Key Faking, Level Mechanism, Data Availability and Data Leaking. The results of verification show the correctness and security of MCAC router architecture, from which it can be concluded that this architecture is reliable.

源语言英语
主期刊名SEKE 2020 - Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering
出版商Knowledge Systems Institute Graduate School
222-227
页数6
ISBN(电子版)1891706500
DOI
出版状态已出版 - 2020
已对外发布
活动32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020 - Pittsburgh, Virtual, 美国
期限: 9 7月 202019 7月 2020

出版系列

姓名Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
PartF162440
ISSN(印刷版)2325-9000
ISSN(电子版)2325-9086

会议

会议32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020
国家/地区美国
Pittsburgh, Virtual
时期9/07/2019/07/20

指纹

探究 'Formal modelling and verification of MCAC router architecture in ICN' 的科研主题。它们共同构成独一无二的指纹。

引用此