In [2] a model for mobility, called Petri hypernets, was presented. Hypernets offer a visual formalism to describe hierarchically structured dynamic agents. The agents take the form of Petri nets, which manipulate other agents as resources. In [4] a logic was proposed in which one can describe the temporal and the structural properties of agents in a hypernet. One can also analyse some properties of hypernets expressible as Petri net invariants thanks to the translation of hypernets to 1-safe Petri net systems given in [3]. Recently, see [1], we have addressed the problem of modelling complex, hybrid discrete agent systems in a modular way. The idea here is to obtain the view of the complete system from a number of simpler views, each devoted to a specific perspective. One view, for instance, could describe how some mobile agents can evolve in time — this view could be captured as a hypernet. Another could address other issues, for instance the rights of an agent to read some messages. The purpose of the talk is to describe how the approach can be used to model, specify and verify some security aspects of mobile agent systems.