An Algorithm for Allocating User Requests to Licenses in the OMA DRM System


IEICE TRANSACTIONS on Information and Systems   Vol.E96-D   No.6   pp.1258-1267
Publication Date: 2013/06/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E96.D.1258
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal Methods
mobile DRM,  OMA,  order of rights object evaluation,  CafeOBJ,  safety,  invariant properties,  

Full Text: PDF>>
Buy this Article

The Open Mobile Alliance (OMA) Order of Rights Object Evaluation algorithm causes the loss of rights on contents under certain circumstances. By identifying the cases that cause this loss we suggest an algebraic characterization, as well as an ordering of OMA licenses. These allow us to redesign the algorithm so as to minimize the losses, in a way suitable for the low computational powers of mobile devices. In addition we provide a formal proof that the proposed algorithm fulfills its intent. The proof is conducted using the OTS/CafeOBJ method for verifying invariant properties.