Formal digital license language with OTS/CafeOBJ method

This paper discusses how to model digital licenses as observational transition systems (OTSs) with CafeOBJ, a formal algebraic specification language. To extend the concept of licensing to cover various application domains of digital rights management, we first analyze the concepts of permission and obligation with some real-world examples which are not covered by current XML-based Rights Expression Languages (RELs), and then discuss how to formally specify licenses in terms of deontic and temporal logic with OTS/CafeOBJ method. Several important deontic and temporal modeling issues of licenses are also addressed for discussion. The proposed formal license language can be used not only for the formal specifications of licenses which capture both static observations and dynamic state transitions of the licenses, but also for the formal verification of licenses thanks to the executability and theorem proving facility of CafeOBJ.