Cover -- Half-title -- Title -- Copyright -- Contents -- Preface -- Acknowledgments -- CHAPTER 1 Secure Communication in Modern Information Societies -- 1.1 ELECTRONIC COMMERCE: THE MANTRA OF Y2K+ -- 1.2 CRYPTOGRAPHIC SYSTEMS -- 1.3 LEGISLATING ELECTRONIC AUTHENTICATION -- 1.4 THE MATHEMATICAL JUDGE -- 1.5 ENCRYPTION POLICIES -- 1.6 TRUST AND COMMUNITIES -- 1.7 BIBLIOGRAPHIC NOTES -- CHAPTER 2 Public-Key Cryptography -- 2.1 SPECIFICATION OF RSA -- 2.1.0.1 Digital Signatures -- 2.1.0.2 A Protocol for Secure Communication -- 2.2 A REALIZATION OF PKCs: RSA -- 2.3 GENERATING LARGE PRIMES -- 2.3.1 Iterative Squaring -- 2.3.2 Correctness of Witness(a,n) -- 2.3.2.1 Fermat'sTheorem -- 2.3.2.2 Greatest Common Divisor -- 2.3.2.3 Square Roots of 1 -- 2.3.2.4 Proof of Theorem 2.32 -- 2.3.3 When Witness(a,n) Fails -- 2.3.4 Efficiency of Finding Large Primes -- 2.4 CORRECTNESS OF RSA -- 2.5 SECURITY OF RSA -- 2.6 INTEGER FACTORIZATION -- 2.6.1 Pollard's Rho Heuristic -- 2.7 OTHER KEY-EXCHANGE REALIZATIONS BASED ON DISCRETE LOGARITHMS -- 2.7.1 Diffie-Hellman Key-Exchange System -- 2.7.2 Station-to-Station Protocol -- 2.7.3 Massey-Omura Cryptosystem -- 2.7.4 ElGamal Cryptosystem -- 2.8 BIBLIOGRAPHIC NOTES -- CHAPTER 3 Symmetric-Key Cryptography -- 3.1 STREAM CIPHERS -- 3.1.1 Some History -- 3.1.2 Notions of Randomness -- 3.1.3 Linear Feedback Shift Registers -- 3.1.3.1 Feedback Shift Registers -- 3.1.3.2 Linear Boolean Functions -- 3.1.4 Nonlinearity -- 3.2 BLOCK CIPHERS -- 3.2.1 Data Encryption Standard: DES -- 3.2.1.1 The Electronic Codebook Mode -- 3.2.1.2 DES Modes of Operations -- 3.2.1.3 Triple DES -- 3.2.2 Advanced Encryption Standard: Rijndael -- 3.2.2.1 Bytes as Polynomials -- 3.2.2.2 Rijndael's Encryption Mode -- 3.2.2.3 Rijndael's Decryption Mode -- 3.2.2.4 Rijndael's Design Criteria -- 3.2.3 Secure Hash Standard: SHA -- 3.2.3.1 Useful Terminology.

3.2.3.2 The Algorithm -- 3.2.3.3 Message Padding -- 3.3 BIBLIOGRAPHIC NOTES -- CHAPTER 4 Security Protocol Design and Analysis -- 4.1 DIGITAL SIGNATURES -- 4.1.1 Digital Signature Standard: DSS -- 4.1.1.1 Protocol Parameters -- 4.1.1.2 Generating a Digital Signature -- 4.1.1.3 Digital Signature Verification -- 4.1.1.4 Correctness of Protocol -- 4.1.1.5 Verifiable Generation of Public Protocol Parameters -- 4.1.1.6 Security of DSS -- 4.1.2 Elliptic Curve Digital Signature Algorithm -- 4.1.2.1 Elliptic Curves -- 4.2 SECURE LOG-IN PROTOCOLS -- 4.2.0.2 The Guillou-Quisquater Protocol -- 4.2.0.3 Combining Identity- and Ticket-Based Log-Ins -- 4.3 AUTHENTICATION REVISITED -- 4.3.0.4 Signatures May Not Lead to Credit -- 4.3.0.5 Encryption May Not Lead to Responsibility -- 4.4 SECRET-SHARING PROTOCOLS -- 4.5 MODEL CHECKING SECURITY PROTOCOL DESIGNS -- 4.5.1 Modeling Network Messages -- 4.5.2 Modeling Network Agents -- 4.5.2.1 Communication between Agents -- 4.5.2.2 Creation of Nonces and Temporary Secrets -- 4.5.2.3 Intruders and Untrusted Channels -- 4.5.2.4 Specifications -- 4.5.2.5 Searching the Global State Space -- 4.5.3 Representing and Deducing Knowledge -- 4.5.4 Two Example Refutations -- 4.5.4.1 Needham-Schroeder Protocol -- 4.5.4.2 Woo-Lam Protocol -- 4.6 BIBLIOGRAPHIC NOTES -- CHAPTER 5 Optimal Public-Key Encryption with RSA -- 5.1 A SIMPLE SEMANTICALLY SECURE ENCRYPTION -- 5.2 A PLAIN-TEXT-AWARE ENCRYPTION -- 5.2.1 Implementation of Plain-Text-Aware Encryption -- 5.3 THE RANDOM ORACLE METHODOLOGY -- 5.4 EXACT SECURITY FOR THE SIMPLE ENCRYPTION -- 5.4.1 Proof of Exact Semantic Security -- 5.5 EXACT SECURITY FOR THE PLAIN-TEXT-AWARE ENCRYPTION -- 5.5.1 Proof of Exact Security for Plain-Text-Aware Encryption -- 5.6 BIBLIOGRAPHIC NOTES -- CHAPTER 6 Analysis of Secure Information Flow -- 6.1 MOTIVATION.

6.2 A TYPE SYSTEM FOR ANALYSIS OF SECURE INFORMATION FLOW -- 6.2.1 Type System for Boolean and Integer Expressions -- 6.2.2 Specifying Secure Information Flow -- 6.2.3 A Core Programming Language -- 6.2.4 Formal Semantics of Core Language -- 6.2.5 Analysis of Secure Information Flow -- 6.2.6 Correctness of Analysis -- Noninterference Property -- 6.2.7 Analyses for Extensions of Core Language -- 6.3 A SEMANTIC APPROACH TO ANALYSIS OF SECURE INFORMATION FLOW -- 6.3.1 Motivation -- 6.3.2 Relational Semantics -- 6.3.3 Safe Abstractions of Security -- 6.3.4 Weakest Preconditions -- 6.3.5 Deterministic Programs -- 6.3.6 Partial Correctness Proofs -- 6.3.7 Verifying and Refuting Program Security -- 6.3.8 A Safe Abstraction -- 6.4 PROGRAM CERTIFICATION -- 6.5 COVERT CHANNELS -- 6.6 BIBLIOGRAPHIC NOTES -- APPENDIX Primitive Roots -- A.1 EXISTENCE OF PRIMITIVE ROOTS -- A.2 COMPUTING PRIMITIVE ROOTS -- Bibliography -- Index.