This technical report presents the syntax and semantics, in terms of transition system, of the messenger paradigm as it has been presented in [8]. Messengers are mobile agents able to collaborate and to coordinate their work, but are not considered as intelligent agents. More precisely, messengers are mobile codes exchanged between messenger platforms. Arriving messengers are immediately executed (interpreted) by platforms. Messengers communicate by the means of a global store, synchronize their execution using process queues, create new messengers and move themselves across the network using appropriate instructions. The purpose of this mathematical formalization is to give a mathematical definition to the basic ingredients of the messenger paradigm: communication through global store, synchronization through process queues, creation of new messengers, and mobility. This formalization is neither concerned with families of messengers collaborating to solve a common goal, nor with the notion of messenger taking part to a service. Further work will be concerned with the choice of a formalism well suited for messengers' specifications.