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

一种可扩展的数字权限表达语言的形式化建模及分析 Formal Specification and Analysis of an Extended Digital Right Expression Language 陈潇怡 CHEN Xiaoyi1 1 first-author 何炎祥 HE Yanxiang2 2 武汉大学经济与管理学院 武汉大学经济与管理学院 Economics and Management School,Wuhan University Economics and Management School,Wuhan University 武汉大学计算机学院 武汉大学计算机学院 School Computer,Wuhan University School Computer,Wuhan University 为更清晰、精确表达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. 数字版权管理 权限表达语言 形式化方法 形式化建模分析 OTS/CafeOBJ方法 digital right management right expression language formal methods formal specification and analysis OTS/CafeOBJ method 10.14188/j.1671-8836.2013.01.018 TP309;TP391.1 国家自然科学基金资助项目（91118003） 2013-01-01 2021-04-01 1 59