Development of system to verify the unforgeability of cryptographic protocols

本研究的目的是：(1)描述加密协议数据的不可伪造性，(2)确定不可伪造性可判定的类别，以及(3)开发验证不可伪造性的系统。形式描述：协议中规定的操作，包括敌人可以执行的操作，用函数表示。敌人可以获得的数据用术语表示。函数之间的关系由公理来描述。另外，获取目标数据的合法操作用术语表示。可判定类：我们得到了问题可判定的充分条件。我们开发了一种算法，有效地适用于实际协议。这个问题被翻译成常规语言的空性问题。在接受语言的有限自动机中，来自某一状态的边数并不多。利用这样的属性，我们开发了算法。不可伪造性问题可以应用于相关问题，例如数据库的安全性。针对数据库的非法数据访问，形式化了安全决策问题，并开发了决策算法。

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.