The use of security patterns has been recognized as effective in mitigating vulnerabilities in software systems. However, it is still not well understood how they can be applied systematically and effectively in concrete systems to achieve the best results. We present a formal approach based on the Alloy model checker to detect information disclosure vulnerabilities and enforce appropriate security patterns automatically. The approach helps improve the overall security posture of software systems while reducing the dependence on manual security analysis. We demonstrate the usability of our approach through the use case of a Smart Meter Gateway. The proposed approach is generic and constitutes a significant advancement toward systematic methods for designing secure software systems.

Electric vehicles (EVs) have gained significant attention due to their environmental and energy-efficient benefits. Dynamic Wireless Charging (DWC) has emerged as one of the most promising EV charging methods because it overcomes the challenges associated with traditional charging stations. However, as EVs keep moving while charging, this requires specific authentication and payment methods, enabling EV mobility privacy and ensuring fair billing. To address these concerns, we propose in this paper a smart contract based solution to deal with privacy and fair billing for EVs dynamic wireless charging. The proposed solution includes a lightweight authentication mechanism enabling a continuous authenticate-and-charge process when EV is moving on the road.

In-motion wireless charging services have emerged for the development of Electric Vehicles (EVs) industry. Fast authentication and privacy awareness are the major concerns in this promising technology. This paper proposes FLPA, a fast and anonymous authentication scheme for EVs charging on the move, which preserves the identity and location privacy of EVs during the recharging process. In order to deal with EV's high mobility and constrained resources of charging pads, FLPA provides lightweight and fast EVs authentication to charging pads while ensuring secure and fair-billing based on authenticated pairwise keys and coin chains. Through a performance analysis, we demonstrate our scheme's advantage compared to current solutions.

Providing a long term security of a computer system requires an efficient management of the resources consumption. This is particularly true for the Mobile Ad-hoc NETworks (MANETs) where nodes are characterized by limited resources. In this paper, we propose a game theoretic framework to predict malicious behaviors within a MANET and to analyze the best security alternatives that preserve the resources consumption of network entities. We model the interactions between an attacker and a defender evolving in the same environment as an evolutionary game. In these games, each entity can learn about the behavior of its opponent over time allowing the adjustment of its strategy. The main results of our game model are the elaboration of the Evolutionary Stable Strategies (ESSs) which is a stronger concept of equilibria and the illustration of the evolution process, based on the replicator dynamic. Numerical experiments verify the correctness of our theoretical analysis and show the feasibility and effectiveness of our model.

In Cloud environments, Cloud users have the possibility to put their sensitive data on Cloud servers, which opens the door to security challenges concerning data protection. In this context, access control is of vital importance, since it provides security mechanisms to protect against inappropriate access to data. Unfortunately, classical access control models such as DAC, MAC, RBAC or ABAC are not sufficiently expressive for highly flexible and dynamic environments such as those found in the Cloud. Often, a combination of elements of these models is necessary in order to properly express varied data protection needs. In this paper, we present a new approach called CatBAC (Category Based Access Control), for building dedicated access control models starting from an abstract meta-model. Hence, in our approach, a meta-model can be refined in accordance with the high level security policies of each specific user. Our framework for building access control models can be implemented as a Cloud service and Cloud providers will then apply different concrete access control models produced by each user to process its incoming access requests.

Several formal access control models are known in the literature, such as DAC, MAC, RBAC, etc. However, these models cannot meet new security requirements required by flexible and dynamic environments which necessitate a combination of elements of these models, in order to properly express varied data protection needs. In this paper, we present a new method for the specification of access control systems. The method makes it possible to design an access control system specific to the high level policy of an organization. The method is based on a generic UML meta-model of access control called CatBAC (Category Based Access Control), together with a refinement process for the extraction of security requirements from high level policies. Based on the category concept, the CatBAC meta-model allows specifying hybrid policies of access control.

Many access control models have been proposed in the literature, and they have been extensively studied under the acronyms of DAC, MAC, RBAC, ABAC, etc. Each of these models has been studied in isolation, but some real-life situations need elements of several of them, in order to properly express data protection needs of complex organizations. A formal framework is presented, that allows not only to combine elements of these models, but also to generalize them in new ways. This framework includes elements of a lifecycle methodology, which starts with a UML-based formalism, called UACML, that expresses semantic elements (classes and their relationships) needed for general access control systems. It continues with the representation of UACML diagrams in our language CatBAC. The latter is a compact textual representation of UACML that makes it possible to express realistic policy systems involving many entities and many constraints. CatBAC is based on Prolog, and this makes it possible to implement analysis and verification tools.

Traditional security and access control systems, such as MLS/Bell-LaPadula, RBAC are rigid and do not contain automatic mechanisms through which a system can increase or decrease users' access to classified information. Therefore, in this paper, we propose a risk-based decision method for an access control system. Firstly, we dynamically calculate the trust and risk values for each subject-object pair. Both values are adaptive, reflecting the past behavior of the users with particular objects. The past behavior is evaluated based on the history of reward and penalty points. These are assigned by the system after the completion of every transaction. Secondly, based on the trust and risk values, an access decision is made.

In enterprise environments, the task of assigning access control rights to subjects for resources is not trivial. Because of their complexity, distribution and size, access control policies can contain anomalies such as inconsistencies, which can result in security vulnerabilities. A set of access control policies is inconsistent when, for specific situations different incompatible policies can apply. Many researchers have tried to address the problem of inconsistency using methods based on formal logic. However, this approach is difficult to implement and inefficient for large policy sets. Therefore, in this paper, we propose a simple, efficient and practical solution for detecting inconsistencies in access control policies with the help of a modified C4.5 data classification algorithm.

Commonly known access control systems respond to users' requests to perform actions on protected objects by giving binary answers such as permit or deny. The decisions are taken on the basis of access control policies, where the risk of allowing access is not necessarily taken into explicit consideration. In this paper, we introduce RBACRmodel (Role Based Access Control Model with Risk), in which each access control decision is taken after consideration of risk assessment. The proposed risk assessment method considers partial orderings on objects and actions to capture the notions of importance of objects and criticality of actions, and determines the risk of assigning a specific role to a specific user. The case of role delegation is also considered.

Abstract Securing Mobile ad hoc Networks (MANET) is a challenging task, notably due to the lack of an online infrastructure. In particular, key management in MANET is a problem for which many solutions have been proposed in literature. Unfortunately, these solutions are rather limited in terms of security and availability of keys. In this paper, we propose a secure, robust, and fully distributed scheme for public‐key certificate management in MANET. Our scheme, based on threshold cryptography, ensures that the private key of the certificate authority will not be revealed to an adversary, even if the number of compromised shareholders exceeds the threshold of vulnerability, thereby thwarting mobile‐adversary attacks. We describe SRKM in detail and, by using security analysis and simulations, show its effectiveness, robustness and security. Copyright © 2010 John Wiley & Sons, Ltd.

This paper proposes robust key management scheme (RKM ): a new certification management scheme for mobile ad-hoc networks. RKM, based on threshold cryptography, ensures better robustness compared to other schemes proposed in the literature. In particular, it guarantees the confidentiality of the private key of the certification authority, even if the number of compromised nodes exceeds the threshold of vulnerability. Thus, our model offers better protection against many attacks such as mobile adversary attack.

A firewall is one of the major security tools available for protecting computer domains. Today, almost all companies have at least one firewall to filter incoming and outgoing traffic according to some requirements called security policy. The configuration of firewalls is however complex and error prone. During the last years, many techniques and tools have been proposed to analyze firewalls. However, most of existing worksare informaland the formalfoundationof firewall is still a missing part. The goal of this paper is to present an overview of the most important problems related to the firewall configuration and analysis. Also, it proposes a formal language for the specification and the verification of firewalls.

A security protocol is a distributed program that can be executed by several actors. Since several runs of the protocol within the same execution are allowed, the protocol models are often infinite and very hard to analyze. In this paper we present a formal reasoning for evaluating security protocol correctness with respect to secrecy and authentication. We build a bounding model for multi-session cryptoprotocol attacks and prove that this model is appropriate for the analysis of the intruder's possible behavior and for demonstrating protocol correctness with respect to both secrecy and authentication. The result allows us to evaluate accurately the intruder's knowledge and his potential actions for building winning strategies during an attack.