- Example 1: Introduction to basic security properties.
- Example 2: Analysis of Attacks
- Example 3: Data Encryption Standard
- Example 4: Using Crypto Algorithms
- Example 4a: Attacks on Message Integrity Codes Computed Using Cipher Block Chaining
- Example 5: Public Key Algorithms
- Example 6: BAN Logic for Protocol Verification
- Example 6a: A Logic for Authentication and Access Control in Distributed Systems
- Example 6b: Encryption Channels
- Example 6c: Certificates & Authentication
- Example 6d: Access Control
- Example 6g: Interprocess Communication
- Example 7: Defining Types
- Example 8: Simple Email Example
- Example 11: Role-Based Access Control
Back to table of contents
- Example 1: Secret Codes introduces notions of
- Privacy
- Authenticity
- Integrity
Back to Examples
- Example 2: Analysis of Attacks shows how predicate calculus is used to analyze the three problems at the end of Chapter 2 in the course text.
- Example 3: Data Encryption Standard is a detailed analysis of DES in predicate calculus.
- Example 4: Using Crypto Algorithms shows how DES is used in electronic code book and cipher block chaining.
- Example 4a: Attacks on Message Integrity Codes Computed Using Cipher Block Chaining (This file is temporarily unavailable) shows how CBC-MICs are vulnerable. It also show how this weakness is exploited in multi-destination electronic mail.
- Example 5: Public Key Algorithms describes modular arithmetic and public key crypto algorithms.
- Example 6: BAN Logic for Protocol Verification introduces concepts of key distribution and authentication protocols. The belief logic developed by Burroughs, Abadi, and Needham (BAN Logic) is introduced and applied to the Otway-Rees key distribution protocol.
- Example 6a: A Logic for Authentication and Access Control in Distributed Systems (Under Development) introduces the syntax and semantics of a logic for authentication and access control in distributed systems. The logic is developed by Lampson, Abadi, Burroughs, and Wobber. The logic is used to reason about authenticating principals and keys, access control, and delegation. It is a way to reason about trust topologies and digital certificates (e.g., X.509).
- Example 6b: Encryption Channels illustrates how encryption channels using symmetric (secret) key algorithms and asymmetric (public) key algorithms are described using the authentication logic of Example 6a. In particular, it shows how to reason about certificate authorities and key distribution centers.
- Example 6c: Certificates and Authentication illustrates how to reason about digital certificates (e.g., X.509 certificates), trust models and topologies. In particular, we look at establishing trust in the context of multiple certification authorities.
- Example 6d: Access Control (Under development) shows how to use the logic of Lampson, Abadi, Burrows, and Wobber to reason about access control and access control lists.
Example 6g: Interprocess Communication is a detailed example of how communication channels and credentials are established between a client workstation and a file server. The example starts with how an operating system is loaded securely to how an access control decision is made for a file access request by an application program.
- Example 7: Defining New Types illustrates how new abstract data types are introduced into our logic. This allows us to reason about the properties of concrete data structures in ways that guarantee our implementations satisfy our specifications.
- Example 8: Simple Email Example shows how to reason about the correctness of a particular message structure using the type theory in Example 7.
- Example 11: Role-Based Access Control illustrates how roles as aggregations of privileges can simplify the assignment of privileges to users.
Updated 2 October 2002