Architecture Design and Security Evaluation of Secure Optical Transport Network Using Formal Verification

In this study, we designed and evaluated the Secure Optical Transport Network (SOTN) architecture, which is expected to be the mainstream of communications between datacenters in the future. We evaluated the security using formal verification and proposed countermeasures against possible adversary models. For the architecture design and evaluation, we referred to IPsec, which is the de-facto standard protocol for communication between datacenters. For the security evaluation, we used ProVerif, which is the de-facto standard of formal verification tools for cryptographic protocols. This study shows that an unknown attack (called the Key Compromised Disagreement (KCD) attack) is detected in the assumed adversary models and that the proposed countermeasures can reduce the impact of the KCD attack. The results suggest that unknown attacks can occur even for individually secure devices depending on their combinational and architectural designs and that the security of the entire architecture can be improved by applying an enhanced authentication mechanism to a specific communication channel.