This paper introduces a new expressive theory of types for the
higher-order pi-calculus and demonstrates its applicability via two
security analyses for higher-order code mobility. The new theory
significantly improves our previous one presented in
[Yoshida and Hennessy 2002] by the use of channel dependent/existential
types. New dependent types control dynamic change of process
accessibility via channel passing, while existential types guarantee
safe scope-extrusion in higher-order process passing. This solves an open
issue in [Yoshida and Hennessy 2002], leading to significant
enlargement of original typability. The resulting typing system is
coherently integrated with the linear/affine typing disciplines as
well as state, concurrency and distribution, allowing precise analysis
of software behaviour with higher-order mobility. As illustration of
the usage of the typed calculus, two basic security concerns for
mobile computation, secrecy for data confidentiality and role-based
access control for authorised resources, are analysed in a uniform
type-based framework, leading to the noninterference theorem and
authority-error freedom in the presence of higher-order code mobility.
