Formal modelling and verification of MCAC router architecture in ICN

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.