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.