2004/05/18 by Riccardo Pucella, Pucella, Riccardo, Vicky Weissman +1
Computer Science · #Cryptography and Security (cs.CR) #D.4.6 #F.4.1 #FOS: Computer and information sciences #K.6.5 #Logic in Computer Science (cs.LO) #cs.CR #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0405066
21 pages. Appeared in the Proceedings of the 15th IEEE Computer Security Foundations Workshop, pp. 282-294, 2002
arxiv created 2004/05/18 · arxiv updated 2009/12/01
We present a logic for reasoning about licenses, which are ``terms of use'' for digital resources. The logic provides a language for writing both properties of licenses and specifications that govern a client's actions. We discuss the complexity of checking properties and specifications written in our logic and propose a technique for verification. A key feature of our approach is that it is essentially parameterized by the language in which the licenses are written, provided that this language can be given a trace-based semantics. We consider two license languages to illustrate this flexibility.