This chapter presents an itinerary language, MAIL, which models the mobile behavior of proactive agents. It is an extension of the core itinerary constructs of the Naplet system. The language is structured and compositional so that an itinerary can be constructed recursively from primitive itineraries. We present its operational semantics in terms of a set of inference rules and prove that MAIL is expressive enough for most migration patterns. In particular, it is complete in the sense that it can specify any itineraries of regular trace models. Moreover, we show that MAIL is amenable to formal methods to reason about mobility and verify correctness and security properties.