Security Verification using Formal Methods

If we are to use electronic voting or electronic commerce systems with confidence, we must ensure their safety.
We must find a way to verify that the protocols used in the network systems satisfy various desired security requirements including non-leakage of important information and protection against spoofing attacks. However, the verifications of complicated protocols utilizing high-level cryptographic techniques are often error-prone.
We are conducting research on security verification with formal methods. Formal methods are schemes designed to provide rigorous verification of the correctness of information systems based on accomplishments in mathematics and mathematical logic research. By applying such methods to cryptographic protocols, we can ensure that network systems offer a high level of security.

We have two approaches for making formal methods applicable to the various security requirements of all systems.

Verification of more complicated properties
To verify a security requirement or property using formal methods, we first need to formulate it in a formal way. This poses no problem for such simple properties as secrecy (e.g., protecting credit card numbers) or authenticity (e.g., protection against spoofing). However, when we expand the target to more complex properties such as anonymity (concealing who voted for Obama) and privacy (avoiding unreasonable surveillance by sensors), the formulation itself becomes a problem.

Verification of higher precision
Formal methods allow us to realize rigorous and automated protocol verification using tools such as theorem proving or model checking systems. However, there is a drawback regarding verification precision: we need some form of idealization or simplification for assumptions related to cryptographic systems (e.g., the probability of breaking the cryptographic scheme is zero). Recently, extensive studies are being undertaken to make the assumptions more realistic.

We developed a method for formalizing and verifying anonymity and privacy based on the view that they are information-hiding properties concerning the link between people and actions. In this view, anonymity and privacy are symmetric to each other, which can be considered a kind of duality in mathematics. This symmetry gives us a clear perspective for requirement formulation and is beneficial for verification efficiency. As an example, we verified the anonymity and the privacy of the FOO electronic voting protocol proposed by Fujioka, Okamoto, and Ohta in 1992.

The approaches of cryptography and formal method approaches of security analysis are diverging. Cryptographers performed analyses under the realistic assumption that cryptanalysis might succeed with some small probability. On the other hand, for the sake of automated verification, formal methods assumed that cryptanalysis never succeeded. This sacrificed the precision of verification. Recently, extensive studies are making the assumptions more realistic.
We have developed a high-precision automated verification method for protocols using hash functions whose formal handling under realistic assumptions was generally believed to be impossible.