NTT Research and Development 2012 Review of Activities

Overview

The anonymity and privacy of users are important issues in information system design. 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.

Features

• Mathematical formalization and rigorous verification of anonymity and privacy
• Flexibility in describing anonymity and privacy requirements through the use of Epistemic logic
• Efficient verification exploiting the symmetry (duality) between anonymity and privacy
• Formal anonymity and privacy verification of the FOO (Fujioka-Okamoto-Ohta) electronic voting protocol

Application scenarios

• Safe and secure e-commerce and e-government systems
  - Flexible requirement descriptions of individual systems using Epistemic logic
• Meets the ISO Evaluation Criteria for Information Technology Security
  - Formal methods are needed for evaluation assurance levels higher than EAL 4
• Clarifying the correspondence between legal and engineering requirements concerning privacy invasion
  - Bridging legal and engineering arguments by using a logical representation