With the emergence of the digital transition, the need to control the processing of digital information has significantly increased. In the EU in particular, Law Enforcement Agencies (LEAs) are caused to exchange information. In recent years, many regulations have emerged to control data processing and exchange. Texts other than the GDPR, such as the “Law Enforcement Directive (LED)”, appeared to regulate specifically their data processing. And although many new formalisms have emerged to represent legal norms and rules, few are provided with a reasoning mechanism. The explainability of the results of systems using these formalisms also remains a major issue when dealing with critical decision situations. This paper aims to propose a framework to operate formal rules from regulations and guide a user in its decision process in a situation of data processing by LEAs by focusing on both the operability of the rules through reasoning and the explainability of the results from the reasoning.

Deciding privacy-type properties of deterministic cryptographic protocols such as anonymity and strong secrecy can be reduced to deciding the symbolic equivalence of processes, where each process is described by a set of possible symbolic traces. This equivalence is parameterized by a deduction system that describes which actions and observations an intruder can perform on a running system.We present in this paper a notion of finitary deduction systems. For this class of deduction system, we first reduce the problem of the equivalence of processes with no disequations to the resolution of reachability problem on each symbolic trace of one process, and then testing whether each solution found is solution of a related trace in the other process. We then extend this reduction to the case of generic deterministic finite processes in which symbolic traces may contain disequalities.

Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable-origination. In this work we relax these restrictions by giving an NP decision procedure for solving general intruder constraints (that do not have these properties). Our result extends a first work by L. Mazaré in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modeling sets). We also give several new applications of the result.

In a distributed environment, and more specially in service oriented architectures, the entities interacting one with another rely on credentials to decide whether an action they are told to perform is permitted. These credentials are exchanged within trust negotiation sessions during which the participating entities build up trust by communicating certificates to trusted peers. Dolev and Yao have introduced a notion of symbolic intruder to represent the capacities of a malicious agent trying to attack a cryptographically secured communication protocol. We present in this paper an adaptation of that intruder that retains the same deductive capabilities but is specialized for the analysis of the exchanges during a trust negotiation session. In particular this permits us to analyze the security of a distributed access control policy w.r.t. a malicious insider.

We propose in this paper a framework in which the security policies of services in a distributed environment can be expressed. Services interact by exchanging credentials. Each service is made up of an access control policy protecting the access to the service, and of a trust negotiation policy controlling the accessibility of the credentials for other services. We add a workflow layer for each service to model its dynamic evolution with respect to the performed accesses. Unlike most of the access control policies which are uniquely based on roles, we choose an attribute based framework leading to more flexibility in the characterization of users. The strengths of this framework are its ability to control and check the access control aspect of the services and its dynamic evolution based on an exchange of credentials. We provide a unified framework for reasoning on access control policies, trust negotiation policies and workflows.

We show that the insecurity problem for protocols with modular exponentiation and arbitrary products allowed in exponents is NP-complete. This result is based on a protocol and intruder model which is powerful enough to uncover known attacks on the Authenticated Group Diffie-Hellman (A-GDH.2) protocol suite. To prove our results, we develop a general framework in which the Dolev-Yao intruder is extended by generic intruder rules. This framework is also applied to obtain complexity results for protocols with commuting public key encryption.

We provide a method for deciding the insecurity of cryptographic protocols in presence of the standard Dolev-Yao intruder (with a finite number of sessions) extended with so-called oracle rules, i.e., deduction rules that satisfy certain conditions. As an instance of this general framework, we ascertain that protocol insecurity is in NP for an intruder that can exploit the properties of the XOR operator. This operator is frequently used in cryptographic protocols but cannot be handled in most protocol models. An immediate consequence of our proof is that checking whether a message can be derived by an intruder (using XOR) is in P. We also apply our framework to an intruder that exploits properties of certain encryption modes such as cipher block chaining (CBC).

We present the lazy strategy implemented in a compiler of cryptographic protocols, Casrul. The purpose of this compiler is to verify protocols and to translate them into rewrite rules that can be used by several kinds of automatic or semi-automatic tools for finding flaws, or proving properties. It is entirely automatic, and the efficiency of the generated rules is guaranteed because of the use of a lazy model of intruder behavior. This efficiency is illustrated on several examples.