Algebraic Specifications for OMA REL Licenses

OMA-Digital Rights Management System is a standard proposed by Open Mobile Alliance for protecting digital content distributed through mobile networks. In such a system, licenses are written in an appropriate language and used to ensure the fine grained consumption of contents. We claim that the Rights Expression Language (OMA-REL) does not rely on formal semantics. To address this problem we propose an abstract syntax for OMA-REL and write an algebraic specification of it using CafeOBJ, an executable algebraic specification language, with the future goal the creation of automated tools that check the behavior of a set of licenses under a certain environment.