Modelling IP Mobility.
We study a highly simplified version of the proposed mobility support in version 6 of Internet Protocols (IP). We concentrate on the issue of ensuring that messages to and from mobile agents are delivered without loss of connectivity. We provide three models, of increasingly complex nature, of a network of routers and computing agents that are interconnected via the routers: the first is without mobile agents and is treated as a specification for the next two&semi; the second supports mobile agents, and the third additionally allows correspondent agents to cache the current location of a mobile agent. Following a detailed analysis of the three models to extract invariant properties, we show that the three models are related by a suitable notion of equivalence based on barbed bisimulation. Finally, we report on some experiments in simulating and verifying finite state versions of our model.
Introduction
We study the modelling of mobile hosts on a network using a simple process
description language, with the intention of being able to prove properties about a
protocol for supporting mobility. The present case study grew out of our interest in
understanding the essential aspects of some extant mechanisms providing mobility
support.
Indeed, the model we study may be considered an extreme simplification of
proposals for mobility support in version 6 of Internet Protocols (IP) [IDM91,
This work was supported under the aegis of IFCPAR 1502-1. An extended abstract of this
paper appears in the Proceedings of CONCUR 98.
y Corresponding author. CMI (LIM), 39 rue Joliot-Curie, F-13453, Marseille, France.
amadio@gyptis.univ-mrs.fr. Partly supported by CTI-CNET 95-1B-182, Action Incitative IN-
z IIT Delhi, New Delhi 110016, India. sanjiva@cse.iitd.ernet.in. Partly supported by AICTE
1-52/CD/CA(08)/96-97.
TUSM94, JP96] 1 . IPv6 and similar mobile internetworking protocols enable messages
to be transparently routed between hosts, even when these hosts may change
their location in the network. The architecture of the model underlying these solutions
may be described as follows: A network consists of several subnetworks,
each interfaced to the rest of the network via a router. Each node has a globally
unique permanent identification and a router address for routing messages to it,
with a mapping associating a node's identifying name to its current router address.
The router associated by default with a node is called its "home router". When
a mobile node moves to a different subnet, it registers with a "foreign" router
administering that subnet, and arranges for a router in its home subnet to act
as a "home" proxy that will forward messages to it at its new "care-of address".
Thus any message sent to a node at its home router can eventually get delivered
to it at its current care-of address. In addition, a mobile node may inform several
correspondent nodes of its current location (router), thus relaxing the necessity
of routing messages via its home subnet. This model, being fairly general, also
applies to several mobile software architectures.
The particular issue we explore here, which is a key property desired of most
mobility protocols, is whether messages to and from mobile agents are delivered
without loss of connectivity during and after an agent's move. Although IP does
not guarantee that messages do not get lost, we model an idealized form of Mobile
IPv6 without message loss, since the analysis presented here subsumes that
required for Mobile IP with possible loss of messages.
We should clarify at the outset that we are not presenting a new architecture
for mobility support; nor are we presenting a new framework or calculus for mo-
bility. Rather, our work may be classified as protocol modelling and analysis: We
take an informal description of an existing protocol, idealize it and abstract away
aspects that seem irrelevant to the properties we wish to check or which are details
for providing a particular functionality, then make a model of the simplified
protocol and apply mathematical techniques to discover the system structure and
its behavioral properties.
We believe that this approach constitutes a useful way of understanding such
protocols, and may assist in the formulation and revision of real-world protocols
for mobile systems. From the informal descriptions of mobility protocols in the
literature, it is difficult to assure oneself of their correctness. As borne out by
our work, the specification and combinatorial analysis of such protocols is too
complicated to rely on an informal justification.
The literature contains various related and other proposals for mobility sup-
port, for example, in descriptions of kernel support for process migration [PM83,
runtime systems for migrant code [BKT92, JLHB88]. A significant
body of work concerns object mobility support in various object-based
software architectures, see, e.g., [Dec86, Piq96, VRHB While these studies
address several other issues relevant to software mobility (e.g., garbage collection),
1 We do not model various aspects of network protocols for mobility. In particular, we totally
ignore security and authentication issues, as well as representational formats and conventions
in network packets, e.g., encapsulation/decapsulation of messages, and tunneling. Broadcast is
not dealt with at all.
we are not aware of any complete modelling and analysis in those settings that
subsumes our work.
We have recently learnt of a "light-weight" formal analysis of the IPv6 protocol
[JNW97]. In that work, Nitpick, a tool that checks properties of finite binary relations
and generates counter-examples, is applied to a finite instance of an abstract
version of the IPv6, to verify that messages do not travel indefinitely in cycles 2 .
The approach is quite similar in spirit to our work summarized in Appendix B,
and uses inductive invariants to verify a cache acyclicity property. This property
is one of those that arise in our analysis presented in x4.3. The Nitpick analysis
focuses on the particular cache management policy suggested for IPv6 together
with timestamping of messages (which requires a protocol for approximating a
global clock), whereas our analysis shows that any cache management policy that
satisfies a particular invariant will ensure correctness.
The literature also contains a number of frameworks for describing mobility
protocols, such as the extension of Unity called Mobile Unity [MR97, PRM97,
RMP97]. One should distinguish the "analysis of protocols for mobility" from
the "definition of models or calculi for mobility"; mobility protocols provide an
implementation basis for the latter, just as, e.g., garbage collection algorithms
provide an implementation basis for functional programming. While we agree that
frameworks including the dynamic generation of names and processes as primitive
operations, such as the -calculus and related formalisms [MPW92, AMST97],
may be suitable for describing mobile systems, we believe that our work provides
some evidence for the assertion that these primitives are not always necessary
nor always appropriate for describing and analyzing mobility protocols. Further,
there is no need to develop an "ad hoc" (in the original, non-pejorative sense)
formalism for analyzing mobility protocols.
The structure of the paper reflects our analysis methodology. After introducing
our language for modelling the protocol (x2), we present a model of the
protocol (x3), and then look for its essential structure in the form of a big invariant
(x4). From this analysis, we gather some insight on why the protocol
works correctly, and suggest some variations. We present the protocol model in
stages, giving three models of increasingly complex nature of a network of routers
and computing agents that are interconnected via the routers. In the first (x3.1),
which we call Stat, computing agents are not mobile. We extend Stat to a system
Mob where agents can move from a router to another (x3.2). Finally, to reduce
indirection and to avoid excessive centralization and traffic congestion, we extend
the system Mob to a system CMob, where the current router of an agent may be
cached by its correspondent agents (x3.3). In x4, we analyze these three different
models, and establish the correspondence between them by showing that systems
Stat, Mob and CMob are barbed bisimilar, with respect to a suitable notion of
observation. We conclude in x5, by summarizing our contributions, recalling the
simplifications we have made, and reporting on some simulation and automatic
verification experiments on a finite-state formulation of the protocol.
The paper need not be read sequentially. By reading x3.1, x3.2 and glancing
In IPv6, messages can in fact travel in cycles. Consider the case where a node keeps moving
in a ring and a message is always being forwarded to it one step behind.
at x4.1, x4.2 the reader will have a general idea of the basic systems Stat and
Mob (in particular Figure 4 should provide a good operational intuition) and of
the techniques we apply in their analysis. The more challenging system CMob,
whose size is about twice the size of Mob, is described in x3.3 and analyzed in
x4.3. The reader motivated by the formal analysis, will have to take a closer look
at the invariants described in Figures 10, 12. Understanding the invariants is
the demanding part, the related proofs (which are in Appendix are basically
large case analyses that require little mathematical sophistication. The footnotes
comment on the relationship between our model and the IP informal specification.
They are addressed mainly to the reader familiar with IP, and they can be skipped
at a first reading. Finally, the reader interested in the finite state version of
the protocol, can get a general overview of the issues in x5, and more details in


Appendix

B.
2 The Process Description Language
We describe the systems in a standard process description language. The notation
we use is intended to be accessible to a general reader, but can be considered an extension
of a name-passing process calculus with syntactic sugar. A system consists
of some asynchronous processes that interact by exchanging messages over channels
with unlimited capacity (thus sending is a non-blocking operation, whereas
attempting to receive on an empty channel causes the process to block). Messages
in the channels can be reordered in arbitrary ways. Processes are described as
a system of parametric equations. The basic action performed by a process in
a certain state is: (i) (possibly) receiving a message, (ii) (possibly) performing
some internal computation, (iii) (possibly) emitting a multiset of messages, and
(iv) going to another state (possibly the same).
There are several possible notations for describing these actions; we follow the
notation of CCS with value passing. We assume a collection of basic sorts, and
allow functions between basic sorts to represent cache memories abstractly. The
functions we actually need have a default value almost everywhere and represent
finite tables.
Let names, values of basic sorts, and functions from
basic sorts to sorts. x stands for a tuple x . The expressions T;
over name equality tests; are process identifiers, and V;
value domains. Processes are typically denoted by are specified by
the following grammar:
Here, 0 is the terminated process, x(x):p is the input prefix, xx is a message, j is
the (asynchronous) parallel composition operator, and [T ]p; p 0 is a case statement.
We write \Pi i2I p i to denote an indexed parallel composition of processes. X(x) is
a process identifier applied to its actual parameters; as usual for every process
identifier X, there is a unique defining equation such that all variables
are contained in fxg. \Phi is the internal choice operation, where in p
we substitute a non-deterministically chosen tuple of values (from appropriate
domains, possibly infinite) for the specified tuple of variables. We use internal
choice to abstract from control details (note that internal choice can be defined
in CCS as the sum of processes guarded by a - action).
Being based on "asynchronous message passing over channels", our process description
language could be regarded as a fragment of an Actor language [AMST97]
or of an asynchronous (polyadic) -calculus [HT91]. The main feature missing is
the dynamic generation of names. As we will see in x3.2, it is possible to foresee
the patterns of generation, and thus model the system by a static network of
processes.
We define a structural equivalence j on processes as the least equivalence relation
that includes: ff-renaming of bound names, associativity and commutativity
of j, the equation unfolding and:
Reduction is up to structural equivalence and is defined by the following rules:
These rules represent communication, internal choice and compatibility of reduction
with parallel contexts, respectively. Using these rules, we can reduce a
process if and only if (i) employing structural equivalence we can bring the process
to the form p j q, and (ii) the first or second rule applies to p.
We introduce the following abbreviations:
if
3 The Model
We describe three systems Stat , Mob, and CMob. All three consist of a collection
of communicating agents that may interact with one another over the network.
Each agent is attached to a router, with possibly many agents attached to the
same router. We assume that each entity, agent or router, has a globally unique
identifying name. For simplicity, we assume a very elementary functionality for
the agents - they can only communicate with other agents, sending or receiving
messages via the routers to which they are attached. The agents cannot communicate
directly between themselves, all communication being mediated by the
routers. We assume that routers may directly communicate with one another,
abstracting away the details of message delivery across the network. The communication
mechanism we assume is an asynchronous one, involving unbounded
buffers and allowing message overtaking.
We assume a collection of names defined as the union of pairwise disjoint sets
Agent Names
The set CN of Control Directives has the following elements (the Control Directives
that we consider in Stat consist of exactly msg, to indicate a data message;
the directives fwdd and upd will be used only in CMob):
msg message regd registered infmd informed fwdd forwarded
immig immigrating repat repatriating mig migrating upd update
The sets AN and DN are assumed to be non-empty. The elements of RN and
LAN are channel names that can carry values of the following domain (note that
the sort corresponding to the set RN is recursively defined):
AN \Theta RN \Theta AN \Theta RN \Theta DN
Elements of this domain may be interpreted as:
[control directive; to agent ; at router ; from agent ; from router ; data ]
We often write x to stand for the tuple [x
indicates that the name is irrelevant ("don't care''). The tables L and H are used
for the address translation necessary to route a message to its destination. L is
an injective function that gives the local address for an agent at a given router,
H computes the "home router" of an agent.

Tables

We denote with obs(x) an atomic observation. If z[x] is a message, we call
the triple [x its observable content (original sender, addressee and data).
We assume a distinguished channel name o on which we can observe either the
reception of a message or anomalous behavior, represented by a special value ffl.
3.1 The system without mobility Stat
In

Figure

1, we present (formally) the system Stat .
Agents An agent A(a) either receives a message from its home router on its local
address and observes it, or it generates a message to a correspondent agent that
it gives to its home router for delivery to the correspondent agent via the latter's
AN \Theta RN \Theta AN \Theta RN \Theta DN
in (a)
in r 0 [msg;
A in (a)
in
Router
in lx j Router (r)

Figure

1: System without mobility
home router. L(H(a); a) represents the local address of the agent a in its home
subnet 3 .
Router The router examines an incoming message, and if it is the destination
router mentioned in the message, accordingly delivers it to the corresponding
agent. Otherwise it sends it to the appropriate router. L(r; x 2 ) is the local address
of x 2 , the addressee of the message, whereas x 3 is the destination router.
3.2 The system with mobility Mob
We now allow agents to migrate from one router (i.e., subnet) to another. While
doing so, the agents and routers engage in a handover protocol [JP96]. When
an agent moves to another router, a proxy "home agent" at its home router 4
forwards messages intended for the mobile agent to a "care-of address" 5 , the
agent's current router. To avoid message loss, the forwarding home agent should
have an up-to-date idea of the current router of the mobile agent. Hence when
a mobile agent moves, it must inform the home agent of its new coordinates. In
the first approximation, we model all messages addressed to a mobile agent being
3 We have used nondeterminism to model actions arising from the transport or higher layers
corresponding to processing a received message, or generating a message to a correspondent
agent. Communication on the LAN channels abstracts link-level communication between the
router and the agent. We have a simplifying assumption that a node can be on-link to only one
router.
4 For simplicity, we identify the routers serving as mobility agents / proxies with the routers
administering a subnet. We also assume that each router is always capable of acting as a home
or foreign agent.
5 We model only what are called "foreign agent care-of addresses" and not "co-located care-of
addresses" in IPv6 parlance.
forwarded via the home agent; later we will consider correspondent agents caching
the current router of a mobile agent. The router description remains unchanged.
We observe that the migration of a mobile agent from one router to another
can be modelled "statically": for each router, for each agent, we have a process
that represents the behavior of a mobile agent either being present there or absent
there, or that of a router enacting the role of a forwarder for the agent, routing
messages addressed to that agent to its current router. Migration may now be described
in terms of a coordinated state change by processes at each of the locations
involved 6 .
Although the model involves a matrix of shadow agents running at each router,
it has the advantage of being static, in terms of processes and channels, requiring
neither dynamic name generation nor dynamic process generation. The conceptual
simplicity of the model is a clear advantage when carrying on proofs which
have a high combinatorial complexity, as well as when attempting verification
by automated or semi-automated means. For instance, the only aspect of the
modelling that brings us outside the realm of finite control systems is the fact
that channels have an infinite capacity, and there is no bound on the number of
messages generated. Starting from this observation, it is possible to consider a
revised protocol which relies on bounded channels (see Appendix B).
In the commentary below, we refer to various processes as agents. Note that
only the agents Ah, Ah in , Ma and Ma in correspond to "real" agents, i.e., the
behavior of mobile nodes. The others may be regarded as roles played by a router
on a mobile node's behalf. Their analogues in IPv6 are implemented as routers'
procedures that use certain tables.
States of the agent at home We describe an agent at its home router in

Figure

2.
Ah The mobile agent is at its home base. It can receive and send messages,
as in the definition of A(a) in Figure 1, and can also move to another router.
When the agent "emigrates", say, to router u, it changes state to Ham(a). We
model the migration by the agent intimating its "shadow" at router u that it is
"immigrating" there, and to prepare to commence operation 7 .
Ham The mobile agent during emigration. We model the agent during "emigra-
tion" by the state Ham(a). During migration, messages addressed to the agent
may continue to arrive; eventually, these messages should be received and handled
by the mobile agent. The emigration completes when the shadow agent at the
target site registers (by sending control message regd) its new care-of router
at the home base. The agent is ready to operate at that foreign subnet once it
6 Thus, our formalization of the migration of an agent, involving the small coordinated state
change protocol, may be considered an abstraction (rather than a faithful representation) of some
of the actions performed when a mobile node attaches itself to a new router and disengages itself
from an old one.
7 Registration is treated in a simple fashion using the immig and repat messages, ignoring
details of Agent Discovery, Advertisement, Solicitation, and protocols for obtaining care-of ad-
dresses. Deregistration is automatic rather than explicit. The issue of re-registration is totally
ignored.
in r 0 [msg;
in if
Ah in
in
in
Haf (a;
in
Router(r) (as in Figure 1)

Figure

2: States of the agent at home
receives an acknowledgement from the home agent (control message infmd). The
control messages (regd and infmd) are required to model the coordinated change
of state at the two sites 8 . The home agent filters messages while waiting for the
regd message; this filtration can be expressed in our asynchronous communication
model by having other messages "put back" into the message buffer, and
remaining in state Ham(a).
Haf The home agent as a forwarder. The home agent forwards messages to the
mobile agent at its current router 9 (via the routers of course), unless informed
by the mobile agent that it is moving from that router. There are two cases
we consider: either the mobile agent is coming home ("repatriation") or it is
migrating elsewhere.
States of the agent away from home We describe the agents at a foreign
router in Figure 3.
Idle If the agent has never visited. The Idle state captures the behavior of the
shadow of an agent at a router it has never visited. If the agent moves to that
8 These messages may be likened to the "binding update for home registration" and "binding
acknowledgement from home".
9 This is the primary care-of address.
in
in
in
\Phi c2fin;out;mvg;y2AN;w2DN ;u2RN
in r[msg;
in if
if u 6=
Ma in (a;
in

Figure

3: States of the agent away from home
router, indicated by the control message immig, then the shadow agent changes
state to Bma(a; r), from where it will take on the behavior of mobile agent a
at the foreign router r. Any other message is ignored, and indeed it should be
erroneous to receive any other message in this state.
Fwd If the agent is not at foreign router r, but has been there earlier. This state
is similar to Idle , except that any delayed messages that had been routed to the
agent while it was at r previously are re-routed via the home router 10 . This state
may be compared to Haf , except that it does not have to concern itself with the
agent migrating elsewhere.
Bma Becoming a foreign mobile agent. Once the protocol for establishing movement
to the current router is complete, the agent becomes a foreign mobile agent.
Messages are filtered looking for an acknowledgement from the home agent that
it is aware of the mobile agent's new current router. Once the home agent has acknowledged
that it has noted the new coordinates, the mobile agent may become
operational 11 .
Ma The mobile agent at a foreign router. As with the mobile agent at its home
base Ah(a), the mobile agent may receive messages, send messages, or move away.
The behavior of the mobile agent in state Ma is similar to that of Ah except that
during movement, different control messages need to be sent to the target site
depending on whether it is home or another site. If the target site is the home
base, then a repat message is sent. Otherwise the target site is intimated of the
wish to "immigrate". The agent goes into the state Fwd .
In the upper part of Figure 4 we describe the possible transitions that relate
to control messages, not including filtering, forwarding, and erroneous situations.
We decorate the transitions with the control messages that are received (-) and
emitted (+). In the lower part of Figure 4 we outline the three basic movements
of an agent a: leaving the home router, coming back to the home router, and
moving between routers different from the home router.
messages forwarded by the home agent may get arbitrarily delayed in transit, it is
important that the mobile agent, in addition to informing its home agent of its current router,
arrange for a forwarder at its prior router to handle such delayed messages. This point is the
only major difference between our model and the IPv6 proposal. In order not to lose messages,
we require a forwarder at any router where the mobile agent has previously visited. The default
target for forwarding is the home router. In the Mobile IPv6 proposal, however, it is not
mandatory for the mobile agent to arrange for a forwarder at the previous router, and if a
message reaches a router that had previously served as a foreign agent, the message may be
dropped. This is permissible in the context of IP since dealing with lost messages is left to the
transport and higher layers. Our analysis shows that Mobile IP can use our default policy of
forwarding to the home router, without messages traversing cycles indefinitely, but at the cost
of some increase in the number of hops for a message. The need for forwarders is, of course,
well known in the folklore regarding implementation of process migration.
In IPv6 a mobile node may begin operation even before it has registered its new location
with the home agent or received an acknowledgement from the home router. Correct updates of
the primary care-of address at the home router are achieved using time-stamping of messages,
which in turn requires synchronized clocks. In contrast, our asynchronous communication model
makes no timeliness assumptions and permits message overtaking. Hence our protocol requires
an acknowledgement from home before permitting further migrations.
(1) Ah(a) +immig
\Gamma! Ham(a) \Gammaregd +infmd
\Gamma! Haf (a; r)
\Gammaimmig +mig
\Gamma! Bma(a; r)
\Gammainfmd
\Gamma! Ma(a; r)
\Gammaimmig +regd
\Gamma! Bma(a; r)
\Gammainfmd
\Gamma! Ma(a; r)
\Gamma! Fwd(a; r)
+repat
\Gamma! Fwd(a; r)
(4:1) Haf (a; r)
\Gammamig +infmd
\Gamma! Haf (a; r 0 )
(4:2) Haf (a; r)
\Gammarepat
\Gamma! Ah(a)
I-Leaving home
Ham(a) Idle=Fwd(a; r) immig
Ham(a) Bma(a; r) regd
Haf (a; r) Bma(a; r) infmd
Haf (a; r) Ma(a; r)
II-Coming home
Ma(a; r) Haf (a; r)
Fwd(a; r) Haf (a; r) repat
Fwd(a; r) Ah(a)
III-Moving between routers different from the home router
Ma(a; r) Haf (a; r) Idle=Fwd(a; r 0 )

Figure

4: Control transitions
We briefly describe how our "static" description that requires a thread for each
agent at each router relates to a more "dynamic" model that is more natural from
a programming viewpoint. First we observe that an agent's name is obtained by
combining a router's name with a local identifying name. The computation of
function H is distributed, in that an agent's name contains sufficient information
for computing its home router's name. Further, our infinite name space of agents
is a virtual representation of a finite location name space with dynamic generation
of names at each location.
As observed earlier, the only actual processes are Ah, Ah in , Ma and Ma in ,
which run in parallel with the routers. The other "agents" are threads run on the
router. The Ham thread is spawned on the home router when Ah wishes to move
this thread becomes Haf, a thread that forwards messages to the mobile
agent and terminates when the agent returns.
Each router maintains a list of agents for whom it serves as a home router,
with their current locations as well as a list of mobile agents currently visiting.
The default policy of a router is to deliver messages to agents actually present
there, to forward messages to mobile agents for whom it serves as a home router,
and to otherwise forward the message to the target agent's home router. Messages
to a non-existent agent trigger an error.
As our analysis will show, the only message an Idle thread can receive is an
immig message. So this thread need not exist. Instead, on receiving an immig
message, the router spawns a Bma thread, updating the list of agents actually
present there. When Ma moves away from a router, it notifies the router to spawn
a Fwd thread. In practice, the Fwd thread will synchronize with the router
to empty the buffer of messages left behind by the agent and then terminate.
Following this implementation, the number of threads running at a router r is
proportional to the number of agents whose home is r or who are currently visiting
r.
3.3 The system with caching CMob
The previous system suffers from overcentralization. All traffic to an agent is
routed through its home router, thus creating inefficiencies as well as poor fault
tolerance. So, correspondent agents can cache the current router of a mobile agent
[JP96]. The agents' definitions are parametric in a function f : AN ! RN , which
represents their current cache. The cache is used to approximate knowledge of
the current location of an agent; this function parameter can be implemented by
associating a list with each agent 12 .
We now use control directives fwdd and upd; the former indicates that the
current data message has been forwarded thus pointing out a "cache miss", the
latter suggests an update of a cache entry, following a cache miss 13 . An agent may
also decide to reset a cache entry to the home router 14 . Note that the protocol does
not require the coherence of the caches. In case of cache miss, we may forward the
message either to the home router (which, as in the previous protocol, maintains
an up-to-date view of the current router) or to the router to which the agent has
moved.
We present in Figure 5, the new definitions of the agent at home. Note the use
of the directives fwdd and upd to update the cache and to suggest cache updates.
In

Figures

6,7 we present the modified definitions for the agent away from
home. We note the introduction of two extra states: Fwd in (a;
To model timing out of cached entries by a forwarder, an extra state Fwd in (a;
is introduced. Non-determinism is used in Fwd and Ma in to model possible resetting
or updating cache entries 15 . Mam(a; r) is an extra state that we need when
an agent moves from a router different from the home router. Before becoming
When moving to another router, we could deliver the current cache with the message immig.
In the presented version we always re-start with the default cache H.
13 A fwdd message can be regarded as having been tunnelled, while a upd message is a binding
update.
14 In IPv6, the validity of a cache entry may expire. In the informal description of the protocol,
the update and deletion of a cache entry are often optional operations. We model this by using
internal choice. No messages to reset a cache entry (binding deletion updates) are ever sent
out, nor are negative acknowledgements sent out. We also note that maintaining the "binding
update list" is not essential to the protocol, but is only a pragmatic design choice. Instead, an
agent may non-deterministically decide to reset a cache entry, thus abstracting from a particular
cache management mechanism.
Timing out of cache entries is modelled using non-determinism, rather than by explicit
representation of time stamps in a message. Note that in the Mobile IP protocol no hypothesis
is made regarding the coordination of the clocks of the agents, so it seems an overkill to introduce
time to speak about these time stamps.
in r 0 [msg;
in if
in Ah(a; f [r 0 =y])
Ah in (a; f; c
let r
in
let r
in
Haf (a;
let r
in
Router(r) (as in Figure 1)

Figure

5: Modified control for agent at home with caching
in
\Phi c2f0;1g
let r
in Fwd(a;
Fwd in (a;
in
in

Figure

Modified control for agent away from home with caching, part I
a forwarder to the router to which the agent moved, we have to make sure that
the agent has arrived there, otherwise we may forward messages to an Idle(a; r 0 )
process, thus producing a run-time error (this situation does not arise in system
Mob because we always forward to the home router).
4 Analysis
We now analyze the three different systems Stat, Mob, and CMob. In each case, the
first step is to provide a schematic description of the reachable configurations, and
to show that they satisfy certain desirable properties. Technically, we introduce a
notion of admissible configuration, i.e., a configuration with certain properties, and
go on to show that the initial configuration is admissible, and that admissibility
is preserved by reduction.
A crucial property of admissible configurations for Mob and CMob is control
stabilization. This means that it is always possible to bring these systems to a
situation where all migrations have been completed (we can give precise bounds
on the number of steps needed to achieve this). We call these states stable. Other
interesting properties we show relate to the integrity and delivery of messages. The
Ma(a;
in r[msg;
in if
if
in if y
Ma in (a;
in
in

Figure

7: Modified control for agent away from home with caching, part II
control stabilization property of admissible configurations is also exploited to build
(barbed) bisimulation relations, with respect to a suitable notion of observation,
between Stat and Mob, and between Stat and CMob.
4.1 Analysis of Stat

Figure

8 presents the notion of admissible configuration for Stat. We will write
s:Rt, s:Ob, s:Ag, and s:Ms to denote the state of the routers, atomic observa-
tions, agents, and data messages, respectively, in configuration s. We will abuse
notation, and regard products of messages as multisets, justified since parallel
composition is associative and commutative. When working with multisets we
will use standard set-theoretic notation, though operations such as union and
difference are intended to take multiplicity of the occurrences into account.
We assume that ]RN - 3, to avoid considering degenerate cases when es-
Ag
j A in (a);

Figure

8: Admissible configurations for Stat
tablishing the correspondence between Stat and Mob (if ]RN - 2, then the
transitions III in Figure 4 cannot arise).
Proposition 4.1 The initial configuration Stat is admissible, and admissible configurations
are closed under reduction.
By the definition of admissible configuration, we can conclude that the error
message offl is never generated (a similar remark can be made for the systems Mob
and CMob, applying theorems 4.5 and 4.13, respectively).
Messages do not get lost or tampered with.
Corollary 4.2 (message integrity) Let s be an admissible configuration for
Stat, let zx 2 s:Ms and suppose s
when the message gets received by its intended
addressee.
Corollary 4.3 (message delivery) Let s be an admissible configuration for Stat
such that zx 2 s:Ms. Then the data message can be observed in at most 4 reductions

4.2 Analysis of Mob
The table in Figure 9 lists the situations that can arise during the migration of an
agent from a router to another. k is the case number, Ag(a; k; denotes the
shadow agents of a not in a Fwd or Idle state in situation k, CMs(a; k; the
migration protocol control messages at z involving at most the sites H(a);
that situation, and R(a; k; denotes the routers involved in situation k of the
protocol at which a's shadow is not in a Fwd or Idle state.
Relying on this table, we define in Figure 10 a notion of admissible function
fl. Intuitively, the function fl associates with each agent a its current migration
control (the state and the protocol messages), the routers already visited, and the
data messages in transit that are addressed to a.
We denote with P fin (X) and M fin (X) the finite parts, and finite multisets of X,
respectively, and with fl(a) i the i-th projection of the tuple fl(a). Then Act(a; fl)
denotes the routers where a has visited, which are not in an Idle state. Condition
states that at most finitely many agents can be on the move ("deranged") at
2 Ah in (a) 0 fr 0 g
3 Ham(a) z[immig; a;
5 Haf (a; r) j Bma(a; r) z[infmd; a;
8 Haf (a; r) j Ma in (a; r) 0 fr
9 Haf (a; r) z[immig; a; r

Figure

9: Control migration (r
M fin ((RN [ LAN ) \Theta RN \Theta AN \Theta RN \Theta DN ) (data messages)
Admissibility conditions on fl:
(CMs(a; k;

Figure

10: Admissible configurations for Mob
any instant. (C 2 ) is a hygiene condition on migration control messages, indicating
that they may be at exactly one of three positions, and that if an agent is on the
move (cases 7 and 9), the home forwarder always points to an active router, where
a proxy agent will return delayed data messages back to a's home; after receiving
the pending control message, the home forwarder will deliver the data message
to the current (correct) location of the mobile agent. Thus, although there may
apparently be forwarding cycles, these will always involve the home forwarder and
will be broken immediately on receipt of the pending control message. Condition
explicitly indicates where a control message involving a may be.
Definition 4.4 (admissible configuration) An admissible configuration for Mob,
m, is generated by a pair (fl; Ob) comprising an admissible function and a process
as follows:
where Rt,Ob are as in Figure 8 and
Ag(a; k;
Let m be an admissible configuration for Mob, generated by (fl; Ob). Further,
let m:DMs(a) denote \Pi (z;r 1 ;a 2 ;r 2 ;d)2fl(a) 6
d], the data messages in
state m addressed to a, and let m:DMs denote all data messages in state m.
We will write m:CMs and m:Ob to denote the state of the control messages and
atomic observations, respectively, in configuration m.
Theorem 4.5 The initial configuration Mob is admissible, and admissible configurations
are closed under reduction.
From this result, it is possible to derive an important property of system Mob:
it is always possible to bring the system to a stable state.
Corollary 4.6 (control stabilization) Let m be an admissible configuration for
Mob generated by (fl; Ob) and let
g.
that m 0 is determined by (fl In
particular, if fl(a)
6g.
The analogies of corollaries 4.2 and 4.3 can be stated as follows.
Messages neither get lost nor is their observable content tampered with.
Corollary 4.7 (message integrity) Let m be an admissible configuration for
Mob, generated by (fl; Ob), and suppose
either or else there exists a z 0
l x 0
that obs(x 0
l
Corollary 4.8 (message delivery) Let a 2 AN and let m be an admissible
configuration for Mob generated by (fl; Ob) such that fl(a) 1 2 K s and (z; r 1 ; a
fl(a) 6 . Then this data message can be observed in at most 10 reductions.
We now introduce a notion of what is observable of a process and a related
notion of barbed bisimulation (cf. [Par81, Pnu85]).
Definition 4.9 Let p be a process. Then O(p) is the following multiset (y can
be ffl):
We note that on an admissible configuration s,
can be applied to an admissible configuration m or c (cf. following definition 4.12).
Definition 4.10 A binary relation on processes R is a barbed bisimulation if
whenever p R q then the following conditions hold:
and symmetrically. Two processes p; q are barbed bisimilar, written p ffl
they are related by a barbed bisimulation.
We use the notion of barbed bisimulation to relate the simple system Stat
(viewed as a specification) to the more complex systems Mob and CMob. Note
that each process p has a unique commitment O(p). Taking as commitments the
atomic observations would lead to a strictly weaker equivalence.
Theorem 4.11 Stat ffl
Mob.
Proofhint. We define the relevant observable content of data messages in an
admissible configuration s for Stat and m for Mob as the following multisets,
respectively:
O
O
Next, we introduce a relation S between admissible configurations for Stat and
Mob as:
We show that S is a barbed bisimulation. 2
4.3 Analysis of CMob
The analysis of CMob follows the pattern presented above for Mob. The statement
of the invariant however is considerably more complicated. The table in Figure
11 lists the situations that can arise during the migration of an agent from a
router to another. Relying on this table, we define in Figure 12 a notion of
admissible function fl. Intuitively, the function fl associates with each agent a
its current migration control (state and protocol messages), the routers already
visited (either Fwd's or Mam's), and the data messages and update messages in
transit which are addressed to a.
3 Ham(a) z[immig; a;
5 Haf (a; r) j Bma(a; r) z[infmd; a;
6 Haf (a; r) j Ma(a;
7 Haf (a; r) j Ma in (a;
9 Haf (a; r) j Mam(a; r) z[immig; a; r

Figure

11: Control migration with caching (r
Again, Act(a; fl) denotes the routers where a has visited, which are not in an
Idle state. Condition (C 1 ), as before, states that at most finitely many agents can
be on the move ("deranged") at any instant. (C 2 ) is, as before, an invariant on
control messages and the forwarder caches, indicating that there are no forwarding
cycles and the cached entries for each agent a always point to routers where
the mobile agent has visited. M serves to indicate the router at which there is a
Mam(a) when there is a pending regd message whose current location is indicated
using Z. (C 3 ) is an invariant dealing with data messages or forwarded data mes-
sages, which indicates that such messages may never arise from, be addressed to,
or be present at agents located at as yet unvisited routers. (C 4 ) is a condition on
update messages, stating that such messages are only sent between shadow agents
of two different agents, and that they may only originate, be present at and be
targetted to routers where the two agents have been active.
Definition 4.12 (admissible configuration with caching) An admissible configuration
with caching cm is generated by a pair (fl; Ob), consisting of an admissible
function with caching and a process, as follows:
where Rt and Ob are as in Figure 8, and
Ag(a; k;
(K \Theta RN \Theta RN \Theta (AN ! RN ) \Theta (RN [ LAN ) \Theta f0; 1g 2 (control migration)
(RN * (RN \Theta fin; ning))\Theta
(RN * (RN \Theta (RN [ LAN )))\Theta (Mam's)
M fin (fmsg; fwddg \Theta (RN [ LAN ) \Theta RN \Theta AN \Theta RN \Theta DN )\Theta (data messages)
Admissibility conditions on fl:
(CMs(a; k;
dom(F
Acyclic(F; M); and
defined
where Acyclic(F; M) means:

Figure

12: Admissible configurations with caching
Let c be an admissible configuration with caching, generated by (fl; Ob). Fur-
ther, let c:DMs(a) denote \Pi (ddir ;z;r 1 ;a 2 ;r
d], the data messages
addressed to a in configuration c, and let c:DMs stand for all data messages
in configuration c. For convenience, we will write c:CMs and c:Ob to denote the
state of the control messages and atomic observations, respectively, in configuration
c.
Theorem 4.13 The initial configuration CMob is admissible, and admissible configurations
with caching are closed under reduction.
As in Mob, it is possible to bring CMob to a stable state.
Corollary 4.14 (control stabilization) Let c be an admissible configuration
with caching generated by (fl; Ob) and let
g. Then c ! -(10\Lambdan) c 0
such that c 0 is generated by (fl
In particular, if fl(a)
6g.
As in Stat and Mob, it is easy to derive corollaries concerning message integrity
and message delivery.
Corollary 4.15 (message integrity) Messages do not get lost nor is their observable
content tampered with. Let c be an admissible configuration with caching,
generated by (fl; Ob), and suppose c ! c 0 . Then for all z
or else there exists a z 0
l x 0
l 2 c 0 :DMs such that
l
Corollary 4.16 (message delivery) Let a 2 AN and let c be an admissible
configuration with caching generated by (fl; Ob) such that (ddir ; z; r 1 ; a
Then the data message can be "delivered" in a number of
reductions proportional to the length of the longest forwarding chain.
The analysis of the invariant allows us to extract some general principles for
the correct definition of the protocol (note that these principles are an output of
the analysis of our protocol model, they are not explicitly stated in the informal
description of the protocol).
ffl Cache entries and Fwd 's always point to routers which have been visited by
the agent.
Any message from agent a to agent a 0 comes from a router r and is directed to
a router r 0 , which have been visited, respectively, by agent a and a 0 .
ffl Agent a never sends update messages to its own shadow agents.
ffl The protocol for moving an agent a from a router to another terminates in a
fixed number steps.
ffl Given an agent a, the forwarding proxy agents never form forwarding cycles.
This ensures that once the agent a has settled in one router, data messages and
update messages in transit can reach it in a number of steps which is proportional
to the length of the longest chain of Fwd 's.
The bottom line of our analysis for system CMob is the analogue of theorem 4.11.
Theorem 4.17 Stat ffl
Conclusions
We have described in a standard process description language a simplified version
of the Mobile IP protocol. We believe that a precise yet abstract model is useful in
establishing the correctness of the protocol, as well as providing a basis for simulation
and experimentation. Our modelling uses non-determinism and asynchronous
communication (with unbounded and unordered buffers). Non-determinism serves
as a powerful abstraction mechanism, assuring us of the correctness of the protocol
for arbitrary behaviors of the processes, even if we try different instances
of particular management policies (e.g., routing and cache management policies)
provided they maintain the same invariants as in the non-deterministic model.
Asynchronous communication makes minimal assumptions on the properties of
the communication channels and timeliness of messages. All we require is that
messages are not lost and in particular we assume there is a mechanism for avoiding
store-and-forward deadlocks. Our analysis shows that message loss can be
avoided by a router forwarding messages addressed to a mobile agent that is no
longer present in that subnet to its home router or to a router to which it has
moved. Moreover, these forwarding links never form cycles. Control Stabilization
is a key property, since cycles that a message may potentially traverse are broken
on stabilization. Furthermore, any (reasonable) cache update policy can be used
provided messages to an agent are forwarded to routers it has previously visited.
Our model allows mobility protocol designers explore alternative policies and
mechanisms for message forwarding and cache management. A concrete suggestion
is that rather than dropping a data message (delayed in transit) for an agent
that has moved away from a router, IPv6 designers could examine the tradeoff between
increased traffic and employing a default policy of tunneling the message to
the home subnet of the agent - particularly for applications where message loss
is costly, or in the context of multi-layer protocols. Other concrete applications
include designing mobility protocols where losing messages may be unacceptable,
e.g., forwarding signals in process migration mechanisms.
In our modelling, we have greatly simplified various details. On the one hand,
this simplification is useful, since it again serves as a way of abstracting from particular
protocols for establishing connections (e.g., Neighbor Discovery, etc. On
the other hand, we have assumed that our so-called "control messages" eventually
reach their destination without getting lost or corrupted. A future direction of
work may be to model protocols that cope with failures, or to model security and
authentication issues.
By concentrating on an abstract and simple model we have been able to specify
the protocol and by a process of analysis to discover and explicate some of its
organizing principles. The specification and combinatorial analysis of the protocol
is sufficiently complicated to preclude leaving it "implicit" in the informal protocol
description. By a careful analysis we have been able to carry out a hand proof. A
direction for further research is the formal development of the proof using a proof
assistant.
Finally, we report on a finite state formulation of the protocol for which automatic
simulation and verification tools are available. The sets RN ; AN ; DN are
assumed finite, so that there are finitely many entities in the systems. Ensuring
that the number of messages does not grow in an unbounded manner also requires
that communication is over bounded capacity channels. In particular we will consider
the limit case where all communications are synchronous (we expect that a
protocol which works with synchronous communication can be easily adapted to
a situation where additional buffers are added).
The main difficulty lies in understanding how to transform asynchronous communication
into synchronous communication without introducing deadlocks. The
synchronous version seems to require a finer, more detailed description of the
protocol and makes the proof of correctness much more complicated. In retro-
spect, this fact justifies the use of an asynchronous communication model with
unbounded and unordered buffers. The systems FStat and FMob with synchronous
communication are described in Appendix B. We have compiled these descriptions
in the modelling language Promela of the simulation and verification tool SPIN
[Hol91]. Extensive simulations on configurations including three routers and three
agents have revealed no errors. We have been able to complete a verification for
the FStat system with two routers and two agents. The size of the verification
task and the complexity of the system FMob make verification of larger systems
difficult. The Promela sources for FMob are available at URL http://protis.univ-
mrs.fr/-amadio/fmob.



--R

A foundation for actor computation.
Orca: a language for parallel programming of distributed systems.
Design of a distributed object manager for Smalltalk-80 system
Design and validation of computer protocols.
An object calculus for asynchronous communication.


A nitpick analysis of mobile IPv6.
Mobility support in IPv6 (RFC).
A Calculus of Mobile Process
Mobile Unity coordination constructs applied to packet forwarding.
The sprite network operating system.
Concurrency and automata on infinite sequences.
Indirect distributed garbage collection: handling object migration.
Process migration in demos/mp.
Linear and branching systems in the semantics and logics of reactive systems.
Expressing code mobility in mobile UNITY.
The Locus Distributed System Architecture.
Mobile UNITY: reasoning and specificaton in mobile computing.
Vip: a protocol providing host mobility.
Mobile objects in distributed Oz.
--TR
The LOCUS distributed system architecture
Design of a distributed object manager for the Smalltalk-80 system
Fine-grained mobility in the Emerald system
The Sprite Network Operating System
Design and validation of computer protocols
IP-based protocols for mobile internetworking
Orca
A calculus of mobile processes, I
VIP: a protocol providing host mobility
Indirect distributed garbage collection
Mobile UNITY
Mobile objects in distributed Oz
Expressing code mobility in mobile UNITY
An Object Calculus for Asynchronous Communication
Linear and Branching Structures in the Semantics and Logics of Reactive Systems
Modelling IP Mobility
Mobile UNITY Coordination Constructs Applied to Packet Forwarding for Mobile Hosts
Concurrency and Automata on Infinite Sequences
Process migration in DEMOS/MP
A foundation for actor computation
internet protocols;formal methods;mobility;bisimulation;modelling;process description languages;protocol analysis;verification