Data privacy and security is becoming one of the most important subjects for IT companies, as it has the potential to shift their reputation and therefore influence their value on the market. However, on a large scale, namely in Big Data platforms, securing data may be a major challenge as it can limit the system's performance. Therefore, finding solutions that enable a compromise between security and performance is a must. In this paper, we present a framework called Distributed Cipher Chaining (DCC) which allows the creation of flexible encryption schemes that can offer configurable levels of availability. We also present a local multi-threaded implementation as well as a distributed multi-process implementation and the advantages and applications of each one. We show that our solution is well adapted to large files as it outperforms state-of-the art methods while improving the diffusion rate.

The formal Event-B method makes it possible to obtain systems or software correct by construction. The modeling activity aims to establish formal models in Event-B. As for the proof activity, it aims at correcting these models. A proven Event-B model is not necessarily valid. We propose to open the Event-B formal method on PDDL in order to further validate Event-B models. We aim to validate the dynamic properties related to the sequence of events authorized on Event-B models. PDDL is a de facto standard language for planning problems. It is equipped with planners to automatically generate solution-plans. To achieve this, we successfully used the MDE approach, Xtext to create an integrated development environment specific to the Event-B language and the Xtend tool to implement our transformation EventB2PDDL and produce PDDL descriptions using a top-down approach.

Summary One of the most critical properties that must be ensured to have a secure electronic voting is verifiability. Political parties, observers, and especially voters want to be able to verify that all eligible votes are cast as intended and counted as cast without compromising votes secrecy or voters privacy. Over the past few decades, an important number of e‐voting protocols attempt to deal with this issue by using cryptographic techniques and/or a public bulletin board. Recently, some blockchain‐based e‐voting systems have been proposed, but were not found practical in the real world, because they do not support situations with large numbers of candidates and voters. In this article, we design and implement a verifiable blockchain‐based online voting protocol, called verify‐your‐vote . Our protocol ensures several security properties thanks to some cryptographic primitives and blockchain technology. We also evaluate its performance in terms of time, cost, and the number of voters and candidates that can be supported.

Cloud computing is an on-demand computing model, using virtualization technology to provide services to users in the form of virtual machines (VMs) through internet. Job-scheduling is one of the fundamental reasons to have high performance in a cloud environment. Therefore, there is a need for protocols that can efficiently allocate jobs to resources. However, due to the lack of an explicit and formal description of the resource perspective in the existing cloud platforms, the correctness of Cloud resources management can not be verified. The aim of the present work is to offer a formal description as a step towards ensuring a correct and consistent Cloud resource allocation modeling. In particular, we propose a distributed formal model for the description of a job-scheduling protocol in the cloud which considers the types of jobs and the resource availability in its scheduling decision. The formal verification of different properties of the proposed model has been performed automatically using Model-checking.

An electronic passport is a relatively new document type which many states are considering as a new form for travelling. E-passport is significantly more secure than a traditional passport. It promises the possibility of secure, simple and quick travel formalities. It is a relatively new feature and it deploys new technologies such as biometrics and Radio Frequency identification. We delve into security features and implications of this impending universal experiment of authentication technology. E-passport is involved in the improvement of travelling security. It is expected to protect data and guarantee authentication on inspection processes. International organizations are enhancing standards of E-passport security by implementation of new protocols. However, attackers still able to break them. In this paper, a new mechanism is presented to strengthen e-passport authentication process. We propose a new protocol based on Elliptic Curve, Identity-Based Encryption and Shared Secret between entities. We formally analyse the authentication of the protocol using the BAN Logic language, which is specially dedicated to describe and verify security protocols. This proposal aims to provide a secure data storage and authentication.

The orientation towards web service technology gives a raise to huge number of functionally similar web services. Hence, quality of service is becoming more important and even essential in web service technology as a distinctive criterion. Generally providers have sufficient information about the really provided quality, however, clients don't. Service level agreements that define the relationship between consumer and provider are the only way to express their functional as well as non-functional requirements and to rise notifications to providers in case of violation. One of the major challenges in this regard is to provide ways to assign responsibilities of each party (client / provider) in such case. The idea is to include expectations for measurable and only-provider related attributes (accessibility, availability, throughput,...). Time is a common measure of performance, but it is reduced into a unique temporal attribute: the response time. The latter depends simultaneously on client, network and provider side. Thus, we introduce three temporal attributes namely connection time, transport time and execution time. In this work, we study quality attributes and propose a quality model which includes a set of selected measurable and only provider related attributes and defined temporal ones. Experiments prove the significance of temporal attributes separation in web service selection and duties.

Non functional requirements are very interesting specially in case of business relationships. In fact they are idioms of communication between business environment parties: provider and consumer. In particular in web services context, these requirements and non functional characteristics are also seen as a ranking and selection criteria. Thus, many researchers propose tools to measure the quality of service value of web services and define scoring formulas to rank them. However, we strongly deem that a web service has relative scores depending on end-user requirements rather than an absolute score. In this research paper, we propose a mean for the client to specify his non functional constraints. These, as well as quality attributes measurements will present inputs of a newly developed scoring web service. This web service computes the score of a web service in request relatively to the client's non functional specifications. In addition, a two level ranking is provided to help the client make the suitable decision especially in case of equal scores.

The Web services orchestration is a useful and complicated approach to integrate heterogeneous systems. To verify the conformance of the orchestrated Web service against the intended behavior, we need to analyse the produced system. To this end, in this paper, we define a security framework namely MoWS (Monitoring as a Web service) for monitoring orchestrated web services by inlining, statically, monitor's web service calls, at some critical points of the program, that checks whether the program adheres to some constraints dictated by a security policy. The rewritten program behaves like the original one except that it is aborted when an action is about to violate a security policy. The described approach is supported by a Java plug-in for eclipse.

This paper is about conformance testing of non-deterministic timed pushdown automata (TPAIO), with urgency modelled as deadlines put on the transitions. The deadlines impose time progress conditions (TPC) on the locations of the TPAIO. In addition to detecting non conform or out of the time limits outputs of an implementation, our tests also detect TPC violations. Our method proceeds by a one-clock determinization of the TPAIO, followed by the computation of a reach ability automaton aiming at covering the reachable transitions and locations of the TPAIO, w.r.t. the stack constraints. Each RA transition records an execution path of the TPAIO. To get the tests, we add to these execution paths the fail verdicts issued from the determinization. Their ability to detect non conform implementation is assessed by mutation: altered implementations are automatically generated from a specification by application of some mutation operators that we define.

Modelling Online Social Networks (OSNs) can be very useful to study many concepts such as viral marketing, human behaviour or information propagation. Most existing studies on OSNs are based on models that are outdated and do not reflect the reality of the structure and characteristics of OSNs. In this paper, we present a new model that represents OSNs more accurately. Facebook being currently the most used Online Social Network in the world, we give its model as an example.

This paper is about conformance testing of non deterministic timed pushdown automata with inputs and outputs (TPAIO), that specify both stack and clock constraints. It proposes a novel off-line test generation method from this model. The first step computes a deterministic timed pushdown tester with inputs and outputs (DTPTIO): a TPAIO which approximates the initial TPAIO with only one clock. Then we compute from the DTPTIO a finite reach ability automaton (RA), whose transitions are related to DTPTIO paths satisfying the stack constraints. This computation takes the DTPTIO transitions as a coverage criterion. The RA transitions, thus the DTPTIO paths, are used for generating test cases that aim at covering the reachable locations and transitions of the TPAIO. The test cases are in the shape of trees equipped with verdicts. Last, we propose a mutation testing method from non-deterministic TPAIO to evaluate the efficiency of our method.

SUMMARY Noninterference is a strong security policy that enforces confidentiality and integrity. Many solutions are proposed in the state of the art for verifying this policy in programs, but few tools are proposed to implement it. In this paper, we define a high‐level model called Component Information Flow, and we develop the tools that simplify distributed secure system development and deployment. The developer focuses on developing the functional part of his or her system and defines his or her system security properties by using a high‐level configuration. When this configuration is validated, that is, no security leak is detected, the system security code is generated. To validate and demonstrate the effectiveness of our approach, we apply the Component Information Flow tools to a classical Web service use case. Copyright © 2012 John Wiley & Sons, Ltd.

Timestamping [1] is a cryptographic technique for adding a reliable date to a document in order to prove its existence at a given time. Several solutions of timestamping exist. They are all based on cryptographic techniques as digital signatures and hash functions. However, with the increase of computing power and the evolution of cryptanalysis methods, cryptography becomes more and more the target of criticism. That's why we need new directions and orientations for timestamping techniques. One of these directions was introduced in [2] and dealt with non interactive timestamping solutions in the Bounded Storage Model. In the Bounded Storage Model, we make the hypothesis that user's storage capacity is bounded but user's computing power is unlimited. In this paper, we first present the existing timestamping systems. Then we introduce the Bounded Storage Model. Finally, we present a new timestamping schema that we have conceived in the bounded storage model.