Biblio

The revelations of Snowden show that hardware and software of devices may corrupt users' machine to compromise the security in various ways. To address this concern, Mironov and Stephen-Davidowitz introduce the Cryptographic Reverse Firewall (CRF) concept that is able to resist the ex-filtration of secret information for some compromised machine (Eurocrypt 2015). There are some applications of CRF deployed in many cryptosystems, but less studied and deployed in Attribute-Based Encryption (ABE) field, which attracts a wide range of attention and is employed in real-world scenarios (i.e., data sharing in cloud). In this work, we focus how to give a CRF security protection for a multi-authority ABE scheme and hence propose a multi-authority key-policy ABE scheme with CRF (acronym, MA-KP-ABE-CRF), which supports attribute distribution and non-monotonic access structure. To achieve this, beginning with revisiting a MA-KP-ABE with non-trivial combining non-monotonic formula, we then give the randomness of ciphertexts and secret keys with reverse firewall and give formal security analysis. Finally, we give a simulation on our MA-KP-ABE-CRF system based on Charm library whose the experimental results demonstrate practical efficiency.

Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, Küsters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.

Data outsourcing to cloud has been a common IT practice nowadays due to its significant benefits. Meanwhile, security and privacy concerns are critical obstacles to hinder the further adoption of cloud. Although data encryption can mitigate the problem, it reduces the functionality of query processing, e.g., disabling SQL queries. Several schemes have been proposed to enable one-dimensional query on encrypted data, but multi-dimensional range query has not been well addressed. In this paper, we propose a secure and scalable scheme that can support multi-dimensional range queries over encrypted data. The proposed scheme has three salient features: (1) Privacy: the server cannot learn the contents of queries and data records during query processing. (2) Efficiency: we utilize hierarchical cubes to encode multi-dimensional data records and construct a secure tree index on top of such encoding to achieve sublinear query time. (3) Verifiability: our scheme allows users to verify the correctness and completeness of the query results to address server's malicious behaviors. We perform formal security analysis and comprehensive experimental evaluations. The results on real datasets demonstrate that our scheme achieves practical performance while guaranteeing data privacy and result integrity.

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.