Abstract
We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.

Abstract

Abstract

Abstract

Abstract
This book describes the Optical Immersion Clearing method and its application to acquire information with importance for clinical practice and various fields of biomedical engineering. The method has proved to be a reliable means of increasing tissue transparency, allowing the investigator or surgeon to reach deeper tissue layers for improved imaging and laser surgery. This result is obtained by partial replacement of tissue water with an active optical clearing agent (OCA) that has a higher refractive index and is a better match for the refractive index of other tissue components. Natural tissue scattering is thereby reduced. An exponential increase in research using this method has occurred in recent years, and new applications have emerged, both in clinical practice and in some areas of biomedical engineering. Recent research has revealed that treating ex vivo tissues with solutions containing active OCAs in different concentrations produces experimental data to characterize drug delivery or to discriminate between normal and pathological tissues. The obtained drug diffusion properties are of interest for the pharmaceutical and organ preservation industry. Similar data can be estimated with particular interest for food preservation. The free water content evaluation is also of great interest since it facilitates the characterization of tissues to discriminate pathologies. An interesting new application that is presented in the book regards the creation of two optical windows in the ultraviolet spectral range through the application of the immersion method. These induced transparency windows open the possibility to diagnose and treat pathologies with ultraviolet light. This book presents photographs from the tissues we have studied and figures that represent the experimental setups used. Graphs and tables are also included to show the numerical results obtained in the sequential calculations performed.

Abstract