Search

Cooperative Intelligent Transport Systems (C-ITS) are becoming indispensable in improving road safety and traffic management. ITS-G5 is the European standard for vehicle to everything (V2X) communications. With advanced V2X applications and use cases, the need for enhanced communication performance and broader perception of the road becomes crucial, particularly in congested areas, where the communication performance decreases significantly. Network slicing is a new network paradigm for next-generation networks. It has proved useful to guarantee the quality-of-service requirements of various applications. This paper presents an end-to-end network slicing for the ITS-G5 vehicular communications where slices' resources are orchestrated on all the ITS infrastructure, including the ITS-G5 radio access network. The proposed slicing mechanism aims to provide enhanced end-to-end (E2E) latency for specific traffic types and user groups. We demonstrate the slicing mechanism's effectiveness on two different priority groups carried in two different slices (i.e., lower-priority slice and higher-priority slice). Simulation results show a significant improvement of the E2E latency for users of the higher-priority slice.

Cooperative Intelligent Transport Systems (C-ITS) are built based on vehicular communication technologies with real-time information exchange to improve overall traffic management such as road safety, efficiency, and comfort. Road safety depends on several factors that should be considered, among which the reliability of the used in-vehicle awareness systems. Therefore, communication technologies are rapidly evolving, and New Radio Access Technologies (RATs) are emerging to provide enhanced performances in terms of reliability, coverage, and throughput. C-ITS can benefit from these new RATs enhancements to allow new use cases and applications and then prevent additional road accidents. In this context, the IEEE 802.11bd and cellular vehicle-to-everything (C-V2X) technologies such as LTE-V2X and NR V2X are being developed. This advance is fundamentally reshaping the C-ITS landscape as both technologies (IEEE 802.11bd and LTE-V2X) are competing. In this paper, we analyze how these technologies help increase road safety by making communication more reliable. Furthermore, we will compare their performance using our IEEE 802.11bd implementation in OMNeT++ in terms of packet reception ratio. Finally, we will forecast the number of avoided serious injuries on the European roads.

Cut-in into vehicle platoons is a dangerous driving maneuver that affects the safety and efficiency of platooning vehicles. An accurate prediction of such maneuver enables the platooning system to take safety measures that ensure the platoon safety and integrity. The contribution of this paper consists of an evaluation of a set of supervised machine learning algorithms for cut-in maneuver recognition, for eventual use in platooning systems. The models were trained and tested on a large-scale publicly available driving dataset, from which cut-in events were extracted. The results show that tree-based classifiers such as Gradient Booting Machine can recognize the cut-in maneuvers with an Fl-score of 98%. An experiment to investigate the model performance with advanced prediction times shows that up to 80.5% of the cut-ins were correctly predicted 1 second before the lane crossing time.

As Internet of Things (IoT) is widely spread and is becoming heterogeneous, a growing number of connected devices are the focus of security threats. Hence, a standardized security strategy seems required. OneM2M [1] is a global standard initiative designed to satisfy the need for a common horizontal platform for the multi-industry M2M/IoT applications. In this paper, we propose an Intrusion Detection and Prevention System (IDPS), for the Service Layer introduced by the oneM2M standard. To our knowledge, it is the first generic IDPS for the oneM2M Service Layer based on Edge Machine Leaning (ML). We will detail, in this work, the strategy of the oneM2M-IDPS. Moreover, we investigate the performance of ML algorithms on the oneM2M generated dataset to choose the best ones for our IDPS. Since we are in the context of tiny devices (IoT), we pay attention in our experiments to the features dimension reduction in ML and thus, to the size of trained models.

Broadcasting official and emergency information is seen as a principle role for controlling crisis situations. In fact, it has a great importance to ensure the communication between network nodes (vehicles, passengers, etc.). This paper presents a survey that examines the existing studies of broadcasting protocols. Our survey follows the guidelines of systematic literature reviews (SLR). It provides a comparison of the existing approaches based on some criteria such as communication technologies and simulation tools. Finally, we highlight some recommendations and possible future researches which need further investigations.

Vehicular ad-hoc networks (VANETs) technology has become an active research area over the last few years. It has a huge potential to improve traffic efficiency, road safety as well as comfort to both passengers and drivers. In this context, one of the most difficult challenges is to ensure that protocols used in VANETs operate properly as expected and do not cause any inconsistencies. In this paper, we follow the guidelines of systematic literature reviews (SLR) to provide a comparison of the existing approaches formally verifying the correctness of VANETs. We introduce a taxonomy of the proposed solutions and we discuss their goals, limits, verification techniques, etc. We conclude the paper with some research challenges of VANETs that still need to be addressed. So, throughout this present paper, we provide information for researchers and developers to understand the contributions and challenges of the existing studies to pave the way for improving their solution.

Internet of Vehicles (IoV) constitutes an important part of the Smart Cities concept, relying on different technologies and including heterogeneous cars types, which raises challenges to ensure and preserve road safety. Throughout this paper, we tackled the data collection and transmission problems related to the safety in the terrestrial domain by identifying the car-types and exposing the different communication data levels and means used in the quest of safety realization.

Wireless Sensor Networks (WSNs) are widely used in critical applications (health-care, transport, volcanic eruption monitoring, etc.). Any design error in WSN algorithms can be harmful for the human's life. Therefore, we should be sure that WSN algorithms work correctly from the very first design stages. In this paper, we propose a new approach combining local computations models and refinement to prove correctness of distributed algorithms for WSNs. We use the formal method Event-B to apply refinement. In fact, local computations models provide abstract description of computations which can be easily specified with Event-B. We illustrate our approach by an example of distributed algorithm for WSN.

Android has deprecated the use of readable/writeable mode for shared preferences from API level 17. Hence, the researchers are not paying much attention towards the privacy leak via shared preferences. However, Android app developers are still using these modes in practice. This may have serious ramifications such as privacy leakage, privilege escalation, etc, and may pose a severe threat to an user’s privacy. In this paper, we present an automaton based static analysis technique named SniffDroid to detect the inter-app privacy leaks via shared preferences in Android. To evaluate the performance of SniffDroid in real-time, we tested it on our developed dataset of 21 apps and 240 Google playstore apps. These apps are chosen from various categories such as banking, wallet, location, shopping, etc. SniffDroid conducts analysis at the component level. The empirical results of the proposed method indicate that SniffDroid operates in linear time w.r.t. the number of components. It works efficiently on apps of all sizes and is scalable.

In wireless sensor networks, Intrusion Detection through sensor monitoring allows locating intricate security attacks like denial of service and routing attacks. Nevertheless, the monitoring process observing sensors behavior can induce an important energy and bandwidth overhead. Furthermore, the monitors can be attacked and their observations would be corrupted. In this paper, we propose an adaptable monitoring system that optimizes sensor resources and resists monitor security attacks. The idea is to select periodically monitors with high reputation and high resilient energy. A theoretical evaluation and simulation results demonstrates the promising efficiency of the proposed approach

Dynamic networks are characterized by frequent topology changes due to the unpredictable appearance and disappearance of mobile devices and/or communication links. In this paper, we propose a correct-by-construction approach for proving distributed algorithms in a forest of spanning trees. Our approach consists in two phases. The first one aims to control the dynamic structure of the network by triggering a maintenance operation when the forest is altered. To do so, we develop a formal pattern using the Event-B method which is based on an existing model for building and maintaining a spanning forest in dynamic networks. The second phase of our approach deals with distributed algorithms which can be applied to spanning trees. We illustrate our pattern through an example of a leader election algorithm. The proof statistics show that our solution can save efforts on specifying as well as proving the correctness of distributed algorithms in a forest of spanning trees.

Broadcast authentication has been widely investigated in the context of wireless sensor networks, Internet, RFIDs, and other scenarios. With the emergence of the Internet of Things that allows to connect different wireless technologies to provide services, broadcast authentication is crucial. Broadcast authentication aims to confirm that the sender of the message is the pretended source. In this direction, different state of the art proposals address this problem either by reducing the communication and overhead burden of security solutions, or by reducing the impact of attacks that aim to jeopordize the effectiveness of the service. In this paper, we propose an improved authentication scheme that is efficient for resource constrained devices. In particular, we shed the light into the security vulnerabilities of lightweight authentication mechanisms and their inability to tackle memory DoS attacks. Hence, we propose an improved scheme derived from the streamlined μTESLA, referred to as X-μTESLA. We demonstrate through our analytical and simulation results that X-μTESLA reduces communication overhead and yields a better performance in terms of energy consumption, memory overhead, and authentication delay than its previous counterparts.

The wide proliferation of wireless sensor networks in various domains has lead to the emergence of numerous applications with different requirements to satisfy for the well functioning. It is imperative to develop different approaches and communication protocols to meet these diverse and specific requirements while considering the most critical constraint, network lifetime. Adopting duty cycling is an efficient way to conserve energy, by allowing nodes to turn off their radio whenever possible. With these intermittent sleeping periods, it is hard to meet short delay delivery for real time traffic in duty cycled networks, since involved nodes in forwarding are not always awake. For delay intolerant applications, providing an always-on path without scarifying energy can be an effective solution. In this context, we propose a node-disjoint multipath routing algorithm, operating under duty cycled environment, to construct n complementary paths from the source towards the sink. To support urgent data transfer from sources of critical traffic, our protocol aims to offer always at least one available path while others are down. Simulation results show good performances in term of energy consumption and the number of exchanged packets control with a relative small increase in paths establishment time.

Proving the correctness of distributed algorithms in dynamic networks is a hard task due to the time complexity and the highly dynamic behavior. In the literature, the existing solutions lack a consensus about their developments and their proofs. Moreover, the proofs which have been presented are done manually. In this paper, we propose a reuse based approach for specifying and proving distributed algorithms in dynamic networks. It consists in developing a formal pattern using Event-B method, based on refinement techniques. The proposed pattern allows to handle topological events in dynamic networks and to characterize the concept of time. Our solution relies on evolving graphs as a powerful model to record the evolution of a network topology. To illustrate it, we present an example of a distributed counting algorithm. The proof statistics related to the development of the pattern and the algorithm show the efficiency of our solution.

Context-awareness has gained an increasing popularity in ubiquitous computing environments as it allows automatic adaptation of protocols behavior according to context changes. Nowadays, wireless sensor networks (WSNs), deployed as a main appliance to gather contextual information, can benefit from their own context data. In such scarce resource networks, the concept of context-awareness can be exploited either to optimize resource usage or to enhance the functional behavior of operating protocols. In this paper, we investigate the benefits brought by the concept of context-awareness when exploited in duty-cycled networks, since WSNs rely mainly on power saving mode in order to prolong the lifetime of sensor nodes. We focus mainly on the broadcast operation required for data collection and routing task. To quantify these improvements, we propose a comparative study relying on our ECAB protocol, using context-awareness jointly with a duty cycle mechanism to assure an efficient multi-hop broadcasting. To this end, we compare ECAB against protocols operating without context-awareness. Results show the effectiveness of this concept to improve network performances related to energy consumption, latency and packet delivery.

In Wireless Ad Hoc Networks, synchronization is a prerequisite to many basic operations such as frequency hopping, power saving, free contention channel access, clustering and security. Clock synchronization requires the availability of a common time reference for all mobile nodes. However, a synchronization algorithm cannot converge quickly to a stable point without considering the effects of collisions and channel interference inherent to wireless environments. In this paper, we propose a Fast Synchronization Protocol with Collision Handling for multi hop wireless ad hoc networks. Performance evaluation results show the ability of our algorithm to improve the convergence time and to assure the network wide synchronization accuracy even in highly dynamic scenarios.

The continued evolution of dynamic distributedsystems keeps the distributed computing an open area ofresearch. To make designing distributed algorithms easier, wemodel these latter with a local computation model. Attractedby the success of mobile agent paradigm in several domains, we are interested to proving benefits in the dynamic distributedsystems. We present in this paper a distributed algorithmthat computes and maintains a hierarchical spanning tree indynamic networks based on mobile agent. The mobile agent hasa responsibility of both computing and maintaining spanningtrees. The variant of the algorithm shown in this paper proposes a solution when channels appears and disappears inthe underling network.

Distributed algorithms are designed to run on interconnected autonomous computing entities for achieving a common task: each entity executes asynchronously the same code and interacts locally with its immediate neighbours. It is widely agreed that the lack of knowledge of the global state makes termination detection one of the most important and complex problems in distributed computing. By relying on refinement, we prove that an algorithm computing a spanning tree with Local Termination Detection (each entity is able to determine only its own termination condition), can be reused and adapted in order to compute the same algorithm with Global Termination Detection (at least one entity is aware that the entire computation is achieved in the network). The main idea relies upon specifying a combination of a well known algorithm namely SSP and the spanning tree algorithm, following a top/down approach. This paper is a starting point towards a general framework for enhancing termination detection property of distributed algorithms and reusing their proofs.

One of the most important issues in dynamic networks is to prove the correctness of distributed algorithms. This issue has been widely studied in the literature. Nevertheless, we note a lack of consensus about the development and proof of these algorithms. Moreover, the proofs which have been presented are usually done manually. In this paper, we introduce a formal pattern based on evolving graphs which allows to record the dynamic behavior of a network topology. To specify the proposed pattern, we use the Event-B formal method which supports a refinement-based incremental development using RODIN platform.

The Internet of Things (IoT) is formed by smart objects and services to interact in real time, and that are deployed in various applications such as home monitoring, healthcare, and smart cities. However, security concerns should not be overlooked since an adversary could exploit the vulnerabilities in the design of some secure protocols. To this aim, in this paper we focus in particular on broadcast authentication in resource constrained devices. This security service is still in its infancy when devices are deployed in unattended environments. We propose a new authentication mechanism based on the state of the art protocol μTESLA, that aims to reduce the delay of forged packets in the receivers buffer, by efficiently computing the key disclosure delay. Then, we integrate this mechanism to two protocols of state of the art LEAP and LEAP++. Furthermore, we assess the feasibility of our solution with a thorough simulation study, taking into account the energy consumption, the delay of forged packets, and the authentication delay.

Duty-cycling scheme consists in switching between active and sleeping modes. While this technique is widely exploited in WSNs to reduce power consumption, It raises several challenges especially for broadcast communications. In fact, as many neighboring nodes are involved in the communication, keeping them all active during a specific period of time requires a preliminary synchronization process which is a complex task and causes extra overhead. In this context, we propose an Efficient Context-Aware multi-hop Broadcasting (ECAB) over asynchronous duty cycled networks. ECAB exploits both the neighborhood knowledge and the traffic load conditions to regulate node behaviors and dynamically adjust duty-cycling schedules. Our objective is to reduce energy consumption without performances penalties. Simulation results show that ECAB outperforms RI-MAC and greatly improves energy consumption compared to broadcast under always-on networks with small degradation related to end-to-end delay and packet delivery.

Broadcast authentication is crucial for civil and military applications related to the Internet of things such as wide-area protection, and target tracking. Authentication in these scenarios is time sensitive, and needs to take into account the characteristics of the deployed devices. Even various smart communication protocols in the literature address the problem of broadcast authentication, however there is still a lack on providing practical and secure authentication solutions. In this paper, we point out the security concerns of current state of the art protocol LEAP. In particular, we address the vulnerability of LEAP to a severe denial of service attack. We propose a new authentication process in μTESLA mechanism that defeats the drawback of LEAP protocol in terms of authentication delay, and resilience to DoS attack, by managing with a simple and effective way to reduce the delay of forged packets in the receivers buffer. Furthermore, we assess the feasibility of our solution with a thorough simulation study, taking into account the authentication delay, the energy consumption and the delay of forged packets.

Simulation tools are useful for detailed analysis of distributed systems that are increasingly present in our daily lives. ViSiDiA (Visualization and Simulation of Distributed Algorithms) is a platform that aims both to facilitate teaching distributed algorithms and to contribute to the research activities. This paper presents design features and examples of how to implement new ViSiDiA's algorithms. These implementations can be done using the Java language or by using the ViSiDiA's GUI (just drawing the relabelling rules that correspond to considered algorithm). We also present a more complex problem for which ViSiDiA served as a simulation and analysis tool.

Due to the lack of knowledge of the global state and the non determinism in the execution of the processes, distributed algorithms are considered to be very complex to design and to prove. However, it becomes crucial to guarantee that these algorithms run as designed. Modularization mechanism in formal development provides a simple way to manage this complexity. In this paper, we rely on the modularization mechanism of the Event-B method and on local computations model to propose a reuse based approach for modelling classes of distributed algorithms. The proposed approach consists in developing a formal pattern defined as a set of proved logical entities called modules. These modules are developed separately and, when needed, can be incorporated and instantiated in a given system development. Such a mechanism can save efforts on modelling and proving the computation steps in distributed algorithms.

In Wireless Sensor Networks, flooding in one of the basic communication primitives. It is used to propagate informations from one node to the entire network. Every node, receiving a piece of information, has to flood it to all its neighborhood. As informations to spread are important, such as fire or intrusion alerts, communications should be secured. In this paper, we present a greedy flooding algorithm for Wireless Sensor Networks secured by a Random Key Pre-distribution model that make them redoubtable. We present two theoretical upper bounds of the time complexity of this algorithm that depend on the network structure. We then use the ViSiDiA platform to implement and simulate our algorithm to validate these theoretical results.

Message authentication for resource constrained devices is a challenging topic. Indeed, given the scarceness of on-board resources, solutions that do not rely on asymmetric key cryptography are in demand. A few solutions to address this issue have been proposed, and some have gained the status of state of the art thanks to their effectiveness and efficiency. However, even if state of the art solutions do provide sender-receiver on-the-fly message authentication, they are not able to tackle a few relevant attacks on received messages when the time dimension is taken into account. In particular, we first introduce two types of attacks: the switch command attack (where an adversary pretends to “switch” two messages over time-that is, altering the relative time ordering), and the drop command attack (where an adversary could pretend not having received a message previously sent from the legitimate sender). We then propose a new solution for broadcast authentication that copes with the above introduced attacks: MASS. Our analysis shows that MASS is effective in detecting both switch command and drop command attacks.

In ad hoc networks, hierarchical routing is viewed as an effective solution to face scalability problems. Such routing relies on a subset of nodes to reduce control overhead associated to routing tasks and preserve network resources. Multipath routing can also be adopted in order to exploit suitably network resources by allowing load balancing and route fault tolerance. Combining the benefits of hierarchical routing and multipath routing can improve significantly the network performances and cope better with mobility. The main contribution of this paper is to propose a multipath extension of a hierarchical routing, which constructs link-disjoint paths and selects less congested and correlated paths for an efficient data transfer and resources use. The performance of our multipath algorithm is witnessed by simulation results. These results indicate that our proposed multipath extension is more effective under various traffic loads in terms of packet delivery ratio and control overhead.

Some of the specific challenges stemming from the ad hoc network are mobility and energy constraints. These intrinsic characteristics make the network management, routing and various networking related tasks more sophisticated. In fact, the most targeted MANET applications are based on collaborative computing where mobile hosts may be involved in team collaborations. Further, as network size increases, communication costs tend to consume a larger proportion of the limited bandwidth. Among the solutions proposed for scaling down large-sized networks, network clustering is one of the most investigated approaches. The basic idea is to select the appropriate nodes able to support additional tasks, so that routing and group communication protocols can be implemented efficiently on top of this virtual backbone. In this context, we propose an enhanced version of LCR (Layered Cluster-based Routing), a hierarchical routing protocol designed for dense and large scale networks. The key feature in this approach is the direction mechanism which limits the area concerned by establishment and maintenance of routes, and consequently reducing the number of dominating nodes involved in routing tasks. Conducted simulations on different scenarios highlight its ability to decrease the energy consumption and wasted bandwidth resources used for routing tasks.

Wireless sensor networks (WSNs) are being widely deployed in military, healthcare, and commercial environments. Because sensor networks pose unique challenges, traditional security methods, commonly used in enterprise networks, cannot be directly applied. In particular, broadcast source authentication is a critical security requirement in wireless sensor networks. Therefore, formal validation of source authentication protocols in wireless sensor networks has become an important research topic. The Multi-Level-µTESLA, Staggered Multi-Level-µTESLA, and Bloom Filter based source authentication protocols are potential candidates for source authentication in WSNs but so far, there has been no formal validation of those protocols. In this paper, we aim to formally verify and model those three authentication protocols using the AVISPA model-checking tool and HLPSL language. We show that those protocols can safely be used for source authentication. We also show that those three protocols exhibit also some DoS attack problems which are hard to eliminate.

The intrinsic characteristics of ad hoc networks, such as the frequent connectivity changes and the strict bandwidth and power constraints, impose further challenges, especially for routing tasks. Besides, existing routing algorithms devoted to ad hoc networks and based on proactive or reactive schemes suffer from scalability due to their intrinsic mechanisms. The control overhead induced by routing packets is a primary factor, since it increases with the number of nodes, especially in large and dense networks evolving in a dynamic environment. Relying on a virtual infrastructure seems a promising approach to overcome the scalability problem. The basic idea consists on assigning additional tasks to a limited set of dominating nodes, satisfying specific requirements. In this paper, we present a routing algorithm, which exploits the benefits of our clustering algorithm TBCA. Conducted simulations show the ability of our new approach to reduce the control overhead and improve the reactivity of routing to the topology changes.

Despite the wide spread of interest to ad hoc networks and the rapid development in wireless communication technologies, energy consumption still remains a critical issue. The use of a low-power mode has been adopted by many approaches in the literature to conserve energy. It allows nodes to switch to the sleeping mode whenever possible to conserve energy. However, most of these approaches do not take into account the impact of such a mode on network capacity and performances. Combining the power saving mode and a clustering technique seems to be a promising approach. In this paper, we present a power saving approach which relies on a virtual infrastructure formed by elected clusterheads and gateways to conserve network capacity. The main contribution lies on the differentiation among packets based on the amount of network resources they have been so far consumed. The proposed structure of the beacon interval can be adjusted dynamically and locally by each node according to its own specific requirements. The good performance of our algorithm in terms of more energy saving and better network throughput is witnessed by extensive simulations under various traffic loads.

Security in mobile agent systems is twofold: protection of mobile agents and protection of agent execution system. Indeed, the proposed solutions for the security of distributed systems arenpsilat sufficient. Moreover, therepsilas no solution which treats the different concerns of security in the mobile agent systems. To achieve this goal, we use formal foundations which provide a rigorous reasoning about security of mobile agent systems. We propose in this paper a formal framework for the security in mobile agent systems which consists of three basic frameworks. The specification framework proposes, explicitly, a generic definition of security policies that may be enhanced by several concepts related to one or more security models. For illustration, we present a security policy enhancement based on the concepts of the RBAC model. Inevitably, we associate to the specification framework a verification framework which checks the consistency of the proposed specifications as well as the consistency intra-policy. In response to the dynamic changes of security requirements in mobile agent systems, we propose a third framework for the reconfiguration of policies.

Needless to say, distributed algorithms are usually hard to design mush harder to prove and to use in real distributed systems. In these systems, local computations theory has proved its power to formalize and prove in an intuitive way distributed algorithms. This paper uses this formalism to present solutions to the election problem in several network topologies using mobile agents at the design and the implementation levels. We formalized the proposed solutions in the local computations model using transition systems [11]. This facilitates the proof of the proposed solutions using the mathematical tool-box provided by the local computation theory. Using mobile agents, the proposed solutions get rid of synchronization and do not need continuous use of all machines computational resources. Proposed solutions are also simulated within the VISIDIA [3] platform.

Distributed applications are becoming increasingly common. However, incorporating security in them remains a major challenge. There are currently few choices to express and enforce security in distributed systems. We can either use a special-purpose language which may be too limited to express security requirements, or use a general purpose language that provides the ability to make complicated security policy but makes us reimplement infrastructure code for authorization, interdiction, obligation and so on with each new security policy. In this paper, we introduce a domain-specific language approach that takes the middle road, giving a way to reuse security infrastructure for new policies while also allowing the expression of complicated security policy easily. We present our DSL approach and and apply it to a real-world scenario: specification and implementation of security policy.

One of the most important issues in mobile agent systems is the security aspect. For the purpose of ensuring security, we provide in this paper a formal model for secure mobile agent system. This model supports the specification of numerous security policy types which control the behaviour of system entities and protect them, as far as possible, from attacks that may occur. In order to verify whether a security policy could overcome a given kind of attack, we present a formal approach to this end. Thus, we propose a precise and formal representation of possible attacks that may occur in a mobile agent systems. According to this representation, we define a set of proved theorems which describe under what conditions a policy succeeds to prevent those attacks. The proposed specifications have been formalized using Z notation and checked using the Z-EVES tool.

This work constitutes a part of a general research project aiming at defining a generic framework for developing secure mobile agent systems stamped with a lack of consensus about their fundamental concepts. In order to facilitate analysis, design and specification of mobile agent systems, we present in this paper a brief definition and relationship among most key concepts for modeling a mobile agent system and the interaction within such dynamic environment. In order to overcome the possible attacks that may occur in a mobile agent system, we must associate the specification of the basic concepts that ensuring security such as: agent authenticity, authority access, security policy and its various kind. The syntax and the semantic of the proposed specifications have been checked using the Z-EVES tool.