Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2013/06/01 Vol. E96-DNo. 6pp. 1258-1267 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Formal Methods Keyword: mobile DRM, OMA, order of rights object evaluation, CafeOBJ, safety, invariant properties,