一种可扩展的数字权限表达语言的形式化建模及分析

Formal Specification and Analysis of an Extended Digital Right Expression Language

为更清晰、精确表达DRM(digital right management)中权限这一关键问题,本文提出了一种可扩展的数字权限表达语言(EDREL:Extended Digital Right Expression Language)模型,并利用形式化方法(OTS/CafeOBJ建模方法),对该模型进行了形式化的建模与许可证性质分析.与现有研究相比,本文提出的模型及方法,在解决权限的准确、无二义性表达的同时,还加入了对授权方和被授权方发生权限纠纷时执行轨迹的判断与回溯的考虑以及权限的二次发布的描述,能更好地满足DRM系统中全面和精确地描述各种权限的需求.

To solve the key problem of DRM（Digital Right Management）,how to express right accurately and clearly,in this paper we propose a kind of EDREL（Extended Digital Right Expression Language）,and introduce formal method（OTS/CafeOBJ method） to formal specify and analyze the properties of license.Comparing with current research,our model and method solve the problem of the accurate and unambiguous expression of right;consider the recording of licensor and licensee,which is easier for solving the right tangle with checking and tracing the executing trace;as well as add the right re-distribution description.So it can meet the requirements in DRM system to express different kinds of right more comprehensively and accurately.