Formal Proof of the IDOP_SP Protocol Based on the Petri Net

IDOP_SP (IPTV DRM interactive operating platform security protocol) protocol is a applied complicated protocol which distributes digital media content in the Internet. The flow of the protocol is based on the behavior of Web service composition and the digital content is transmitted to the customer in the form of hybrid digital objects. But the protocol security only can be assured after the protocol is formally analyzed and verified. In this paper, we use a Petri Net to model the IDOP_SP and verify the security of the IDOP_SP protocol based on the model. The result shows that the applied complicated protocol is secure which satisfies confidentiality, authentication and non-repudiation. It also shows that the Petri net is a good tool to verify the security of complicated protocols.