TY - GEN
T1 - Formal modelling and verification of MCAC router architecture in ICN
AU - Xu, Junya
AU - Zhu, Huibiao
AU - Xiao, Lili
AU - Yin, Jiaqi
AU - Fei, Yuan
AU - Lu, Gang
N1 - Publisher Copyright:
© 2020 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - CSP
KW - ICN
KW - MCAC Router Architecture
KW - Modeling
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85090507569&partnerID=8YFLogxK
U2 - 10.18293/SEKE2020-048
DO - 10.18293/SEKE2020-048
M3 - 会议稿件
AN - SCOPUS:85090507569
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 222
EP - 227
BT - SEKE 2020 - Proceedings of the 32nd International Conference on Software Engineering and Knowledge Engineering
PB - Knowledge Systems Institute Graduate School
T2 - 32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020
Y2 - 9 July 2020 through 19 July 2020
ER -