Biblio

A considerable portion of computing power is always required to perform symbolic calculations. The reliability and effectiveness of algorithms are two of the most significant challenges observed in the field of scientific computing. The terms “feasible calculations” and “feasible computations” refer to the same idea: the algorithms that are reliable and effective despite practical constraints. This research study intends to investigate different types of computing and modelling challenges, as well as the development of efficient integration methods by considering the challenges before generating the accurate results. Further, this study investigates various forms of errors that occur in the process of data integration. The proposed framework is based on automata, which provides the ability to investigate a wide-variety of distinct distance-bounding protocols. The proposed framework is not only possible to produce computational (in)security proofs, but also includes an extensive investigation on different issues such as optimal space complexity trade-offs. The proposed framework in embedded with the already established symbolic framework in order to get a deeper understanding of distance-bound security. It is now possible to guarantee a certain level of physical proximity without having to continually mimic either time or distance.

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).

While information-theoretic security is stronger than computational security, it has long been considered impractical. In this work, we provide new insights into the design of practical information-theoretic cryptosystems. Firstly, from a theoretical point of view, we give a brief introduction into the existing information theoretic security criteria, such as the notions of Shannon's perfect/ideal secrecy in cryptography, and the concept of strong secrecy in coding theory. Secondly, from a practical point of view, we propose the concept of ideal secrecy outage and define a outage probability. Finally, we show how such probability can be made arbitrarily small in a practical cryptosystem.

An important principle in computational security is to reduce the attack surface, by maintaining the Trusted Computing Base (TCB) small. Even so, no security technique ensures full protection against any adversary. Thus, sensitive applications should be designed with several layers of protection so that, even if a layer might be violated, sensitive content will not be compromised. In 2015, Intel released the Software Guard Extensions (SGX) technology in its processors. This mechanism allows applications to allocate enclaves, which are private memory regions that can hold code and data. Other applications and even privileged code, like the OS kernel and the BIOS, are not able to access enclaves' contents. This paper presents a novel password file protection scheme, which uses Intel SGX to protect authentication credentials in the PAM authentication framework, commonly used in UNIX systems. We defined and implemented an SGX-enabled version of the pam\_unix.so authentication module, called UniSGX. This module uses an SGX enclave to handle the credentials informed by the user and to check them against the password file. To add an extra security layer, the password file is stored using SGX sealing. A threat model was proposed to assess the security of the proposed solution. The obtained results show that the proposed solution is secure against the threat model considered, and that its performance overhead is acceptable from the user point of view. The scheme presented here is also suitable to other authentication frameworks.

Today's major concern is not only maximizing the information rate through linear network coding scheme which is intelligent combination of information symbols at sending nodes but also secured transmission of information. Though cryptographic measure of security (computational security) gives secure transmission of information, it results system complexity and consequent reduction in efficiency of the communication system. This problem leads to alternative way of optimally secure and maximized information transmission. The alternative solution is secure network coding which is information theoretic approach. Depending up on applications, different security measures are needed during the transmission of information over wiretapped network with potential attack by the adversaries. In this research work, mathematical model for different security constraints with upper and lower boundaries were studied depending up on the randomness added to the source message and hence the security constraints on linear network code for randomized source messages depends both on randomness added and number of random source symbols. If the source generates large number random symbols, lesser number of random keys can give higher security to the information but information theoretic security bounds remain same. Hence maximizing randomness to the source is equivalent to adding security level.