arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Mathilde Arnaud

9 papers · 2010–2026

2010: 22011: 22012: 02013: 02014: 02015: 02016: 12017: 02018: 02019: 02020: 02021: 12022: 12023: 12024: 02025: 02026: 1
2010peak 2 in 20102026

Frequent co-authors

Papers

showing 1–9 of 9 RSS

Modeling and Verifying Ad Hoc Routing Protocols

Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune

Computer Networks and Communications · · cited 20× · DOI ↗ · more like this ·

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route. Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in NPTIME) whether…

An Illustrative Use Case of the DIVERSITY Platform based on UML Interaction Scenarios

Mathilde Arnaud, Boutheina Bannour, Arnault Lapitre

Software · Electronic Notes in Theoretical Computer Science · · cited 10× · DOI ↗ · more like this ·

DIVERSITY is a multi-purpose customizable platform based on symbolic execution. DIVERSITY has been designed for the purpose of managing the diversity of different semantics, but also the diversity of possible analyses based on symbolic execution. In this paper, we show how the input language of DIVERSITY can be used to encode the semantics of UML scenarios which include timing constraints expressed with the VSL language (standardized in the UML profile for embedded systems MARTE). We apply symbolic execution on practical scenarios of a system-on-chip example 3 in order to select test behaviors using an advanced exploration strategy implemented in DIVERSITY.

A New Generic Representation for Modeling Privacy

Myriam Clouet, Thibaud Antignac, Mathilde Arnaud +2 more

Sociology and Political Science · HAL (Le Centre pour la Communication Scientifique Directe) · · cited 2× · DOI ↗ · more like this ·

Verifying how personal data is used in industrial applications is of utmost importance for evaluating privacy. Existing works propose many definitions of privacy and offer a wide variety of approaches for verifying privacy properties. Yet, as far as we know, there is currently no generic setting allowing to model all these concepts, as well as to express and verify related privacy properties, whilst taking into account the various abstraction levels involved when designing and implementing a computer system. This work proposes a generic representation for modeling privacy relying on a new classification scheme and a new ontology. These aim to be generic enough for modeling key privacy concepts and their relationships, as well as helping express and verify related properties at different levels of abstractions. Our representation of privacy can also be specialized into various existing…

Investigating Process Algebra Models to Represent Structured Requirements for Time-sensitive CPS

Mathilde Arnaud

Computational Theory and Mathematics · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · · cited 2× · DOI ↗ · more like this ·

Cyber-Physical Systems (CPS) contain complex computational components that control physical entities. The design of these components must take into account the realtime and concurrent nature of these systems. Formulating requirements that describe CPS behaviors precisely, ruling out misunderstandings, is a crucial yet difficult endeavor. To increase trust in the requirements, formal methods can be used to check relevant properties of the requirements. We investigate a process algebra to capture real-time behaviors and concurrency in CPS requirements in order to automate their analysis. We use a structured natural language to first express CPS requirements: this takes into account current practice, indeed requirements should be easily writable as well as graspable by stakeholders with various points of view and ease communication among them. At the same time, requirements analysis using…

Modelling and simulating new power grid control architectures

Mathilde Arnaud, Arnault Lapitre, Yves Lhuillier +4 more

Computer Networks and Communications · HAL (Le Centre pour la Communication Scientifique Directe) · · cited 1× · DOI ↗ · more like this ·

With the growing number of distributed energy resources, electricity grids have a stronger need for resilience that can be met by automation. Various architectures for such automated mechanisms are possible and they need to be systematically evaluated. The NACRE platform presented here allows to model and simulate various control architectures and to evaluate their behaviors against different types of communication hazards. The first version of the platform is evaluated on a use case.

Formal verification of secured routing protocols

Mathilde Arnaud

Computer Networks and Communications · HAL (Le Centre pour la Communication Scientifique Directe) · · cited 1× · OpenAlex ↗ · more like this ·

Le développement des réseaux de communication digitaux tel Internet a rendu omniprésents les protocoles de communication. Les différents appareils électroniques que nous utilisons au quotidien doivent interagir les uns avec les autres afin de réaliser les taches nombreuses et variées qui sont devenues courantes, comme d'utiliser d'un téléphone portable, envoyer ou recevoir des messages électroniques, faire des achats en ligne et ainsi de suite. Pour ces applications, la sécurité est une notion cruciale. Par exemple, dans le cas des achats en ligne, il faut que la transaction ait lieu sans divulguer les informations personnelles de l'acheteur à un tiers. Les protocoles de communications contiennent les règles qui régissent ces interactions. Afin de s'assurer qu'ils garantissent un certain niveau de sécurité, on souhaite pouvoir les analyser. Une analyse manuelle, ou leur faire subir des…

Deciding security for protocols with recursive tests. Research Report LSV-11-05, Laboratoire Specification et Verification

Mathilde Arnaud

Computer Networks and Communications · · cited 0× · OpenAlex ↗ · more like this ·

Abstract. Security protocols aim at securing communications over pub-lic networks. Their design is notoriously difficult and error-prone. Formal methods have shown their usefulness for providing a careful security anal-ysis in the case of standard authentication and confidentiality protocols. However, most current techniques do not apply to protocols that per-form recursive computation e.g. on a list of messages received from the network. While considering general recursive input/output actions very quickly yields undecidability, we focus on protocols that perform recursive tests on received messages but output messages that depend on the inputs in a standard way. This is in particular the case of secured routing proto-cols, distributed right delegation or PKI certification paths. We provide NPTIME decision procedures for protocols with recursive tests and for a bounded number of…

February 2010Modeling and Verifying Ad Hoc Routing Protocols ∗

Stéphanie Delaune, Mathilde Arnaud, Véronique Cortier +1 more

Computer Networks and Communications · · cited 0× · OpenAlex ↗ · more like this ·

Mobile ad hoc networks consist of mobile wireless devices which autonomously organize their infrastructure. In such networks, a central issue, ensured by routing protocols, is to find a route from one device to another. Those protocols use cryptographic mechanisms in order to prevent malicious nodes from compromising the discovered route. Our contribution is twofold. We first propose a calculus for modeling and reasoning about security protocols, including in particular secured routing protocols. Our calculus extends standard symbolic models to take into account the characteristics of routing protocols and to model wireless communication in a more accurate way. Our second main contribution is a decision procedure for analyzing routing protocols for any network topology. By using constraint solving techniques, we show that it is possible to automatically discover (in NPTIME) whether…

One-dimensional self-organization of water molecules in proton conducting Andersson-Wadsley titanates

Mathilde Arnaud, Guillaume Benas, Narimane Meziani +13 more

cond-mat.mtrl-sci · · arXiv ↗ · more like this ·

Layered alkali titanates with M 2 Ti 2 O 5 chemical formula (MTO, M=K,Rb) belonging to the Andersson-Wadsley perovskite family spontaneously incorporate water to form MTO.(H 2 O) x compounds, which exhibit superionic conductivity. At very low hydration x, scanning electron microscopy evidences one-dimensional heterogeneous patterns oriented along ___ b that are arranged in an orderly manner. At higher hydration, the material is observed to spontaneously exfoliate by creating (001) surfaces. Simulations carried out using Density Functional Theory reveal an ordered arrangement of the guest water molecules in Rb 2 Ti 2 O 5 , with strong hydrogen bonds between the water molecules and the apical oxygen of the host crystal. At low hydration x, the water molecules form self-organized one dimensional (1D) double chains along ___ b. Further increase of the water content leads to the creation of…