For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
An Algorithm for Allocating User Requests to Licenses in the OMA DRM System
Nikolaos TRIANTAFYLLOU Petros STEFANEAS Panayiotis FRANGOS
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2013/06/01
Online ISSN: 1745-1361
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>>
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.