Nuovo DRM Paradiso : formal specification and verification of a DRM protocol
HL Hugo Jonker, S. Krishnan Nair, Mohammad Torabi Dashti · 2006
Abstract. We present a DRM-preserving content redistribution scheme, based on the NPGCT scheme [15], 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.