Technical University Eindhoven (THE NETHERLANDS)
Free University Amsterdam (THE NETHERLANDS)
CWI (AMSTERDAM, THE NETHERLANDS)
muCRL (micro Common Representation Language)
regular alternation-free mu-calculus
CADP (Construction and Analysis of Distributed Processes)
(distributed) mCRL toolset
A challenge in DRM (Digital Rights Management) techniques is to
enforce DRM policies after the content has been distributed to
consumers. Currently, this issue is solved by limiting the
distribution to compliant devices only. This case study describes the
design and verification of a new protocol, called Nuovo DRM, allowing
that consumers can not only buy the right to use a content, but also
to redistribute or resell the content in a controlled manner.
The verification approach uses several steps. First, the Nuovo DRM protocol and the intruder are formalised in muCRL. Each participant of the protocol is modeled as a separate process. Second, the requirements of the protocol are expressed as formulas in the regular alternation-free mu-calculus. Third, the muCRL toolset is used to generate the LTS (Labeled Transition System) corresponding to the formal specification of the protocol. Finally, EVALUATOR is used to verify the requirements of the protocol using the generated LTS.
The protocol is verified for two scenarios, both consisting of two compliant devices. The first scenario assumes that the network is operational and that no malicious agent is presented. In this case, the CADP toolbox allows to prove the absence of deadlocks, that each request is eventually answered, and that each reception of a content is preceded by its payment. In the second scenario, an intruder has control over the network and the compliant devices. In this case, the CADP toolbox allowed to verify that no protected content is revealed to any non-compliant device, that the protocol resists masquerading attacks, and that the protocol is fair.
Formal analysis and verification increases the confidence in the
correctness of security protocols by helping to find issues overlooked
by protocol designers. As regards CADP, the authors state that
EVALUATOR is "capable of efficiently checking alternation-free
H.L. Jonker, S. Krishnan Nair, and M. Torabi Dashti.
"Nuovo DRM Paradiso: Formal Specification and Verification of a DRM
Protocol". In Proceedings of the 1st Benelux Workshop on
Information and System Security WISSec 2006 (Antwerpen, Belgium),
Lecture Notes in Computer Science. Springer Verlag, November 2006.
Full version available on-line at: http://www.win.tue.nl/~hjonker/publications/nuovo-drm-techreport.pdf
or from the CADP Web site in PDF or PostScript
[Dashti-Nair-Jonker-08] Mohammad Torabi Dashti, Srijith Krishnan Nair, and Hugo Jonker. "Nuovo DRM Paradiso: Designing a Secure, Verified, Fair Exchange DRM Scheme". In Fundamenta Informaticae, volume 89, number 4, pp. 393-417, 2008.
Full version available from the CADP Web site in PDF or PostScript
Department of Mathematics and Computer Science
Technical University of Eindhoven
P.O. Box 513
5600 MB Eindhoven
Tel: +31 40 - 247 5158
Fax: +31 40 - 247 5361
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|