Biblio

In recent years, the research community has increasingly focused on understanding the security and privacy challenges posed by deep learning models. However, the security domain and the privacy domain have typically been considered separately. It is thus unclear whether the defense methods in one domain will have any unexpected impact on the other domain. In this paper, we take a step towards enhancing our understanding of deep learning models when the two domains are combined together. We do this by measuring the success of membership inference attacks against two state-of-the-art adversarial defense methods that mitigate evasion attacks: adversarial training and provable defense. On the one hand, membership inference attacks aim to infer an individual's participation in the target model's training dataset and are known to be correlated with target model's overfitting. On the other hand, adversarial defense methods aim to enhance the robustness of target models by ensuring that model predictions are unchanged for a small area around each sample in the training dataset. Intuitively, adversarial defenses may rely more on the training dataset and be more vulnerable to membership inference attacks. By performing empirical membership inference attacks on both adversarially robust models and corresponding undefended models, we find that the adversarial training method is indeed more susceptible to membership inference attacks, and the privacy leakage is directly correlated with model robustness. We also find that the provable defense approach does not lead to enhanced success of membership inference attacks. However, this is achieved by significantly sacrificing the accuracy of the model on benign data points, indicating that privacy, security, and prediction accuracy are not jointly achieved in these two approaches.

Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be synergistically exploited to create side-channel leaks that are greater than the sum of their parts. While both hardware and software mitigations have been proposed against these attacks, provable security has remained elusive. This paper introduces a formal methodology for enabling secure speculative execution on modern processors. We propose a new class of information flow security properties called trace property-dependent observational determinism (TPOD). We use this class to formulate a secure speculation property. Our formulation precisely characterises all transient execution vulnerabilities. We demonstrate its applicability by verifying secure speculation for several illustrative programs.

Considering application to communication among wireless sensors, Ma and Tsudik introduced the notion of forward-secure sequential aggregate (FssAgg) authentication in 2007. They also proposed an FssAgg MAC scheme composed of a MAC function and cryptographic hash functions at the same time. The security of their proposed scheme has not been analyzed yet and remains open. It is shown in this paper that a slight variant of the Ma-Tsudik FssAgg MAC scheme is secure under reasonable and standard assumptions on security of the underlying primitives. An efficient instantiation of the underlying MAC function using a cryptographic hash function is also discussed.

A method to increase the resiliency of in-cone logic locking against the SAT attack is described in this paper. Current logic locking techniques provide protection through the addition of circuitry outside of the original logic cone. While the additional circuitry provides provable security against the SAT attack, other attacks, such as the removal attack, limit the efficacy of such techniques. Traditional in-cone logic locking is not prone to removal attacks, but is less secure against the SAT attack. The focus of this paper is, therefore, the analysis of in-cone logic locking to increase the security against the SAT attack, which provides a comparison between in-cone techniques and newly developed methodologies. A novel algorithm is developed that utilizes maximum fanout free cones (MFFC). The application of the algorithm limits the fanout of incorrect key information. The MFFC based algorithm resulted in an average increase of 61.8% in the minimum number of iterations required to complete the SAT attack across 1,000 different variable orderings of the circuit netlist while restricted to a 5% overhead in area.

We introduce FairSwap – an efficient protocol for fair exchange of digital goods using smart contracts. A fair exchange protocol allows a sender S to sell a digital commodity x for a fixed price p to a receiver R. The protocol is said to be secure if R only pays if he receives the correct x. Our solution guarantees fairness by relying on smart contracts executed over decentralized cryptocurrencies, where the contract takes the role of an external judge that completes the exchange in case of disagreement. While in the past there have been several proposals for building fair exchange protocols over cryptocurrencies, our solution has two distinctive features that makes it particular attractive when users deal with large commodities. These advantages are: (1) minimizing the cost for running the smart contract on the blockchain, and (2) avoiding expensive cryptographic tools such as zero-knowledge proofs. In addition to our new protocols, we provide formal security definitions for smart contract based fair exchange, and prove security of our construction. Finally, we illustrate several applications of our basic protocol and evaluate practicality of our approach via a prototype implementation for fairly selling large files over the cryptocurrency Ethereum. This article is summarized in: the morning paper an interesting/influential/important paper from the world of CS every weekday morning, as selected by Adrian Colyer

Remote data possession is becoming an increasingly important issue in cloud storage. It enables users to verify if their outsourced data have remained intact while in cloud storage. The existing remote data audit (RDA) protocols were designed with the public key infrastructure (PKI) system. However, this incurs considerable costs when users need to frequently access data from the cloud service provider with PKI. This study proposes a protocol, called identity-based RDA (ID-RDA) that addresses this problem without the need for users’ certificates. This study outperforms existing RDA protocols in computation and communication.

Cryptographic channels aim to enable authenticated and confidential communication over the Internet. The general understanding seems to be that providing security in the sense of authenticated encryption for every (unidirectional) point-to-point link suffices to achieve this goal. As recently shown (in FSE17/ToSC17), however, the security properties of the unidirectional links do not extend, in general, to the bidirectional channel as a whole. Intuitively, the reason for this is that the increased interaction in bidirectional communication can be exploited by an adversary. The same applies, a fortiori, in a multi-party setting where several users operate concurrently and the communication develops in more directions. In the cryptographic literature, however, the targeted goals for group communication in terms of channel security are still unexplored. Applying the methodology of provable security, we fill this gap by defining exact (game-based) authenticity and confidentiality goals for broadcast communication, and showing how to achieve them. Importantly, our security notions also account for the causal dependencies between exchanged messages, thus naturally extending the bidirectional case where causal relationships are automatically captured by preserving the sending order. On the constructive side we propose a modular and yet efficient protocol that, assuming only point-to-point links between users, leverages (non-cryptographic) broadcast and standard cryptographic primitives to a full-fledged broadcast channel that provably meets the security notions we put forth.

In the literature, many chaotic systems have been used in the design of image encryption algorithms. In this study, an application of fractional order chaotic systems is investigated. The aim of the study is to improve the disadvantageous aspects of existing methods based on discrete and continuous time chaotic systems by utilizing the features of fractional order chaotic systems. The most important advantage of the study compared to the literature is that the proposed encryption algorithm is designed with a provable security approach. Analyses results have been shown that the proposed method can be used successfully in many information security applications.

User authentication in wireless sensor networks is more complex than normal networks due to sensor network characteristics such as unmanned operation, limited resources, and unreliable communication. For this reason, various authentication protocols have been presented to provide secure and efficient communication. In 2017, Wu et al. presented a provable and privacy-preserving user authentication protocol for wireless sensor networks. Unfortunately, we found that Wu et al.'s protocol was still vulnerable against user impersonation attack, and had a problem in the password change phase. We show how an attacker can impersonate an other user and why the password change phase is ineffective.

The Internet of Things (IoT) consists of embedded devices that sense and manage our environment in a growing range of applications. Large-scale IoT systems such as smart cities require significant investment in both equipment and personnel. To maximize return on investment, IoT platforms should support multiple third-party applications and adaptation of infrastructure over time. Realizing the vision of shared IoT platforms demands strong security guarantees. That is particularly challenging considering the limited capability and resource constraints of many IoT devices. In this paper, we present SPEED, an approach to secure erasure with verifiability in IoT. Secure erasure is a fundamental property when it comes to share an IoT platform with other users which guarantees the cleanness of a device's memory at the beginning of the application deployment as well as at the time of releasing the underlying IoT device. SPEED relies on two security primitives: memory isolation and distance bounding protocol. We evaluate the performance of SPEED by implementing it on a simple bare-metal IoT device belongs to Class-1. Our evaluation results show a limited overhead in terms of memory footprint, time, and energy consumption.

Companies are often motivated to evaluate their environmental sustainability, and to make public pronouncements about their performance with respect to quantitative sustainability metrics. Public trust in these declarations is enhanced if the claims are certified by a recognized authority. Because accurate evaluations of environmental impacts require detailed information about industrial processes throughout a supply chain, protecting the privacy of input data in sustainability assessment is of paramount importance. We introduce a new paradigm, called privacy-preserving certification, that enables the computation of sustainability indicators in a privacy-preserving manner, allowing firms to be classified based on their individual performance without revealing sensitive information to the certifier, other parties, or the public. In this work, we describe different variants of the certification problem, highlight the necessary security requirements, and propose a provably-secure novel framework that performs the certification operations under the management of an authorized, yet untrusted, party without compromising confidential information.

When relying on public key infrastructure (PKI) for authentication, whether a party can be trusted primarily depends on its certificate status. Bob's certificate status can be retrieved by Alice through her interaction with Certificate Authority (CA) in the PKI. More specifically, Alice can download Certificate Revocation List (CRL) and then check whether the serial number of the Bob's certificate appears in this list. If not found, Alice knows that Bob can be trusted. Once downloaded, a CRL can be used offline for arbitrary many times till it expires, which saves the bandwidth to an extreme. However, if the number of revoked certificates becomes too large, the size of the CRL will exceed the RAM of Alice's device. This conflict between bandwidth and RAM consumption becomes even more challenging for the Internet-of-Things (IoT), since the IoT end-devices is usually constrained by both factors. To solve this problem in PKI-based authentication in IoT, we proposed two novel lightweight CRL protocols with maximum flexibility tailored for constrained IoT end-devices. The first one is based on generalized Merkle hash tree and the second is based on Bloom filter. We also provided quantitative theorems for CRL parameter configuration, which help strike perfect balance among bandwidth, RAM usage and security in various practical IoT scenarios. Furthermore, we thoroughly evaluated the proposed CRL protocols and exhibited their outstanding efficiency in terms of RAM and bandwidth consumption. In addition, our formal treatment of the security of a CRL protocol can also be of independent interest.

Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limited in scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Grégoire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary's knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPA-PKE (Gentry et al., STOC 2008), (Hierarchical) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Gröbner basis computations for subalgebras in the (non-)commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs.

Direct Memory Access (DMA) attacks can allow attackers to access memory directly, bypassing OS supervision or software protections. In this work, we put forth and benchmark a cryptographically secure attestation scheme, which detects DMA attacks. In fact, our scheme detects any attack in a more general class of attacks which we call "direct injection". We prove security of our scheme under a realistic machine model which extends in a non-trivial manner a cryptographic model proposed by Lipton, Ostrovsky, and Zikas (ICALP 2016.) Despite the fact that our scheme, in its current form, protects against write-only attacks, both our security model and our scheme can be extended to allow the attacker to have additional read access to memory—thereby capturing leakage—as well as detecting more types of memory corruptions such as bit flips.

Thumbnail preserving encryption (TPE) was suggested by Wright et al. [Information Hiding & Multimedia Security Workshop 2015] as a way to balance privacy and usability for online image sharing. The idea is to encrypt a plaintext image into a ciphertext image that has roughly the same thumbnail as well as retaining the original image format. At the same time, TPE allows users to take advantage of much of the functionality of online photo management tools, while still providing some level of privacy against the service provider. In this work we present two new approximate TPE encryption schemes. In our schemes, ciphertexts and plaintexts have perceptually similar, but not identical, thumbnails. Our constructions are the first TPE schemes designed to work well with JPEG compression. In addition, we show that they also have provable security guarantees that characterize precisely what information about the plaintext is leaked by the ciphertext image. We empirically evaluate our schemes according to the similarity of plaintext & ciphertext thumbnails, increase in file size under JPEG compression, preservation of perceptual image hashes, among other aspects. We also show how approximate TPE can be an effective tool to thwart inference attacks by machine-learning image classifiers, which have shown to be effective against other image obfuscation techniques.

Deduplication is a widely used technique for reducing storage space of cloud service providers. Yet, it is unclear how to support deduplication of encrypted data securely until the study of Bellareetal on message-locked encryption (Eurocrypt 2013). Since then, there are many improvements such as strengthening its security, reducing client storage, etc. While updating a (shared) file is common, there is little attention on how to efficiently update large encrypted files in a remote storage with deduplication. To modify even a single bit, existing solutions require the trivial and expensive way of downloading and decrypting the large ciphertext. We initiate the study of updatable block-level message-locked encryption. We propose a provably secure construction that is efficiently updatable with O(logtextbarFtextbar) computational cost, where textbarFtextbar is the file size. It also supports proof-of-ownership, a nice feature which protects storage providers from being abused as a free content distribution network.

Encrypted databases, a popular approach to protecting data from compromised database management systems (DBMS's), use abstract threat models that capture neither realistic databases, nor realistic attack scenarios. In particular, the "snapshot attacker" model used to support the security claims for many encrypted databases does not reflect the information about past queries available in any snapshot attack on an actual DBMS. We demonstrate how this gap between theory and reality causes encrypted databases to fail to achieve their "provable security" guarantees.

For a secure communication over an insecure channel the Diffie-Hellman key exchange protocol (DHKEP) is treated as the de facto standard. However, it suffers form server-side compromisation, identity compromisation, man-in-the-middle, replay attacks, etc. Also, there are single point of vulnerability (SOV), single point of failure (SOF) and user privacy preservation issues. This work proposes an identity-based two-server DHKEP to address the aforesaid issues and alleviating the attacks. To preserve user identity from outside intruders, a k-anonymity based identity hiding principle has been adopted. Further, to ensure efficient utilization of channel bandwidth, the proposed scheme employs elliptic curve cryptography. The security analysis substantiate that our scheme is provably secure and successfully addressed the above-mentioned issues. The performance study contemplates that the overhead of the protocol is reasonable and comparable with other schemes.

A strong designated verifier signature (SDVS) is a variation of traditional digital signatures, since it allows a signer to designate an intended receiver as the verifier rather than anyone. To do this, a signer must incorporate the verifier's public key with the signing procedure such that only the intended receiver could verify this signature with his/her private key. Such a signature further enables a designated verifier to simulate a computationally indistinguishable transcript intended for himself. Consequently, no one can identify the real signer's identity from a candidate signer and a designated verifier, which is referred to as the property of signer ambiguity. A strong notion of signer ambiguity states that no polynomial-time adversary can distinguish the real signer of a given SDVS that is not received by the designated verifier, even if the adversary has obtained the signer's private key. In 2013, Islam and Biswas proposed a provably secure certificateless strong designated verifier signature (CL-SDVS) scheme based on bilinear pairings. In this paper, we will demonstrate that their scheme fails to satisfy strong signer ambiguity and must assume a trusted private key generator (PKG). In other words, their CL-SDVS scheme is vulnerable to both key-compromise and malicious PKG attacks. Additionally, we present an improved variant to eliminate these weaknesses.

We consider the situation, where an adversary may learn the ephemeral values used by the prover within an identification protocol, aiming to get the secret keys of the user, or just to impersonate the prover subsequently. Unfortunately, most classical cryptographic identification protocols are exposed to such attacks, which might be quite realistic in case of software implementations. According to a recent proposal from SECIT-2017, we regard a scheme to be secure, if a malicious verifier, allowed to set the prover's ephemerals in the query stage, cannot impersonate the prover later on. We focus on the Okamoto Identification Scheme (IS), and show how to make it immune to the threats described above. Via reduction to the GDH Problem, we provide security guarantees in case of insufficient control over the unit executing Okamoto identification protocol (the standard Okamoto protocol is insecure in this situation).

In this paper, we propose principles of information control and sharing that support ORCON (ORiginator COntrolled access control) models while simultaneously improving components of confidentiality, availability, and integrity needed to inherently support, when needed, responsibility to share policies, rapid information dissemination, data provenance, and data redaction. This new paradigm of providing unfettered and unimpeded access to information by authorized users, while at the same time, making access by unauthorized users impossible, contrasts with historical approaches to information sharing that have focused on need to know rather than need to (or responsibility to) share.

A one-message unilateral entity authentication scheme allows one party, called the prover, to authenticate himself, i.e., to prove his identity, to another party, called the verifier, by sending a single authentication message. In this paper we consider schemes where the prover and the verifier do not share any secret information, such as a password, in advance. We propose the first theoretical characterization for one-message unilateral entity authentication schemes, by formalizing the security requirements for such schemes with respect to different kinds of adversaries. Afterwards, we propose three provably-secure constructions for one-message unilateral entity authentication schemes.

Cloud services are widely used to virtualize the management and actuation of the real-world the Internet of Things (IoT). Due to the increasing privacy concerns regarding querying untrusted cloud servers, query anonymity has become a critical issue to all the stakeholders which are related to assessment of the dependability and security of the IoT system. The paper presents our study on the problem of query receiver-anonymity in the cloud-based IoT system, where the trade-off between the offered query-anonymity and the incurred communication is considered. The paper will investigate whether the accepted worst-case communication cost is sufficient to achieve a specific query anonymity or not. By way of extensive theoretical analysis, it shows that the bounds of worst-case communication cost is quadratically increased as the offered level of anonymity is increased, and they are quadratic in the network diameter for the opposite range. Extensive simulation is conducted to verify the analytical assertions.

Security is an important requirement of every reactive system of the smart gird. The devices connected to the smart system in smart grid are exhaustively used to provide digital information to outside world. The security of such a system is an essential requirement. The most important component of such smart systems is Operating System (OS). This paper mainly focuses on the security of OS by incorporating Access Control Mechanism (ACM) which will improve the efficiency of the smart system. The formal methods use applied mathematics for modelling and analysing of smart systems. In the proposed work Formal Security Analysis (FSA) is used with model checking and hence it helped to prove the security of smart systems. When an Operating System (OS) takes into consideration, it never comes to a halt state. In the proposed work a Transition System (TS) is designed and the desired rules of security are provided by using Linear Temporal Logics (LTL). Unlike other propositional and predicate logic, LTL can model reactive systems with a prediction for the future state of the systems. In the proposed work, Simple Promela Interpreter (SPIN) is used as a model checker that takes LTL and TS of the system as input. Hence it is possible to derive the Büchi automaton from LTL logics and that provides traces of both successful and erroneous computations. Comparison of Büchi automaton with the transition behaviour of the OS will provide the details of security violation in the system. Validation of automaton operations on infinite computational sequences verify that whether systems are provably secure or not. Hence the proposed formal security analysis will provably ensures the security of smart systems in the area of smart grid applications.

Over the past few years we have articulated theory that describes ‘encrypted computing’, in which data remains in encrypted form while being worked on inside a processor, by virtue of a modified arithmetic. The last two years have seen research and development on a standards-compliant processor that shows that near-conventional speeds are attainable via this approach. Benchmark performance with the US AES-128 flagship encryption and a 1GHz clock is now equivalent to a 433MHz classic Pentium, and most block encryptions fit in AES's place. This summary article details how user data is protected by a system based on the processor from being read or interfered with by the computer operator, for those computing paradigms that entail trust in data-oriented computation in remote locations where it may be accessible to powerful and dishonest insiders. We combine: (i) the processor that runs encrypted; (ii) a slightly modified conventional machine code instruction set architecture with which security is achievable; (iii) an ‘obfuscating’ compiler that takes advantage of its possibilities, forming a three-point system that provably provides cryptographic "semantic security" for user data against the operator and system insiders.