Recovery from DoS Attacks in MIPv6: Modelling and Validation

Denial-of-service (DoS) attacks form a very important category of security threats that are prevalent in MIPv6 (mobile internet protocol version 6) today. Many schemes have been proposed to alleviate such threats, including one of our own [9]. However, reasoning about the correctness of such protocols is not trivial. In addition, new solutions to mitigate attacks may need to be deployed in the network on a frequent basis as and when attacks are detected, as it is practically impossible to anticipate all attacks and provide solutions in advance. This makes it necessary to validate the solutions in a timely manner before deployment in the real network. However, threshold schemes needed in group protocols make analysis complex. Model checking threshold-based group protocols that employ cryptography have not been successful so far. Here, we propose a new simulation based approach for validation using a tool called FRAMOGR that supports executable specification of group protocols that use cryptography. FRAMOGR allows one to specify attackers and track probability distributions of values or paths. We believe that infrastructure such as FRAMOGR would be required in future for validating new group based threshold protocols that may be needed for making MIPv6 more robust.

Computing complete test graphs for hierarchical systems

Conformance testing focuses on checking whether an implementation. under test (IUT) behaves according to its specification. Typically, testers are interested it? performing targeted tests that exercise certain features of the IUT This intention is formalized as a test purpose. The tester needs a "strategy" to reach the goal specified by the test purpose. Also, for a particular test case, the strategy should tell the tester whether the IUT has passed, failed. or deviated front the test purpose. In [8] Jeron and Morel show how to compute, for a given finite state machine specification and a test purpose automaton, a complete test graph (CTG) which represents all test strategies. In this paper; we consider the case when the specification is a hierarchical state machine and show how to compute a hierarchical CTG which preserves the hierarchical structure of the specification. We also propose an algorithm for an online test oracle which avoids a space overhead associated with the CTG.

Extended colored Petri net: An efficient tool for analyzing concurrent systems

This paper proposes a novel and simple definition of general colored Petri nets. This definition is coherent with that of (uncolored) Petri nets, preserves the reflexivity of the original net and is extended to represent inhibitors. Also suggested are systematic and formal merging rules to obtain a well-formed structure of the extended colored Petri net by folding a given uncolored net. Finally, we present a technique to compute colored invariants by selecting colored RP-subnets. On the average, the proposed technique performs better than the existing ones. The analysis procedure is explained through an illustrative example of a three-level interrupt-priority-handler scheme.

Electronic structure of early 3d-transition-metal oxides by analysis of the 2p core-level photoemission spectra

The electronic structures of a wide range of early transition-metal (TM) compounds, including Ti and V oxides with metal valences ranging from 2+ to 5+ and formal d-electron numbers ranging from 0 to 2, have been investigated by a configuration-interaction cluster model analysis of the core-level metal 2p x-ray photoemission spectra (XPS). Inelastic energy-loss backgrounds calculated from experimentally measured electron-energy-loss spectra (EELS) were subtracted from the XPS spectra to remove extrinsic loss features. Parameter values deduced for the charge-transfer energy Delta and the d-d Coulomb repulsion energy U are shown to continue the systematic trends established previously for the late TM compounds, giving support to a charge-transfer mechanism for the satellite structures. The early TM compounds are characterized by a large metal d-ligand p hybridization energy, resulting in strong covalency in these compounds. Values for Delta and U suggest that many early TM compounds should be reclassified as intermediate between the charge-transfer regime and the Mott-Hubbard regime.

Heterogeneous locational optimisation using a generalised Voronoi partition

In this paper a generalisation of the Voronoi partition is used for locational optimisation of facilities having different service capabilities and limited range or reach. The facilities can be stationary, such as base stations in a cellular network, hospitals, schools, etc., or mobile units, such as multiple unmanned aerial vehicles, automated guided vehicles, etc., carrying sensors, or mobile units carrying relief personnel and materials. An objective function for optimal deployment of the facilities is formulated, and its critical points are determined. The locally optimal deployment is shown to be a generalised centroidal Voronoi configuration in which the facilities are located at the centroids of the corresponding generalised Voronoi cells. The problem is formulated for more general mobile facilities, and formal results on the stability, convergence and spatial distribution of the proposed control laws responsible for the motion of the agents carrying facilities, under some constraints on the agents' speed and limit on the sensor range, are provided. The theoretical results are supported with illustrative simulation results.