Biblio

Supervisory control and data acquisition (SCADA) systems are used with monitoring and control purposes for the process not to fail in industrial control systems. Today, the increase in the use of standard protocols, hardware, and software in the SCADA systems that can connect to the internet and institutional networks causes these systems to become a target for more cyber-attacks. Intrusion detection systems are used to reduce or minimize cyber-attack threats. The use of deep learning-based intrusion detection systems also increases in parallel with the increase in the amount of data in the SCADA systems. The unsupervised feature learning present in the deep learning approaches enables the learning of important features within the large datasets. The features learned in an unsupervised way by using deep learning techniques are used in order to classify the data as normal or abnormal. Architectures such as convolutional neural network (CNN), Autoencoder (AE), deep belief network (DBN), and long short-term memory network (LSTM) are used to learn the features of SCADA data. These architectures use softmax function, extreme learning machine (ELM), deep belief networks, and multilayer perceptron (MLP) in the classification process. In this study, anomaly-based intrusion detection systems consisting of convolutional neural network, autoencoder, deep belief network, long short-term memory network, or various combinations of these methods on the SCADA networks in the literature were analyzed and the positive and negative aspects of these approaches were explained through their attack detection performances.

In today’s world, Supervisory Control and Data Acquisition (SCADA) networks have many critical tasks, including managing infrastructure such as power, water, and sewage systems, and controlling automated manufacturing and transportation systems. Securing these systems is crucial. Here we describe a project to design security into an example system using formal specifications. Our example system is a component in a cybersecurity testbed at the University of Cincinnati, which was described in previous work. We also show how a design flaw can be discovered and corrected early in the system development process.

High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance. This mismatch, combined with the high-profile Spectre-style attacks that exploit speculative execution, naturally casts doubts on the robustness of high-assurance cryptography guarantees. In this paper, we dispel these doubts by showing that the benefits of high-assurance cryptography extend to speculative execution, costing only a modest performance overhead. We build atop the Jasmin verification framework an end-to-end approach for proving properties of cryptographic software under speculative execution, and validate our approach experimentally with efficient, functionally correct assembly implementations of ChaCha20 and Poly1305, which are secure against both traditional timing and speculative execution attacks.

The utilization of "cloud storage services (CSS)", empowering people to store their data in cloud and avoid from maintenance cost and local data storage. Various data integrity auditing (DIA) frameworks are carried out to ensure the quality of data stored in cloud. Mostly, if not all, of current plans, a client requires to utilize his private key (PK) to generate information authenticators for knowing the DIA. Subsequently, the client needs to have hardware token to store his PK and retain a secret phrase to actuate this PK. In this hardware token is misplaced or password is forgotten, the greater part of existing DIA plans would be not able to work. To overcome this challenge, this research work suggests another DIA without "private key storage (PKS)"plan. This research work utilizes biometric information as client's fuzzy private key (FPK) to evade utilizing hardware token. In the meantime, the plan might in any case viably complete the DIA. This research work uses a direct sketch with coding and mistake correction procedures to affirm client identity. Also, this research work plan another mark conspire that helps block less. Verifiability, yet in addition is viable with linear sketch Keywords– Data integrity auditing (DIA), Cloud Computing, Block less Verifiability, fuzzy biometric data, secure cloud storage (SCS), key exposure resilience (KER), Third Party Auditor (TPA), cloud audit server (CAS), cloud storage server (CSS), Provable Data Possession (PDP)

In order to protect user privacy and provide better access control in Internet of Things (IoT) environments, designing an appropriate two-party authentication and key exchange protocol is a prominent challenge. In this paper, we propose a lightweight certificateless non-interactive authentication and key exchange (CNAKE) protocol for mutual authentication between remote users and smart devices. Based on elliptic curves, our lightweight protocol provides high security performance, realizes non-interactive authentication between the two entities, and effectively reduces communication overhead. Under the random oracle model, the proposed protocol is provably secure based on the Computational Diffie-Hellman and Bilinear Diffie-Hellman hardness assumption. Finally, through a series of experiments and comprehensive performance analysis, we demonstrate that our scheme is fast and secure.

Modern digital signature schemes can provide more guarantees than the standard notion of (strong) unforgeability, such as offering security even in the presence of maliciously generated keys, or requiring to know a message to produce a signature for it. The use of signature schemes that lack these properties has previously enabled attacks on real-world protocols. In this work we revisit several of these notions beyond unforgeability, establish relations among them, provide the first formal definition of non re-signability, and a transformation that can provide these properties for a given signature scheme in a provable and efficient way.Our results are not only relevant for established schemes: for example, the ongoing NIST PQC competition towards standardizing post-quantum signature schemes has six finalists in its third round. We perform an in-depth analysis of the candidates with respect to their security properties beyond unforgeability. We show that many of them do not yet offer these stronger guarantees, which implies that the security guarantees of these post-quantum schemes are not strictly stronger than, but instead incomparable to, classical signature schemes. We show how applying our transformation would efficiently solve this, paving the way for the standardized schemes to provide these additional guarantees and thereby making them harder to misuse.

The globalized supply chain in the semiconductor industry raises several security concerns such as IC overproduction, intellectual property piracy and design tampering. Logic locking has emerged as a Design-for-Trust countermeasure to address these issues. Original logic locking proposals provide a high degree of output corruption – i.e., errors on circuit outputs – unless it is unlocked with the correct key. This is a prerequisite for making a manufactured circuit unusable without the designer’s intervention. Since the introduction of SAT-based attacks – highly efficient attacks for retrieving the correct key from an oracle and the corresponding locked design – resulting design-based countermeasures have compromised output corruption for the benefit of better resilience against such attacks. Our proposed logic locking scheme, referred to as SKG-Lock, aims to thwart SAT-based attacks while maintaining significant output corruption. The proposed provable SAT-resilience scheme is based on the novel concept of decoy key-inputs. Compared with recent related works, SKG-Lock provides higher output corruption, while having high resistance to evaluated attacks.

Cloud storage technology enables users to outsource local data to cloud service provider (CSP). In spite of its copious advantages, how to ensure the integrity of data has always been a significant issue. A variety of provable data possession (PDP) scheme have been proposed for cloud storage scenarios. However, the participation of centralized trusted third-party auditor (TPA) in most of the previous work has brought new security risks, because the TPA is prone to the single point of failure. Furthermore, the existing schemes do not consider the fair arbitration and lack an effective method to punish the malicious behavior. To address the above challenges, we propose a novel blockchain-based decentralized data integrity auditing scheme without the need for a centralized TPA. By using smart contract technique, our scheme supports automatic compensation mechanism. DO and CSP must first pay a certain amount of ether for the smart contract as deposit. The CSP gets the corresponding storage fee if the integrity auditing is passed. Otherwise, the CSP not only gets no fee but has to compensate DO whose data integrity is destroyed. Security analysis shows that the proposed scheme can resist a variety of attacks. Also, we implement our scheme on the platform of Ethereum to demonstrate the efficiency and effectiveness of our scheme.

In this paper, we propose a new provably secure cryptosystem for two party communication that provides security in the face of new technological breakthroughs. Most of the practical cryptosystems in use today can be breached in the future with new sophisticated methods. This jeopardizes the security of older but highly confidential messages. Our protocol is based on the bounded storage model first introduced in [1]. The protocol is secure as long as there is bound on the storage, however large it may be. We also suggest methods to extend the protocol to unbounded storage models where access to adversary is limited. Our protocol is a substantial improvement over previously known protocols and uses short key and optimal number of public random bits size of which is independent of message length. The smaller and constant length of key and public random string makes the scheme more practical. The protocol generates key using elements of the additive group \$\textbackslashtextbackslashmathbbZ\_\textbackslashtextbackslashmathrmn\$. Our protocol is very generalized and the protocol in [1] is a special case of our protocol. Our protocol is a step forward in making provably secure cryptosystems practical. An important open problem raised in [2] was designing an algorithm with short key and size of public random string \$O(\textbackslashtextbackslashmathcalB)\$ where \$\textbackslashtextbackslashmathcalB\$ bounds the storage of adversary. Our protocol satisfies the conditions and is easy to implement.

The 5G technology brings the substantial improvement on the quality of services (QoS), such as higher throughput, lower latency, more stable signal and more ultra-reliable data transmission, triggering a revolution for the wireless mobile network. But in a general traffic channel in the 5G-based wireless mobile network, an attacker can detect a message transmitted over a channel, or even worse, forge or tamper with the message. Building a secure channel over the two parties is a feasible solution to this uttermost data transmission security challenge in 5G-based wireless mobile network. However, how to authentication the identities of the both parties before establishing the secure channel to fully ensure the data confidentiality and integrity during the data transmission has still been a open issue. To establish a fully secure channel, in this paper, we propose a strongly secure pairing-free certificateless authenticated key agreement (PF-CL-AKA) protocol with two-way identity-based authentication before extracting the secure session key. Our protocol is provably secure in the Lippold model, which means our protocol is still secure as long as each party of the channel has at least one uncompromised partial private term. Finally, By the theoretical analysis and simulation experiments, we can observe that our scheme is practical for the real-world applications in the 5G-based wireless mobile network.

To improve efficiency of stegosystem on blockchain and balance the time consumption of Encode and Decode operations, we propose a new blockchain-based steganography scheme, called Keys as Secret Messages (KASM), where a codebook of mappings between bitstrings and public keys can be pre-calculated by both sides with some secret parameters pre-negotiated before covert communication. By applying properties of elliptic curves and pseudorandom number generators, we realize key derivation of codebook item, and we construct the stegosystem with provable security under chosen hiddentext attack. By comparing KASM with Blockchain Covert Channel (BLOCCE) and testing on Bitcoin protocol, we conclude that our proposed stegosystem encodes hiddentexts faster than BLOCCE does and can decode stegotexts in highly acceptable time. The balanced time consumption of Encode and Decode operations of KASM make it applicable in the scene of duplex communication. At the same time, KASM does not leak sender’s private keys, so sender’s digital currencies can be protected.

A standard requirement for a signature scheme is that it is existentially unforgeable under chosen message attacks (EUF-CMA), alongside other properties of interest such as strong unforgeability (SUF-CMA), and resilience against key substitution attacks.Remarkably, no detailed proofs have ever been given for these security properties for EdDSA, and in particular its Ed25519 instantiations. Ed25519 is one of the most efficient and widely used signature schemes, and different instantiations of Ed25519 are used in protocols such as TLS 1.3, SSH, Tor, ZCash, and WhatsApp/Signal. The differences between these instantiations are subtle, and only supported by informal arguments, with many works assuming results can be directly transferred from Schnorr signatures. Similarly, several proofs of protocol security simply assume that Ed25519 satisfies properties such as EUF-CMA or SUF-CMA.In this work we provide the first detailed analysis and security proofs of Ed25519 signature schemes. While the design of the schemes follows the well-established Fiat-Shamir paradigm, which should guarantee existential unforgeability, there are many side cases and encoding details that complicate the proofs, and all other security properties needed to be proven independently.Our work provides scientific rationale for choosing among several Ed25519 variants and understanding their properties, fills a much needed proof gap in modern protocol proofs that use these signatures, and supports further standardisation efforts.

Clustering artworks is difficult for several reasons. On the one hand, recognizing meaningful patterns in accordance with domain knowledge and visual perception is extremely difficult. On the other hand, applying traditional clustering and feature reduction techniques to the highly dimensional pixel space can be ineffective. To address these issues, we propose to use a deep convolutional embedding model for digitized painting clustering, in which the task of mapping the raw input data to an abstract, latent space is jointly optimized with the task of finding a set of cluster centroids in this latent feature space. Quantitative and qualitative experimental results show the effectiveness of the proposed method. The model is also capable of outperforming other state-of-the-art deep clustering approaches to the same problem. The proposed method can be useful for several art-related tasks, in particular visual link retrieval and historical knowledge discovery in painting datasets.

This paper presents an IoT enabled real time occupancy semantic search system leveraging ETSI defined context information and interface meta model standard- ``Next Generation Service Interface for Linked Data'' (NGSI-LD). It facilitates interoperability, integration and federation of information exchange related to spatial infrastructure among geo-distributed deployed IoT entities, different stakeholders, and process domains. This system, in the presented use case, solves the problem of adhoc booking of meetings in real time through semantic discovery of spatial data and metadata related to room occupancy and thus enables optimum utilization of spatial infrastructure in university campuses. Therefore, the proposed system has the capability to save on effort, cost and productivity in institutional spatial management contexts in the longer run and as well provide a new enriched user experience in smart public buildings. Additionally, the system empowers different stakeholders to plan, forecast and fulfill their spatial infrastructure requirements through semantic data search analysis and real time data driven planning. The initial performance results of the system have shown quick response enabled semantic discovery of data and metadata (textless2 seconds mostly). The proposed system would be a steppingstone towards smart management of spatial infrastructure which offers scalability, federation, vendor agnostic ecosystem, seamless interoperability and integration and security by design. The proposed system provides the fundamental work for its extension and potential in relevant spatial domains of the future.

Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.

Today's Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol's authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.

Controller area network is the serial communication protocol, which broadcasts the message on the CAN bus. The transmitted message is read by all the nodes which shares the CAN bus. The message can be eavesdropped and can be re-used by some other node by changing the information or send it by duplicate times. The message reused after some delay is replay attack. In this paper, the CAN network with three CAN nodes is implemented using the universal verification components and the replay attack is demonstrated by creating the faulty node. Two types of replay attack are implemented in this paper, one is to replay the entire message and the other one is to replay only the part of the frame. The faulty node uses the first replay attack method where it behaves like the other node in the network by duplicating the identifier. CAN frame except the identifier is reused in the second method which is hard to detect the attack as the faulty node uses its own identifier and duplicates only the data in the CAN frame.

Mobile payment protocols have attracted widespread attention over the past decade, due to advancements in digital technology. The use of these protocols in online industries can dramatically improve the quality of online services. However, the central issue of concern when utilizing these types of systems is their accountability, which ensures trust between the parties involved in payment transactions. It is, therefore, vital for researchers to investigate how to handle the accountability of mobile payment protocols. In this research, we introduce a secure mobile payment protocol to overcome this problem. Our payment protocol combines all the necessary security features, such as confidentiality, integrity, authentication, and authorization that are required to build trust among parties. In other words, is the properties of mutual authentication and non-repudiation are ensured, thus providing accountability. Our approach can resolve any conflicts that may arise in payment transactions between parties. To prove that the proposed protocol is correct and complete, we use the Scyther and AVISPA tools to verify our approach formally.

UPI (Unified Payments Interface) is a framework in India wherein customers can send payments to merchants from their smartphones. The framework consists of UPI servers that are connected to the banks at the sender and receiver ends. To send and receive payments, customers and merchants would have to first register themselves with UPI servers by executing a registration protocol using payment apps such as BHIM, PayTm, Google Pay, and PhonePe. Weaknesses were recently reported on these protocols that allow attackers to make money transfers on behalf of innocent customers and even empty their bank accounts. But the reported weaknesses were found after informal and manual analysis. However, as history has shown, formal analysis of cryptographic protocols often reveals flaws that could not be discovered with manual inspection. In this paper, we model UPI protocols in the pattern of traditional cryptographic protocols such that they can be rigorously studied and analyzed using formal methods. The modeling simplifies many of the complexities in the protocols, making it suitable to analyze and verify UPI protocols with popular analysis and verification tools such as the Constraint Solver, ProVerif and Tamarin. Our modeling could also be used as a general framework to analyze and verify many other financial payment protocols than just UPI protocols, giving it a broader applicability.

In the era of big data and artificial intelligence, computer networks have become an important infrastructure, and the Internet has become ubiquitous. The most basic property of computer networks is reachability. The needs of the modern Internet mainly include cost, performance, reliability, and security. However, even for experienced network engineers, it is very difficult to manually conFigure the network to meet the needs of the modern large-scale Internet. The engineers often make mistakes, which can cause network paralysis, resulting in incalculable losses. Due to the development of automatic reasoning technology, automatic verification of network configuration is used to avoid mistakes. Network verification is at least an NP-C problem, so it is necessary to compress the network to reduce the network scale, thereby reducing the network verification time. This paper proposes a new model of network modeling, which is more suitable for the verification of network configuration on common protocols (such as RIP, BGP). On the basis of the existing compression method, two compression rules are added to compress the modeled network, reducing network verification time and conducting network reachability verification experiments on common networks. The experimental results are slightly better than the current compression methods.

This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature.

Given the central importance of designing secure protocols, providing solid mathematical foundations and computer-assisted methods to attest for their correctness is becoming crucial. Here, we elaborate on the formal approach introduced by Bana and Comon in [10], [11], which was originally designed to analyze protocols for a fixed number of sessions, and lacks support for proof mechanization.In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model. More specifically, we develop a meta-logic as well as a proof system for deriving security properties. Proofs in our system only deal with high-level, symbolic representations of protocol executions, similar to proofs in the symbolic model, but providing security guarantees at the computational level. We have implemented our approach within a new interactive prover, the Squirrel prover, taking as input protocols specified in the applied pi-calculus, and we have performed a number of case studies covering a variety of primitives (hashes, encryption, signatures, Diffie-Hellman exponentiation) and security properties (authentication, strong secrecy, unlinkability).

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model

Ad Hoc Network is wireless networks that get more attention from past to present. Mobile ad hoc network (MANET) is one of the types of ad hoc networks, it deployed rapidly because it infrastructure-less. A node in a mobile ad hoc network communicates through wireless links without wired channels. When source nodes want to communicate with the destination outside its transmission range it uses multi-hop mechanisms. The intermediate node forwards the data packet to the next node until the data packet reaches its destination. Due wireless links and lack of centralized administration device, mobile ad hoc network is more vulnerable for security attacks. The rushing attack is one of the most dangerous attacks in the on-demand routing protocol of mobile ad hoc networks. Rushing attack highly transmits route request with higher transmission power than the genuine nodes and become participate between source and destination nodes, after that, it delays or drop actual data pass through it. In this study, the researcher incorporates rushing attack in one of the most commonly used mobile ad hoc network routing protocols namely Ad hoc on-demand multipath distance vector and provides a rushing attack prevention method based on the time threshold value and random route selection. Based on the time RREQ arrives a node takes a decision, if the RREQ packet arrives before threshold value, the RREQ packet consider as came from an attacker and discarded else RREQ packet received then randomly select RREQ to forward. In this study performance metrics like packet delivery ratio, end-to-end delay and throughput have been evaluated using Network simulation (NS-2.35). As a result of simulation shows newly proposed prevention mechanism improves network performance in all cases than the network under attacker. For example, the average packet delivery ratio enhanced from 54.37% to 97.69%, throughput increased from 20.84bps to 33.06bpsand the average delay decreased from 1147.22ms to 908.04ms. It is concluded that the new proposed techniques show improvement in all evaluated performance metrics.