Oussama NAHNAH

Internet of things connect unlimited number of heterogeneous devices in order to facilitate services and hence touching most of daily life fields. However, security concerns are a major obstacle to the development and rapid deployment of this high technology. Thus, securing the authentication process has become very important, as it is necessary to prove the legitimacy of the communication devices. Recently, researchers are proposing several mutual authentication and session key agreement protocols. In this regard, we propose our own improved protocol that relies on login, mutual authentication and the agreement of session key in a safety way to secure communications. For the security evaluation of the proposal, we use the authentication BAN logic and the widely used AVISPA tool. The results prove the achievement of mutual authentication and session key agreement securely, in addition to its safety against some known attacks as eavesdropping and replay attacks. For a performance evaluation, we compare the proposal with recent related works in terms of computational and communication costs. The results show the lightness of our protocol and thus its suitability to heterogeneous IoT devices.

Designing distributed algorithms for a swarm of robots and proving their soundness is a complex, highly combinatorial, and error-prone task. While some attempts at automation have been made, they have remained limited. We propose a partly automated method to synthesize algorithms that solve the perpetual exploration of a finite grid containing an obstacle using luminous myopic robots, with common chirality, in the fully synchronous Look-Compute-Move model. This generic method is supported by a proof-of-concept tool that generates algorithms and verifies them by simulation on small grids. The results of the simulation are generalized to larger grids with a pen-and-paper proof.

Concevoir des algorithmes distribués pour essaims de robots et prouver leur validité est une tâche complexe, fortement combinatoire et sujette aux erreurs. Les tentatives d'automatisation sont restées limitées. Nous proposons une méthode partiellement automatisée pour synthétiser des algorithmes d'exploration perpétuelle d'une grille finie avec obstacle pour des robots lumineux myopes avec chiralité. Cette approche est illustrée par un outil de génération d'algorithmes et de validation par simulation sur des petites grilles. Les résultats sont généralisés à de plus grandes grilles par preuve.