Development of system to verify the unforgeability of cryptographic protocols

1999 Fiscal Year Final Research Report Summary

• Project/Area Number: 10650361
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: 情報通信工学
• Research Institution: Osaka University
• Principal Investigator: FUJIWARA Toru Graduate School of Engineering Science, Osaka University Professor, 基礎工学研究科, 教授 (70190098)
• Project Period (FY): 1998 – 1999
• Keywords: Information Security / Cryptography / Cryptographic Protocols / Database / Formal verification / Security / Unforgeability / Algorithm

Research Abstract

The purpose of this research is (1) to describe the unforgeability of data for cryptographic protocols,(2) determine classes for which the unforgeability is decidable, and (3) develop a system to verify the unforgeability.
1. Formal description : Operations provided in the protocol including the operations which enemy can execute are representer by functions. Data which the enemy can obtain are represented by terms. Relations between functions are described by axioms. Also, legal operation for obtaining the target data is represented by a term.
2. Decidable class : we obtained an sufficient condition under which the problem is decidable.
3. We developed an algorithm which works effectively for practical protocols. The problem is translated into the emptiness problem of a regular language. The number of edges from a state in the finite automata which accepts the language is not many. Using properties like this, we developed the algorithm.
4. The unforgeability problem can be applied to related problems, say the security of databases. For the illegal data access for a database, we formalize the decision problem for the security, and developed the decision algorithm.