| |
Course Syllabus
Course goals:
The goals of the course are a theoretical knowledge of formal methods in security, together with
knowledge of the most important case studies in the field.
Student Work:
- Homework will consist of regular written exercises and some programming problems.
- Students will also present tutorials on the various formal security specification
languages available. Other work may include a final term paper.
- Tests: There will be one midterm and one final exam, both in class.
Grades:Will be calculated from grades received for the tests (25% each),
homework assignments (20%), and research work (30%).
Topics
Week 1: Mathematical preliminaries: prepositional logic, predicate logic;
Mathematical preliminaries: model logic
Week 2: Formal systems intro: formal languages with well-defined syntax,
semantics; proof systems
Week 3: Implementations built on formal systems;
Motivation: increases reliability, reveals ambiguities, mistakes;
Formal specifications: operational, denotational, axiomatic, model-oriented,
and property-oriented
Week 4: Program Verification: partial correctness, total correctness, Hoare's rules
Week 5: Real world issues
Week 6: Temporal logic and specifications: formal semantics
Week 7: Computation tree logic
Week 8: Security overview: risks, types of threats, vulnerabilities, trust, security
needs, policy; Encryption, hashes and MACs, authentication
Week 9: Formal security models: finite state machine, lattice, access matrix, security
kernel, info-flow
Week 10: Take-grant model; Bell-LaPadula
Week 11: Specification languages: general properties, goal
Week 13: Knowledge logic: BAN
Week 13: Process theory: Spi-calculus, Strands, MSR, FDR Casper, Petri nets
Week 14: Inductive methods: temporal logic, automata: CAPSL, NRL, Murf
Week 15: Review; Student discussion on term papers.
Basic Bibliography
Primary text: none
Primary bibliographic sources:
- C. E. Landwehr. A Survey of Formal Models for Computer Security. Naval Research
Laboratory NRL Report 8489, 1981.
- AD Gordon, M Abadi, A Calculus for Cryptographic Protocols: The Spi Calculus, 4th
ACM Conference on Computer and Communications Security, 1997.
- M Burrows, M Abadi, RM Needham. A Logic of Authentication, DEC SRC Research Report 39,
- J. M. Wing. A Symbiotic Relationship Between Formal Methods and Security. Proceedings
from Workshops on Computer Security, Fault Tolerance, and Software Assurance: From Needs to
Solution. Technical report CMU-CS-98-188, 1998.
Secondary bibliographic sources:
- Bruce Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C
(2nd ed). John Wiley & Sons, 1996.
- William Stallings. Cryptography and Network Security: Principles and Practice (2nd ed).
Prentice Hall, 1999.
- Charlie Kaufman, Radia Perlman, Mike Speciner. Network Security: Private Communication
in a Public World. Prentice Hall, 1995.
|
|
|