Nuovo DRM Paradiso: formal specification and verification of a DRM
Hugo Jonker, S. Krishnan Nair, Mohammad Torabi Dashti · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2006
We present a DRM-preserving content redistribution scheme, based on the NPGCT scheme, that provides fairness in unsupervised exchanges. The proposed scheme is formally specified, verified and shown to achieve its design goals. The NPGCT mechanism of detection and revocation of circumvented devices is also reexamined here