Biblio

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.

Existing Lipschitz-based provable defences to adversarial examples only cover the L2 threat model. We introduce the first bound that makes use of Lipschitz continuity to provide a more general guarantee for threat models based on any Lp norm. Additionally, a new strategy is proposed for designing network architectures that exhibit superior provable adversarial robustness over conventional convolutional neural networks. Experiments are conducted to validate our theoretical contributions, show that the assumptions made during the design of our novel architecture hold in practice, and quantify the empirical robustness of several Lipschitz-based adversarial defence methods.

The following topics are dealt with: learning (artificial intelligence); neural nets; feature extraction; pattern classification; convolutional neural nets; computer network security; security of data; recurrent neural nets; data privacy; and cloud computing.

Sometimes a security-critical decision must be made using information provided by peers. Think of routing messages, user reports, sensor data, navigational information, blockchain updates. Attackers manifest as peers that strategically report fake information. Trust models use the provided information, and attempt to suggest the correct decision. A model that appears accurate by empirical evaluation of attacks may still be susceptible to manipulation. For a security-critical decision, it is important to take the entire attack space into account. Therefore, we define the property of robustness: the probability of deciding correctly, regardless of what information attackers provide. We introduce the notion of realisations of honesty, which allow us to bypass reasoning about specific feedback. We present two schemes that are optimally robust under the right assumptions. The “majority-rule” principle is a special case of the other scheme which is more general, named “most plausible realisations”.

Industry is increasingly adopting Reinforcement Learning algorithms (RL) in production without thoroughly analyzing their security features. In addition to the potential threats that may arise if the functionality of these algorithms is compromised while in operation. One of the well-known RL algorithms is the Contextual Multi-Armed Bandit (CMAB) algorithm. In this paper, we explore how the CMAB can be used to solve the Link Adaptation problem - a well-known problem in the telecommunication industry by learning the optimal transmission parameters that will maximize a communication link's throughput. We analyze the potential vulnerabilities of the algorithm and how they may adversely affect link parameters computation. Additionally, we present a provable security assessment for the Contextual Multi-Armed Bandit Reinforcement Learning (CMAB-RL) algorithm in a network simulated environment using Ray. This is by demonstrating CMAB security vulnerabilities theoretically and practically. Some security controls are proposed for CMAB agent and the surrounding environment. In order to fix those vulnerabilities and mitigate the risk. These controls can be applied to other RL agents in order to design more robust and secure RL agents.

OAuth 2.0 is one of the most widely used Internet protocols for authorization/single sign-on (SSO) and is also the foundation of the new SSO protocol OpenID Connect. Due to its complexity and its flexibility, it is difficult to comprehensively analyze the security of the OAuth 2.0 standard, yet it is critical to obtain practical security guarantees for OAuth 2.0. In this paper, we present the first computationally sound security analysis of OAuth 2.0. First, we introduce a new primitive, the three-party authenticated secret distribution (3P-ASD for short) protocol, which plays the role of issuing the secret and captures the token issue process of OAuth 2.0. As far as we know, this is the first attempt to formally abstract the authorization technology into a general primitive and then define its security. Then, we present a sufficiently rich three-party security model for OAuth protocols, covering all kinds of authorization flows, providing reasonably strong security guarantees and moreover capturing various web features. To confirm the soundness of our model, we also identify the known attacks against OAuth 2.0 in the model. Furthermore, we prove that two main modes of OAuth 2.0 can achieve our desired security by abstracting the token issue process into a 3P-ASD protocol. Our analysis is not only modular which can reflect the compositional nature of OAuth 2.0, but also fine-grained which can evaluate how the intermediate parameters affect the final security of OAuth 2.0.

The prevalence and availability of cloud infrastructures has made them the de facto solution for storing and archiving data, both for organizations and individual users. Nonetheless, the cloud's wide spread adoption is still hindered by dependability and security concerns, particularly in applications with large data collections where efficient search and retrieval services are also major requirements. This leads to an increased tension between security, efficiency, and search expressiveness. In this paper we tackle this tension by proposing BISEN, a new provably-secure boolean searchable symmetric encryption scheme that improves these three complementary dimensions by exploring the design space of isolation guarantees offered by novel commodity hardware such as Intel SGX, abstracted as Isolated Execution Environments (IEEs). BISEN is the first scheme to support multiple users and enable highly expressive and arbitrarily complex boolean queries, with minimal information leakage regarding performed queries and accessed data, and verifiability regarding fully malicious adversaries. Furthermore, BISEN extends the traditional SSE model to support filter functions on search results based on generic metadata created by the users. Experimental validation and comparison with the state of art shows that BISEN provides better performance with enriched search semantics and security properties.

After several years of research on onion routing, Camenisch and Lysyanskaya, in an attempt at rigorous analysis, defined an ideal functionality in the universal composability model, together with properties that protocols have to meet to achieve provable security. A whole family of systems based their security proofs on this work. However, analyzing HORNET and Sphinx, two instances from this family, we show that this proof strategy is broken. We discover a previously unknown vulnerability that breaks anonymity completely, and explain a known one. Both should not exist if privacy is proven correctly.In this work, we analyze and fix the proof strategy used for this family of systems. After proving the efficacy of the ideal functionality, we show how the original properties are flawed and suggest improved, effective properties in their place. Finally, we discover another common mistake in the proofs. We demonstrate how to avoid it by showing our improved properties for one protocol, thus partially fixing the family of provably secure onion routing protocols.

Cyber incidents are occurring every day using various attack strategies. Deploying security solutions with strong configurations will reduce the attack surface and improve the forensic readiness, but will increase the security overhead and cost. In contrast, using moderate or low security configurations will reduce that overhead, but will inevitably decrease the investigation readiness. To avoid the use of cost-prohibitive approaches in developing forensic-ready systems, we present in this paper a game theoretic approach for deploying an investigation-ready infrastructure. The proposed game is a non-cooperative two-player game between an adaptive cyber defender that uses a cognitive security solution to increase the investigation readiness and reduce the attackers' untraceability, and a cyber attacker that wants to execute non-provable attacks with a low cost. The cognitive security solution takes its strategic decision, mainly based on its ability to make forensic experts able to differentiate between provable identifiable, provable non-identifiable, and non-provable attack scenarios, starting from the expected evidences to be generated. We study the behavior of the two strategic players, looking for a mixed Nash equilibrium during competition and computing the probabilities of attacking and defending. A simulation is conducted to prove the efficiency of the proposed model in terms of the mean percentage of gained security cost, the number of stepping stones that an attacker creates and the rate of defender false decisions compared to two different approaches.

Provable Data Possession (PDP) is one of the data security techniques to make sure that the data stored in the cloud storage exists. In PDP, the integrity of the data stored in the cloud storage is probabilistically verified by the user or a third-party auditor. In the conventional PDP, the user creates the metadata used for audition. From the viewpoint of user convenience, it is desirable to be able to audit without operations other than uploading. In other words, the challenge is to provide a transparent PDP that verifies the integrity of files according to the general cloud storage system model so as not to add operations to users. We propose a scheme in which the cloud generates the metadata used during verification, and the user only uploads files. It is shown that the proposed scheme is resistant to the forgery of cloud proof and the acquisition of data by a third-party auditor.

We consider the problem of protecting cloud services from simultaneous white-box and black-box attacks. Recent research in cryptographic program obfuscation considers the problem of protecting the confidentiality of programs and any secrets in them. In this model, a provable program obfuscation solution makes white-box attacks to the program not more useful than black-box attacks. Motivated by very recent results showing successful black-box attacks to machine learning programs run by cloud servers, we propose and study the approach of augmenting the program obfuscation solution model so to achieve, in at least some class of application scenarios, program confidentiality in the presence of both white-box and black-box attacks.We propose and formally define encrypted-input program obfuscation, where a key is shared between the entity obfuscating the program and the entity encrypting the program's inputs. We believe this model might be of interest in practical scenarios where cloud programs operate over encrypted data received by associated sensors (e.g., Internet of Things, Smart Grid).Under standard intractability assumptions, we show various results that are not known in the traditional cryptographic program obfuscation model; most notably: Yao's garbled circuit technique implies encrypted-input program obfuscation hiding all gates of an arbitrary polynomial circuit; and very efficient encrypted-input program obfuscation for range membership programs and a class of machine learning programs (i.e., decision trees). The performance of the latter solutions has only a small constant overhead over the equivalent unobfuscated program.

Most searchable attribute-based encryption schemes only support the search for single-keyword without attribute revocation, the data user cannot quickly detect the validity of the ciphertext returned by the cloud service provider. Therefore, this paper proposes an authorization of searchable CP-ABE scheme with attribute revocation and applies the scheme to the cloud computing environment. The data user to send the authorization information to the authorization server for authorization, assists the data user to effectively detect the ciphertext information returned by the cloud service provider while supporting the revocation of the user attribute in a fine-grained access control structure without updating the key during revocation stage. In the random oracle model based on the calculation of Diffie-Hellman problem, it is proved that the scheme can satisfy the indistinguishability of ciphertext and search trapdoor. Finally, the performance analysis shows that the scheme has higher computational efficiency.

Strong designated verifier signature scheme is a concept in which a user (signer) can issue a digital signature for a special receiver; i.e. signature is produced in such way that only intended verifier can check the validity of produced signature. Of course, this type of signature scheme should be such that no third party is able to validate the signature. In other words, the related designated verifier cannot assign the issued signature to another third party. This article proposes a new ID-based strong designated verifier signature scheme which has provable security in the ROM (Random Oracle Model) and BDH assumption. The proposed scheme satisfies the all security requirements of an ID-based strong designated verifier signature scheme. In addition, we propose some usage scenarios for the proposed schemes in different applications in the Internet of Things and Cloud Computing era.

Logic encryption, a method to lock a circuit from unauthorized use unless the correct key is provided, is the most important technique in hardware IP protection. However, with the discovery of the SAT attack, all traditional logic encryption algorithms are broken. New algorithms after the SAT attack are all vulnerable to structural analysis unless a provable obfuscation is applied to the locked circuit. But there is no provable logic obfuscation available, in spite of some vague resorting to logic resynthesis. In this paper, we formulate and discuss a trilemma in logic encryption among locking robustness, structural security, and encryption efficiency, showing that pre-SAT approaches achieve only structural security and encryption efficiency, and post-SAT approaches achieve only locking robustness and encryption efficiency. There is also a dilemma between query complexity and error number in locking. We first develop a theory and solution to the dilemma in locking between query complexity and error number. Then, we provide a provable obfuscation solution to the dilemma between structural security and locking robustness. We finally present and discuss some results towards the resolution of the trilemma in logic encryption.

The globalization of the integrated circuit supply chain has given rise to major security concerns ranging from intellectual property piracy to hardware Trojans. Logic encryption is a promising solution to tackle these threats. Recently, a Boolean satisfiability attack capable of unlocking existing logic encryption techniques was introduced. This attack initiated a paradigm shift in the design of logic encryption algorithms. However, recent approaches have been strongly focusing on low-cost countermeasures that unfortunately lead to low functional and structural corruption. In this paper, we show that a simple approach can offer provable security and more than 99% corruption if a higher area overhead is accepted. Our results strongly suggest that future proposals should consider higher overheads or more realistic circuit sizes for the evaluation of modern logic encryption algorithms.

This paper focuses on research of a provably secure code-based pseudorandom sequence generators whose cryptanalysis problem equals to syndrome decoding (belonging to the NP-complex class). It was found that generated sequences of such well-known Fischer-Stern code-based generator don’t have a maximum period, the actual period is much lower than expected. In our work, we have created a new generator scheme. It retains all advantages of the Fisher-Stern algorithm and provides pseudorandom sequences which are formed with maximum period. Also comparative analysis of proposed generator and popular generators was conducted.