Название: Handbook of Formal Analysis and Verification in Cryptography
Автор: Sedat Akleylek, Besik Dundua
Издательство: CRC Press
Год: 2024
Страниц: 445
Язык: английский
Формат: pdf (true)
Размер: 11.8 MB

This handbook of formal analysis in cryptography is very important for secure communication and processing of information. It introduces readers to several formal verification methods and software used to analyse cryptographic protocols. The chapters give readers general knowledge and formal methods focusing on cryptographic protocols.

Handbook of Formal Analysis and Verification in Cryptography includes major formalisms and tools used for formal verification of cryptography, with a spotlight on new-generation cryptosystems such as post-quantum, and presents a connection between formal analysis and cryptographic schemes. The text offers formal methods to show whether security assumptions are valid and compares the most prominent formalism and tools as they outline common challenges and future research directions.

The handbook can be divided into three parts, the first two on formal analysis of cryptographic protocols, and the last one giving surveys of other areas.

The first part, consisting of Chapters 1 and 2, gives background and a broad overview of formal analysis of cryptographic protocols. Chapter 1 is a survey of cryptography since Shannon’s groundbreaking work in the 1940s. It goes on to cover relevant topics including secret-key cryptography, public-key cryptography, post-quantum cryptography, and homomorphic encryption, giving details about specific algorithms along the way. This gives a context from which to view the other chapters in the book. Chapter 2 then gives an overview of the various theories and techniques used in formal analysis of cryptographic protocols, showing how techniques such as model checking, belief logics, and model extraction have been used in this area.

Once the reader has been introduced to the basics, the next part, consisting of Chapters 3 and 4, introduces specific tools and techniques. Chapter 3 covers tools that have been developed specifically for the analysis of cryptographic protocols, covering six different such tools. Chapter 4 demonstrates how an existing formal methods tool, the Isabelle/HOL theorem prover, can be used for the formal analysis of cryptographic protocols, taking advantage of the prover’s support for inductive reasoning. Finally, Chapter 5 covers special topics in the formal analysis of cryptographic protocols, in particular, how to specify protocols, and the use of multiple analysis tools.

The last parts, consisting of Chapters 6 and 7, give in-depth explorations of the applications of formal methods to two other areas. Chapter 6 presents an overview of the application of formal methods to the development of secure cryptographic Web applications, taking into account the highly distributed nature of Web services and their effects on security. This includes not only formal verification of the protocols the Web applications use, but the software in which the applications are implemented. Chapter 7 gives a survey of formal quantum programming algorithms, showing how the mechanisms of quantum computation are captured formally.

Graduate students, researchers, and engineers worldwide will find this an exciting read.