The recent innovation of telecommunication and networking technology is enabling easy and flexible distribution of digital multimedia contents. However, such rapid progress has brought about various problems on intellectual properties and security. We are investigating a technique to solve the problem called active contents based on hierarchical structures of mobile agents. The agents work as wrappers of contents and can easily manage the policies for contents distribution. In this paper, we give a formal model of active contents in order to establish rigorous foundations for the active contents technique, especially the system of the policy control mechanisms. Using the model, we can verify if the behaviors of the active contents satisfy the given policies or not. An example of the redistribution prohibition policy illustrates how the verification works.