Certified Security by Design Using Higher Order Logic (Chapman & Hall/CRC Cryptography and Network Security Series)
暫譯: 以高階邏輯進行安全設計認證（Chapman & Hall/CRC 密碼學與網路安全系列）

This textbook serves the needs of engineers and computer scientists responsible for designing, implementing, and verifying secure computer and information systems. Methods are based on the application of logic as a means for describing, reasoning about, and verifying the properties of systems. We use logic from the conceptualization stage, through the design phase, and up to and including verification and certification. The use of computer-aided design (CAD) tools and computer assisted reasoning tools, such as theorem provers, is essential. We have included numerous examples to illustrate principles, as well as many exercises to serve as assessments of knowledge.