Formal Specification and Verification of a DRM Protocol

Organisation:	Technical University Eindhoven (THE NETHERLANDS) Free University Amsterdam (THE NETHERLANDS) CWI (AMSTERDAM, THE NETHERLANDS)
Method:	muCRL (micro Common Representation Language) regular alternation-free mu-calculus
Tools used:	CADP (Construction and Analysis of Distributed Processes) (distributed) mCRL toolset
Domain:	Security Protocols.
Period:	2006
Size:	n/a
Description:	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.
Conclusions:	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 mu-calculus formulas."
Publications:	[Jonker-Nair-Dashti-06] 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
Contact:	H.L. Jonker Department of Mathematics and Computer Science Technical University of Eindhoven P.O. Box 513 5600 MB Eindhoven THE NETHERLANDS Tel: +31 40 - 247 5158 Fax: +31 40 - 247 5361 Email: h.l.jonker@tue.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page