Multi-Agent System (MAS) verification comprises formal techniques to model distributed systems, express system properties, and verify them. Capacity Alternating-time Temporal Logic (CapATL) was recently introduced to reason about MASs where agents can have different profiles, called capacities. However, CapATL assumes agents know the global system state throughout the interaction, which is a strong constraint. This paper extends the concept of agent capacities to systems with imperfect information, enabling the formalisation of a wide range of systems which were previously out of reach. Our contributions are: (i) an extension with imperfect information of CapATL, called Capacity Alternating-time Temporal Epistemic Logic (CapATEL), (ii) the analysis and comparison of different semantics, (iii) a completeness result for the CapATEL model-checking problem when agents have bounded recall, and (iv) a cybersecurity illustration that showcases CapATEL’s applicability.

In multi-agent systems, especially in cybersecurity, the dynamic interplay between attackers and defenders is crucial to the security and resilience of the system. Traditional methods often assume static game models and fail to account for the strategic adaptation of the environment to the actions of the players. This paper presents Coalition Obstruction Temporal Logic (COTL), a formal framework for analyzing defender coalitions in dynamic game scenarios. Within this framework, defenders, conceptualized as demons, can actively obstruct attackers by selectively disabling certain actions in response to perceived threats. We establish the formal semantics of COTL and propose a model checking algorithm to verify complex security properties in systems with evolving adversarial dynamics. The utility of the framework is demonstrated through its application to a coalition of defenders that collaboratively defend a system against coordinated attacks.

Cyber-Physical Systems (CPSs) complexity has been continuously increasing to support new life-impacting applications, such as Internet of Things (IoT) devices or Industrial Control Systems (ICSs). These characteristics introduce new critical security challenges to both industrial practitioners and academics. This work investigates how Model-Based System Engineering (MBSE) and attack graph approaches could be leveraged to model secure Cyber-Physical System solutions and identify high-impact attacks early in the system development life cycle. To achieve this, we propose a new framework that comprises (1) an easily adoptable modeling paradigm for Cyber-Physical System representation, (2) an attack-graph-based solution for Cyber-Physical System automatic quantitative security analysis, based on the MulVAL security tool, (3) a set of Model-To-Text (MTT) transformation rules to bridge the gap between SysML and MulVAL. We illustrated the validity of our proposed framework through an autonomous ventilation system example. A Denial of Service (DoS) attack targeting an industrial communication protocol was identified and displayed as attack graphs. In future work, we intend to connect the approach to dynamic security databases for automatic countermeasure selection.

International audience

Games that are played in a dynamic model have been studied in several contexts, such as cybersecurity and planning. In this paper, we introduce a logic for reasoning about a particular class of games with temporal goals played in a dynamic model. In such games, the actions of a player can modify the game model itself. We show that the model-checking problem for our logic is decidable in polynomial-time. Then, using this logic, we show how to express interesting properties of cybersecurity games defined on attack graphs.

An attack graph is a succinct representation of all the paths in an open system that allow an attacker to enter a forbidden state (e.g., a resource), besides any attempt of the system to prevent it.Checking system vulnerability amounts to verifying whether such paths exist.In this paper we reason about attack graphs by means of a game-theoretic approach.Precisely, we introduce a suitable game model to represent the interaction between the system and the attacker and an automata-based solution to show the absence of vulnerability.

International audience

The demand for Internet of Things services is increasing exponentially, and consequently a big number of devices are being deployed. To efficiently authenticate these services, the use of Physical Unclonable Functions (PUF) has been introduced as a promising solution that is suitable for the resource-constraint nature of these devices. A growing number of PUF architectures has been demonstrated mathematically clonable through Machine Learning (ML) modeling techniques. The use of ML PUF models has been recently proposed to authenticate the IoT objects. This procedure facilitates the scalability of the authentication process by reducing the storage space required for each device. Nonetheless, the leakage scenario of the PUF model to an adversary due to an insider threat within the organization is not supported by the existing solutions. Hence, the security of these PUF model-based enrollment proposals can be compromised. In this paper, we propose an enrollment solution that exploits a ML PUF model in the authentication process, called Water-PUF. Our enrollment scheme is based on a specifically designed black-box watermarking technique for PUF models with a binary output response. This procedure prevents an adversary from relying on the watermarked model in question or another derivative model to bypass the authentication. Therefore, any leakage of the watermarked PUF model that is used for the enrollment does not affect the correctness of the protocol. The Water- PUF design is validated by a number of simulations against numerous watermark suppression attacks to assess the robustness of our proposal.

Moving Target Defense (MTD) is a promising de-fense technique that aims to break the asymmetry between attacker and defender by reconfiguring a system's assets. When used in a critical embedded system, non-functional constraints limit the set of usable MTD techniques, therefore limiting the entropy of reconfigurations. It is therefore necessary to compute an optimal moving target strategy in order to reduce the time between reconfigurations, while managing their impact on the quality of service provided to users. In this paper, we propose a game-theoretic approach to define an optimal moving target defense strategy. Our approach translates risk analysis parame-ters into a Bayesian Stackelberg game, which we translate to a mixed integer linear program. We validate our approach on an industrial case study from the automotive domain, showing the practical usability of our approach. In further experiments, we assess the scalability of our method, as well as the solution's stability in case new vulnerabilities are discovered after the deployment of the system.

Numerous secure device pairing (SDP) protocols have been proposed to establish a secure communication between unidentified IoT devices that have no preshared security parameters due to the scalability requirements imposed by the ubiquitous nature of the IoT devices. In order to provide the most user‐friendly IoT services, the usability assessment has become the main requirement. Thus, the complete security analysis has been replaced by a sketch of a proof to partially validate the robustness of the proposal. The few existing formal or computational security verifications on the SDP schemes have been conducted based on the assessment of a wide variety of uniquely defined security properties. Therefore, the security comparison between these protocols is not feasible and there is a lack of a unified security analysis framework to assess these pairing techniques. In this paper, we survey a selection of secure device pairing proposals that have been formally or computationally verified. We present a systematic description of the protocol assumptions, the adopted verification model, and an assessment of the verification results. In addition, we normalize the used taxonomy in order to enhance the understanding of these security validations. Furthermore, we refine the adversary capabilities on the out‐of‐band channel by redefining the replay capability and by introducing a new notion of delay that is dependent on the protocol structure that is more adequate for the ad hoc pairing context. Also, we propose a classification of a number of out‐of‐band channels based on their security properties and under our refined adversary model. Our work motivates the future SDP protocol designer to conduct a formal or a computational security assessment to allow the comparability between these pairing techniques. Furthermore, it provides a realistic abstraction of the adversary capabilities on the out‐of‐band channel which improves the modeling of their security characteristics in the protocol verification tools.

International audience

ESIoT is a secure access control and authentication protocol introduced for Internet of Things (IoT) applications. The core primitive of ESIoT is an identity-based broadcast encryption scheme called Secure Identity-Based Broadcast Encryption (SIBBE). SIBBE is designed to provide secure key distribution among a group of devices in IoT networks, and enable devices in each group to perform mutual authentication. The scheme is also designed to hide the structure of the group from nodes outside of the group. We identify multiple efficiency and security issues in this primitive that prove SIBBE unsuitable for IoT applications. First, we show that contrary to what was claimed, the size of the ciphertexts generated by the encryption function is not constant but in fact linear in the number of devices in the group. Additionally, we demonstrate that the encryption and decryption costs are also linear in the number of nodes in the group, implying scalability issues thus inefficiency for IoT applications. In terms of security, we prove that SIBBE does not achieve the desired property of anonymity and allows an attacker to gain information on the structure of any given group. Finally, we demonstrate how SIBBE does not achieve the claimed chosen-ciphertext security. We however prove its security for a weaker security notion (namely selective-ID indistinguishability against chosen-plaintext attacks) under a variant of the GDDHE assumption.

The new developments in cloud computing have introduced significant security challenges to guarantee the confidentiality, integrity, and availability of outsourced data. A service level agreement (SLA) is usually signed between the cloud provider (CP) and the customer. For redundancy purposes, it is important to verify the CP's compliance with data backup requirements in the SLA. There exist a number of security mechanisms to check the integrity and availability of outsourced data. This task can be performed by the customer or be delegated to an independent entity that we will refer to as the verifier. However, checking the availability of data introduces extra costs, which can discourage the customer of performing data verification too often. The interaction between the verifier and the CP can be captured using game theory in order to find an optimal data verification strategy. In this paper, we formulate this problem as a two player non-cooperative game. We consider the case in which each type of data is replicated a number of times, which can depend on a set of parameters including, among others, its size and sensitivity. We analyze the strategies of the CP and the verifier at the Nash equilibrium and derive the expected behavior of both the players. Finally, we validate our model numerically on a case study and explain how we evaluate the parameters in the model.

The need to secure communications between personal devices is increasing nowadays, especially in the context of Internet of Things. Authentication between devices which have no prior common knowledge is a challenging problem. One solution consists in using a pre-authenticated auxiliary channel, human assisted or location limited, usually called out-of-band channel. A large number of device pairing protocols using an out-of-band channel were proposed. However most of these propositions lacks a formal analysis, and therefore may be vulnerable to some attacks. In this paper, we introduce a new key agreement protocol between two wireless devices. This protocol, only using two wireless messages and one out-of-band message, offers better communication costs than currently existing solutions, yet still ensuring a reasonable security. Security of our proposal is validated both via a formal proof of the security of our protocol in an extension of the strand space model and an estimation of the attack success probability in a computational model.

The need to secure communications between personal devices is increasing nowadays, especially in the context of Internet of Things. Authentication between devices which have no prior common knowledge is a challenging problem. One solution consists in using a pre-authenticated auxiliary channel, human assisted or location limited, usually called out-of-band channel. A large number of device pairing protocols using an out-of-band channel were proposed, but they usually suffer from a lack of formal analysis. In this paper, we introduce a formal model, conceived as an extension of Strand Spaces, to analyze such protocols. We use it to analyze a device pairing protocol with unilateral out-of-band channel proposed by Wong & Stajano. This leads us to discover some vulnerabilities in this protocol. We propose a modified version of the protocol together with a correctness proof in our model.

The widespread deployment of smart meters in the advanced metering infrastructure (AMI) raises privacy concerns. Analyzing the data collected from smart meters can expose habits and can be potentially used to predict consumers' behaviors. In this paper, we analyze the confidentiality of information in the AMI consisting of nodes with interdependent correlated security assets. On each node, the defender can choose one of several security modes available. We try to answer the following questions: 1) What is the expected behavior of a rational attacker?; 2) What is the optimal strategy of the defender?; and 3) Can we configure the security modes on each node to discourage the attacker from launching any attacks? In this paper, we formulate the problem as a noncooperative game and analyze the behavior of the attacker and the defender at the Nash equilibrium. The attacker chooses his targets in order to collect the maximum amount of data on consumers, and the defender chooses the encryption level of outbound data on each device in the AMI. Using our model, we derive the minimum defense resources required and the optimal strategy of the defender. Finally, we show how our framework can be applied in a real-world scenario via a case study.

Extensive research in recent years has shown the benefits of cooperative relaying in wireless networks, where nodes overhear and cooperatively forward packets transmitted between their neighbors. Most existing studies focus on physical-layer optimization of the effective channel capacity for a given transmitter-receiver link; however, the interaction among simultaneous flows between different endpoint pairs, and the conflicts arising from their competition for a shared pool of relay nodes, are not yet well understood. In this paper, we study a distributed pricing framework, where sources pay relay nodes to forward their packets, and the payment is shared equally whenever a packet is successfully relayed by several nodes at once. We formulate this scenario as a Stackelberg (leader-follower) game, in which sources set the payment rates they offer, and relay nodes respond by choosing the flows to cooperate with. We provide a systematic analysis of the fundamental structural properties of this generic model. We show that multiple follower equilibria exist in general due to the nonconcave nature of their game, yet only one equilibrium possesses certain continuity properties that further lead to a unique system equilibrium among the leaders. We further demonstrate that the resulting equilibria are reasonably efficient in several typical scenarios.

In this paper, we address the crucial issue of how to design efficient MAC protocols in autonomous wireless networks with selfish users. We model the wireless medium access control problem as a non-cooperative game in which the MAC protocol can be regarded as distributed strategy update scheme approaching the equilibrium point. Under such game theoretic framework, three MAC protocols, the aggressive, conservative and cheat-proof MAC protocol, are then proposed with tunable parameters allowing them to converge to the desired social optimal point. The first two MAC protocols require network participants to follow the rules, while the cheat-proof MAC protocol can survive the selfish environments where nodes are purely self-interested. Based on our game theoretic analysis, we provide a general methodology for designing efficient MAC protocols for autonomous wireless networks. We believe that the proposed methodology not only provides a general way of designing stable and controllable MAC protocols achieving high performance even in selfish environments, but also provides a general framework that can be extended to design efficient protocols in other non-cooperative environments.

Due to the dynamic, distributed, and heterogeneous nature of today's networks, intrusion detection systems (IDSs) have become a necessary addition to the security infrastructure and are widely deployed as a complementary line of defense to classical security approaches. In this paper, we address the intrusion detection problem in heterogeneous networks consisting of nodes with different noncorrelated security assets. In our study, two crucial questions are: What are the expected behaviors of rational attackers? What is the optimal strategy of the defenders (IDSs)? We answer the questions by formulating the network intrusion detection as a noncooperative game and performing an in-depth analysis on the Nash equilibrium and the engineering implications behind. Based on our game theoretical analysis, we derive the expected behaviors of rational attackers, the minimum monitor resource requirement, and the optimal strategy of the defenders. We then provide guidelines for IDS design and deployment. We also show how our game theoretical framework can be applied to configure the intrusion detection strategies in realistic scenarios via a case study. Finally, we evaluate the proposed game theoretical framework via simulations. The simulation results show both the correctness of the analytical results and the effectiveness of the proposed guidelines.

We present a game-theoretic study on the power and rate control problem in IEEE 802.11 WLANs where network participants choose appropriate transmission power and data rate to achieve maximum throughput with minimum energy consumption. In such game-theoretic study, the central issues are the existence, uniqueness of the Nash equilibrium (NE), the convergence to the NE and the system performance at the NE. We conduct our study for three specific games: the fixed-rate power control game GNPC, the fixed-power rate control game GNRCand the joint power rate control game GNJPRC. As main contributions, we establish the existence, uniqueness and convergence of the NE for the three games. In GNRCwhere the NE is inefficient, we provide pricing scheme to improve the efficiency. Based on our analysis on GNJPRC, we propose the joint power and rate control procedure to approach the NE which is proven to be social optimal. The procedure is distributed and simple to incorporate into the existing IEEE 802.11 MAC protocol.

We present our paradigm of autonomic networks through a specific model of mobile ad hoc networks. Accordingly, we define a security platform, in which we introduce basic solutions for building autonomic security systems. We then present our relevant studies about event-driven network security evolution, security-policy negotiation and enforcement, and collaboration between autonomic nodes.

We present a non-cooperative game-theoretical study of the power and rate control problem in IEEE 802.11 WLANs where network participants choose appropriate transmission power and data rate to achieve maximum throughput with minimum energy consumption. In such game-theoretical study, the central question is whether a Nash equilibrium (NE) exists, if so, whether the network operates efficiently at the NE. In this paper, we show the existence and uniqueness of the NE and the convergence to the NE under best response strategy. However, the unique NE is inefficient, i.e., neither social optimal nor Pareto optimal. Motivated by this fact, we propose both linear and non-linear pricing scheme to improve efficiency. We demonstrate that by wisely choosing the parameters, the game converges to an efficient NE. Finally, we examine the convergence to the NE under a practical rate update scheme: the subgradient rate update. Both analytical and numerical results show that the proposed rate control scheme can lead the network to the social optimal equilibrium.

In wireless mobile ad hoc networks where nodes are selfish and non-cooperative, a natural and crucial question is how well or how bad the MAC layer protocol IEEE 802.11 DCF performs. In this paper, we study this question by modeling the selfish MAC protocol as a non- cooperative repeated game where players follow the TIT- FOR-TAT (TFT) strategy which is regarded as the best strategy in such environments. We show for single-hop ad hoc networks the game admits a number of Nash Equilibria (NE). We then perform NE refinement to eliminate the inefficient NE and show that there exists one efficient NE maximizing both local and global payoff. We also propose an algorithm to approach the efficient NE. We then extend our efforts to multi-hop case by showing that the game converges to a NE which may not be globally optimal but quasi- optimal in the sense that the global payoff is only slightly less than the optimal case. As conclusion, we answer the posed question by showing that selfishness does not always lead to network collapse. On the contrary, it can help the network operate at a NE globally which is optimal or quasi-optimal under the condition that players are long-sighted and follow the TFT strategy.

In this paper, motivated by the need of a quantitative model for the power and rate control in IEEE 802.11 WLANs and the lack of related work in the literature, we address the problem by establishing a quantitative game theoretic framework. Our motivation of using game theoretic approach rather than global optimization approach is two-fold: 1) game theory is a powerful tool to model selfish behaviors and their impact on the system performance in distributed environments with self-interested players; 2) game theory can model the features or constraints of IEEE 802.11 WLANs such as lack of coordination and network feedback.