Biblio

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

We present a formal OpenFlow-based network programming language (OF) including various flow rules, which can not only describe the behaviors of an individual switch, but also support to model a network of switches connected in the point-to-point topology. Besides, a topology-oriented operational semantics of the proposed language is explored to specify how the packet is processed and delivered in the OpenFlow-based networks. Based on the formal framework, we also propose an approach to detect potential security threats caused by the conflict of dynamic flow rules imposed by dynamic OpenFlow applications.

With the development of IoT, smart health has significantly improved the quality of people's life. A large amount of smart health monitoring system has been proposed, which provides an opportunity for timely and efficient diagnosis. Nevertheless, most of them ignored the impact of environment on patients' health. Due to the openness of the communication channel, data security and privacy preservation are crucial problems to be solved. In this work, an environment aware privacy-preserving authentication protocol based on the fuzzy extractor and elliptic curve cryptography (ecc) is designed for health monitoring system with mutual authentication and anonymity. Edge computing unit can authenticate all environmental sensors at one time. Fuzzy synthetic evaluation model is utilized to evaluate the environment equality with the patients' temporal health index (THI) as an assessment factor, which can help to predict the appropriate environment. The session key is established for secure communication based on the predicted result. Through security analysis, the proposed protocol can prevent common attacks. Moreover, performance analysis shows that the proposed protocol is applicable for resource-limited smart devices in edge computing health monitoring system.

In this paper, we propose an exact closed-form expression of secrecy outage probability (SOP) for underlay cognitive network with energy scavenging capable relay over Nakagami-m fading channels and under both (maximum transmit and interference) power constraints. Various results validated the proposed expression and shed insights into the security performance of this network in key specifications.

We present a security analysis of several gesture CAPTCHA challenges designed to operate on mobiles. Mobile gesture CAPTCHA challenges utilize the accelerometer and the gyroscope inputs from a mobile to allow a human to solve a simple test by physically manipulating the device. We have evaluated the security of gesture CAPTCHA in mobile devices and found them resistant to a range of common automated attacks. Our study has shown that using an accelerometer and the gyroscope readings as an input to solve the CAPTCHA is difficult for malware, but easy for a real user. Gesture CAPTCHA is effective in differentiating between humans and machines.

The purpose of this paper is to improve the safety of chaotic image encryption algorithm. Firstly, to achieve this goal, it put forward two improved chaotic system logistic and henon, which covered an promoted henon chaotic system with better probability density, and an 2-dimension logistic chaotic system with high Lyapunov exponents. Secondly, the chaotic key stream was generated by the new 2D logistic chaotic system and optimized henon mapping, which mixed in dynamic proportions. The conducted sequence has better randomness and higher safety for image cryptosystem. Thirdly, we proposed algorithm takes advantage of the compounded chaotic system Simulation experiment results and security analysis showed that the proposed scheme was more effective and secure. It can resist various typical attacks, has high security, satisfies the requirements of image encryption theoretical.

The security of logic locking has been called into question by various attacks, especially a Boolean satisfiability (SAT) based attack, that exploits scan access in a working chip. Among other techniques, a robust design-for-security (DFS) architecture was presented to restrict any unauthorized scan access, thereby, thwarting the SAT attack (or any other attack that relies on scan access). Nevertheless, in this work, we successfully break this technique by recovering the secret key despite the lack of scan access. Our security analysis on a few benchmark circuits protected by the robust DFS architecture demonstrates the effectiveness of our attack; on average 95% of the key bits are correctly recovered, and almost 100% in most cases. To overcome this and other prevailing attacks, we propose a defense by making fundamental changes to the robust DFS technique; the new defense can withstand all logic locking attacks. We observe, on average, lower area overhead ( 1.65%) than the robust DFS design ( 5.15%), and similar test coverage ( 99.88%).

We present TendrilStaller, an eclipse attack targeting at Bitcoin's peer-to-peer network. TendrilStaller enables an adversary to delay block propagation to a victim for 10 minutes. The adversary thus impedes the victim from getting the latest blockchain state. It only takes as few as one Bitcoin full node and two light weight nodes to perform the attack. The light weight nodes perform a subset of the functions of a full Bitcoin node. The attack exploits a recent block propagation protocol introduced in April 2016. The protocol prescribes a Bitcoin node to select 3 neighbors that can send new blocks unsolicited. These neighbors are selected based on their recent performance in providing blocks quickly. The adversary induces the victim to select 3 attack nodes by having attack nodes send valid blocks to the victim more quickly than other neighbors. For this purpose, the adversary deploys a handful of light weight nodes so that the adversary itself receives new blocks faster. The adversary then performs the attack to delay blocks propagated to the victim. We implement the attack on top of current default Bitcoin protocol We deploy the attack nodes in multiple locations around the globe and randomly select victim nodes. Depending on the round-trip time between the adversary and the victim, 50%-85% of the blocks could be delayed to the victim. We further show that the adoption of light weight nodes greatly increases the attack probability by 15% in average. Finally, we propose several countermeasures to mitigate this eclipse attack.

In this work, we perform security analysis of using an e-mail as a self-service password reset point, and exploit some of the vulnerabilities of e-mail servers' forgotten password reset paths. We perform and illustrate three different attacks on a personal Email account, using a variety of tools such as: public knowledge attainable through social media or public records to answer security questions and execute a social engineering attack, hardware available to the public to perform a man in the middle attack, and free software to perform a brute-force attack on the login of the email account. Our results expose some of the inherent vulnerabilities in using emails as password reset points. The findings are extremely relevant to the security of mobile devices since users' trend has leaned towards usage of mobile devices over desktops for Internet access.

Big data will bring revolutionary changes from life to thinking for society as a whole. At the same time, the massive data and potential value of big data are subject to many security risks. Aiming at the above problems, a data privacy protection model for big data platform is proposed. First, the data privacy protection model of big data for data owners is introduced in detail, including protocol design, logic design, complexity analysis and security analysis. Then, the query privacy protection model of big data for ordinary users is introduced in detail, including query protocol design and query mode design. Complexity analysis and safety analysis are performed. Finally, a stand-alone simulation experiment is built for the proposed privacy protection model. Experimental data is obtained and analyzed. The feasibility of the privacy protection model is verified.

To improve production efficiency, more industrial control systems are connected to IT networks, and more IT technologies are applied to industrial control networks, network security has become an important problem. Industrial control network security analysis and decision-making is a effective method to solve the problem, which can predict risks and support to make decisions before the actual fault of the industrial control network system has not occurred. This paper proposes a security analysis and decision-making method with forward reasoning based on strong relevant logic for industrial control networks. The paper presents a case study in security analysis and decision-making for industrial control networks. The result of the case study shows that the proposed method is effective.

Organizations perform security analysis for assessing network health and safe-guarding their growing networks through Vulnerability Assessments (AKA VA Scans). The output of VA scans is reports on individual hosts and its vulnerabilities, which, are of little use as the origin of the attack can't be located from these. Attack Graphs, generated without an in-depth analysis of the VA reports, are used to fill in these gaps, but only provide cursory information. This study presents an effective model of depicting the devices and the data flow that efficiently identifies the weakest nodes along with the concerned vulnerability's origin.The complexity of the attach graph using MulVal has been greatly reduced using the proposed approach of using the risk and CVSS base score as evaluation criteria. This makes it easier for the user to interpret the attack graphs and thus reduce the time taken needed to identify the attack paths and where the attack originates from.

With the development of cloud computing technology in the Internet of Things (IoT), the trajectory privacy in location-based services (LBSs) has attracted much attention. Most of the existing work adopts point-to-point and centralized models, which will bring a heavy burden to the user and cause performance bottlenecks. Moreover, previous schemes did not consider both online and offline trajectory protection and ignored some hidden background information. Therefore, in this paper, we design a trajectory protection scheme based on fog computing and k-anonymity for real-time trajectory privacy protection in continuous queries and offline trajectory data protection in trajectory publication. Fog computing provides the user with local storage and mobility to ensure physical control, and k-anonymity constructs the cloaking region for each snapshot in terms of time-dependent query probability and transition probability. In this way, two k-anonymity-based dummy generation algorithms are proposed, which achieve the maximum entropy of online and offline trajectory protection. Security analysis and simulation results indicate that our scheme can realize trajectory protection effectively and efficiently.

Vehicular ad hoc networks (VANETs) have been growing rapidly because it can improve traffic safety and efficiency in transportation. In VANETs, messages are broadcast in wireless environment, which is vulnerable to be attacked in many ways. Accordingly, it is essential to authenticate the legitimation of vehicles to guarantee the performance of services. In this paper, we propose an anonymous conditional privacy-preserving authentication scheme based on message authentication code (MAC) for VANETs. With verifiable secret sharing (VSS), vehicles can obtain a group key for message generation and authentication after a mutual authentication phase. Security analysis and performance evaluation show that the proposed scheme satisfies basic security and privacy-preserving requirements and has a better performance compared with some existing schemes in terms of computational cost and communication overhead.

Securing multi-party communication is very challenging particularly in dynamic networks. Existing multi-recipient cryptographic schemes pose variety of limitations. These include: requiring trust among all recipients to make an agreement, high computational cost for both encryption and decryption, and additional communication overhead when group membership changes. To overcome these limitations, this paper introduces a novel multi-recipient asymmetric cryptographic scheme, AMOUN. This scheme enables the sender to possibly send different messages in one ciphertext to multiple recipients to better utilize network resources, while ensuring that each recipient only retrieves its own designated message. Security analysis demonstrates that proposed scheme is secure against well-known attacks. Evaluation results demonstrate that lightweight AMOUN outperforms RSA and Multi-RSA in terms of computational cost for both encryption and decryption. For a given prime size, in case of encryption, AMOUN achieves 86% and 98% lower average computational cost than RSA and Multi-RSA, respectively; while for decryption, it shows performance improvement of 98% compared to RSA and Multi-RSA.

The Internet of Things (IoT) is a new paradigm in which every-day objects are interconnected between each other and to the Internet. This paradigm is receiving much attention of the scientific community and it is applied in many fields. In some applications, it is useful to prove that a number of objects are simultaneously present in a group. For example, an individual might want to authorize NFC payment with his mobile only if k of his devices are present to ensure that he is the right person. This principle is known as Grouping-Proofs. However, existing Grouping-Proofs schemes are mostly designed for RFID systems and don't fulfill the IoT characteristics. In this paper, we propose a Threshold Grouping-Proofs for IoT applications. Our scheme uses the Key-Policy Attribute-Based Encryption (KP-ABE) protocol to encrypt a message so that it can be decrypted only if at least k objects are simultaneously present in the same location. A security analysis and performance evaluation is conducted to show the effectiveness of our proposal solution.

IoT-based services are widely increasing due to their advantages such as economy, automation, and comfort. Smart cities are among major applications of IoT-based systems. However, security and privacy threats are vital issues challenging the utilization of such services. Connectivity nature, variety of data technology, and volume of data maintained through these systems make their security analysis a difficult process. Threat modeling is one the best practices for security analysis, especially for complex systems. This paper proposes a threat extraction method for IoT-based systems. We elaborate on a smart city scenario with three services including lighting, car parking, and waste management. Investigating on these services, firstly, we identify thirty-two distinct threat types. Secondly, we distinguish threat root causes by associating a threat to constituent parts of the IoT-based system. In this way, threat instances can be extracted using the proposed derivation rules. Finally, we evaluate our method on a smart car parking scenario as well as on an E-Health system and identify more than 50 threat instances in each cases to show that the method can be easily generalized for other IoT-based systems whose constituent parts are known.

The real-time map updating enables vehicles to obtain accurate and timely traffic information. Especially for driverless cars, real-time map updating can provide high-precision map service to assist the navigation, which requires vehicles to actively upload the latest road conditions. However, due to the untrusted network environment, it is difficult for the real-time map updating server to evaluate the authenticity of the road information from the vehicles. In order to prevent malicious vehicles from deliberately spreading false information and protect the privacy of vehicles from tracking attacks, this paper proposes a trust-based real-time map updating scheme. In this scheme, the public key is used as the identifier of the vehicle for anonymous communication with conditional anonymity. In addition, the blockchain is applied to provide the existence proof for the public key certificate of the vehicle. At the same time, to avoid the spread of false messages, a trust evaluation algorithm is designed. The fog node can validate the received massages from vehicles using Bayesian Inference Model. Based on the verification results, the road condition information is sent to the real-time map updating server so that the server can update the map in time and prevent the secondary traffic accident. In order to calculate the trust value offset for the vehicle, the fog node generates a rating for each message source vehicle, and finally adds the relevant data to the blockchain. According to the result of security analysis, this scheme can guarantee the anonymity and prevent the Sybil attack. Simulation results show that the proposed scheme is effective and accurate in terms of real-time map updating and trust values calculating.

Cyber-physical systems (CPS) are state-of-the-art communication environments that offer various applications with distinct requirements. However, security in CPS is a nonnegotiable concept, since without a proper security mechanism the applications of CPS may risk human lives, the privacy of individuals, and system operations. In this paper, we focus on PHY-layer security approaches in CPS to prevent passive eavesdropping attacks, and we propose an integration of physical layer operations to enhance security. Thanks to the McEliece cryptosystem, error injection is firstly applied to information bits, which are encoded with the forward error correction (FEC) schemes. Golay and Hamming codes are selected as FEC schemes to satisfy power and computational efficiency. Then obtained codewords are transmitted across reliable intermediate relays to the legitimate receiver. As a performance metric, the decoding frame error rate of the eavesdropper is analytically obtained for the fragmentary existence of significant noise between relays and Eve. The simulation results validate the analytical calculations, and the obtained results show that the number of low-quality channels and the selected FEC scheme affects the performance of the proposed model.

Although Vehicle Named Data Network (VNDN) possess the communication benefits of Named Data Network and Vehicle Opportunity Network, it also introduces some new privacy problems, including the identity security of Data Requesters and Data Providers. Data providers in VNDN need to sign data packets directly, which will leak the identity information of the providers, while the vicinity malicious nodes can access the sensitive information of Data Requesters by analyzing the relationship between Data Requesters and the data names in Interest Packages that are sent directly in plaintext. In order to solve the above privacy problems, this paper presents an identity privacy protection strategy for Data Requesters and Data Providers in VNDN. A ring signature scheme is used to hide the correlation between the signature and the data provider and the anonymous proxy idea is used to protect the real identity of the data requester in the proposed strategy. Security Analysis and experiments in the ONE-based VNDN platform indicate that the proposed strategy is effective and practical.

Cloud computing has become an important and popular infrastructure for data storage and sharing. Typically, data owners outsource their massive data to a public cloud that will provide search services to authorized data users. With privacy concerns, the valuable outsourced data cannot be exposed directly, and should be encrypted before outsourcing to the public cloud. In this paper, we focus on k-Nearest Neighbor (k-NN) search over encrypted data. We propose efficient and secure k-NN search schemes based on matrix similarity to achieve efficient and secure query services in public cloud. In our basic scheme, we construct the traces of two diagonal multiplication matrices to denote the Euclidean distance of two data points, and perform secure k-NN search by comparing traces of corresponding similar matrices. In our enhanced scheme, we strengthen the security property by decomposing matrices based on our basic scheme. Security analysis shows that our schemes protect the data privacy and query privacy under attacking with different levels of background knowledge. Experimental evaluations show that both schemes are efficient in terms of computation complexity as well as computational cost.

Modern vehicles in Intelligent Transportation Systems (ITS) can communicate with each other as well as roadside infrastructure units (RSUs) in order to increase transportation efficiency and road safety. For example, there are techniques to alert drivers in advance about traffic incidents and to help them avoid congestion. Threats to these systems, on the other hand, can limit the benefits of these technologies. Securing ITS itself is an important concern in ITS design and implementation. In this paper, we provide a security model of ITS which extends the classic layered network security model with transportation security and information security, and gives a reference for designing ITS architectures. Based on this security model, we also present a classification of ITS threats for defense. Finally a proof-of-concept example with malicious nodes in an ITS system is also given to demonstrate the impact of attacks. We analyzed the threat of malicious nodes and their effects to commuters, like increasing toll fees, travel distances, and travel times etc. Experimental results from simulations based on Veins shows the threats will bring about 43.40% more total toll fees, 39.45% longer travel distances, and 63.10% more travel times.

Software-Defined Networking (SDN) introduces a centralized network control and management by separating the data plane from the control plane which facilitates traffic flow monitoring, security analysis and policy formulation. However, it is challenging to choose a proper degree of traffic flow handling granularity while proactively protecting forwarding devices from getting overloaded. In this paper, we propose a novel traffic flow matching control framework called Q-DATA that applies reinforcement learning in order to enhance the traffic flow monitoring performance in SDN based networks and prevent traffic forwarding performance degradation. We first describe and analyse an SDN-based traffic flow matching control system that applies a reinforcement learning approach based on Q-learning algorithm in order to maximize the traffic flow granularity. It also considers the forwarding performance status of the SDN switches derived from a Support Vector Machine based algorithm. Next, we outline the Q-DATA framework that incorporates the optimal traffic flow matching policy derived from the traffic flow matching control system to efficiently provide the most detailed traffic flow information that other mechanisms require. Our novel approach is realized as a REST SDN application and evaluated in an SDN environment. Through comprehensive experiments, the results show that-compared to the default behavior of common SDN controllers and to our previous DATA mechanism-the new Q-DATA framework yields a remarkable improvement in terms of traffic forwarding performance degradation protection of SDN switches while still providing the most detailed traffic flow information on demand.

This paper introduces complex network into software clone detection and proposes a clone code detection method based on software complex network feature matching. This method has the following properties. It builds a software network model with many added features and codes written with different languages can be detected by a single method. It reduces the space of code comparison, and it searches similar subnetworks to detect clones without knowing any clone codes information. This method can be used in detecting open source code which has been reused in software for security analysis.

The increase of the digitalization taking place in various industrial domains is leading developers towards the design and implementation of more and more complex networked control systems (NCS) supported by Wireless Sensor Networks (WSN). This naturally raises new challenges for the current WSN technology, namely in what concerns improved guarantees of technical aspects such as real-time communications together with safe and secure transmissions. Notably, in what concerns security aspects, several cryptographic protocols have been proposed. Since the design of these protocols is usually error-prone, security breaches can still be exposed and MALICIOUSly exploited unless they are rigorously analyzed and verified. In this paper we formally verify, using ProVerif, three cryptographic protocols used in WSN, regarding the security properties of secrecy and authenticity. The security analysis performed in this paper is more robust than the ones performed in related work. Our contributions involve analyzing protocols that were modeled considering an unbounded number of participants and actions, and also the use of a hierarchical system to classify the authenticity results. Our verification shows that the three analyzed protocols guarantee secrecy, but can only provide authenticity in specific scenarios.