The Seal calculus is a distributed process calculus in which locations and movement of computational entities are explicit. The calculus is targeted at secure distributed applications over large scale open networks such as the Internet. Security is addressed by a fine-grained access control mechanism. In [14] we motivated the design choices. Here we develop some technical tools, which include both a reduction and a commitment semantics and observational equivalences, to allow us to state and formally verify properties of mobile programs. In particular for studying security, we develop the notion of confinement. Confinement is essential for security; as it expresses that an execution environment has complete control over the communication capabilities of the programs that are running within it.