Protecting customer privacyFormal verification technology for anonymity and privacyNTT Communication Science Laboratories

The protection of user personal information is important in the design of information systems. In particular, user anonymity and privacy protection are important issues in information system design. However, until now, there have been no rigorous, general-purpose methods of verifying how information systems protect anonymity or privacy. This is due to the difficulty of rigorously defining anonymity and privacy, as well as the fact that it would take a great deal of time to exhaustively examine all the state transitions of the system.

In this technology, the concept of anonymity and privacy is expressed rigorously (formally) using mathematical logic, with the idea that anonymity is concealing "who" and privacy is concealing "what." It then mathematically proves on a computer whether an information system protects anonymity and privacy. Proofs can be made more efficient by using a mathematical concept called "duality." Using this technology, we have successfully verified the anonymity and privacy of the FOO Internet electronic voting protocol. The application of this technology enables the verification of information systems that require a high level of security.

• Formal formulation and rigorous verification of anonymity and privacy using mathematical methods
• Epistemic logic provides flexibility in describing the properties (anonymity, privacy) that the system should satisfy
• Efficient safety verification using symmetry of anonymity and privacy
• Applicable to information systems that require high security, such as e-voting, e-commerce, and e-government

This technology is used to rigorously verify that the designed information system protects the anonymity and privacy of its users. The behavior of a system is described by a state transition model (automaton). Anonymity and privacy, which are requirement specifications, are described using a logical system called "epistemic logic." The expressive power of epistemic logic provides the flexibility to express sensitive requirements.

One of the features of this technology is that it provides a formal and generic way of formulating information systems through epistemic logic. Another feature of this technology is that it enables efficient verification by using duality to commonize verification tasks in terms of anonymity and privacy. Specifically, the intermediate property of role interchangeability is demonstrated by simulation of a state transition machine, from which anonymity and privacy are derived. Role interchangeability is symmetrical to itself, and the proof can be shared.

Formal
To be rigorous in describing and analyzing a subject, using mathematics and mathematical logic.

FOO Internet Voting Protocol
An electronic voting protocol developed by Fujioka, Okamoto, and Ota (currently at University of Electro-Communications) of NTT Information Sharing Platform Laboratories. The application of a cryptographic technique called "blind signatures" enables practical Internet electronic voting.

State transition model
A theoretical model (automaton) that describes the behavior of a system with only a collection of states and the transition rules between them.

Epistemic logic
A logical system that can describe not only true or false, but also "it is known that" or "it is not known that."

Role interchangeability
A property where even if you and another person switch roles, you cannot tell from the outside

NTT Communication Science Laboratories - Media Information Laboratory