System threat analysis requires a wide range of knowledge and is time-consuming. In this study, we propose FSTM system, a method to visualize threats in the system to support threat modeling using a formal verification tool. Concretely, given a security requirement and a system model, we represent what kind of attacks are enabled to prevent the system from satisfying the security requirement using an AND-OR tree based on exhaustive formal verification. To generate an exhaustive AND-OR tree, a large number of system models modified to enable various attack patterns and verification costs are required because verification results must be obtained for all threat patterns. We used the property that we call monotonicity of security to reduce the number of verifications and automatically generate a verification model for each threat pattern from a single verification model. We implemented FSTM system using Tamarin Prover, a formal verification tool, and evaluated it with case studies.

In this study, we designed and evaluated the Se-cure Optical Transport Network (SOTN) architecture, which is expected to be the mainstream of communications between datacenters in the future. We evaluated the security using for-mal 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 veri-fication 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.