ISA 763 Security Protocol Verification - Fall 2013
Description
Teaches how to design, understand, verify, and test communication protocols so they meet their objectives of recognizing the basic components of a communication protocol. These include specifying security properties accurately, modeling actors and malefactors against which a protocol ought to be secure and discussing verification and testing methods, including their limitations. This is a graduate level class where we read many papers and apply their methods to model and verify the properties of protocol that are being used today.
Time permitting, this year's class will focus on the following topics
- Specifying components of protocols using CSP (Casper and FDR) and Pi (Spi and Applied Pi) calculus
- Composing Security properties using Protocol Composition Logic
- Formal basis for Trusted Computing:Protocols and Correctness arguments.
- Comparison between formal and computational models of cryptographic protocols
Textbook
- Title: The modeling and analysis of security protocols: The CSP Approach
- Authors: P.Y.A. Ryan, S.A. Schneider, M.H. Goldsmith, G. Lowe and A.W. Roscoe
- Available at CSP Text
- Many other (parts of) textbooks and papers will be assigned as reading as the class progresses.
- All relevant material, including papers and powerpoint presentations and other material will be distributed
- Follow the GMU blackboard page for the class closely
Class Details
- Section 01:
- Class Times: Thursdays 7.20-10.00 pm
- Location: Innovation Hall 136
Personnel
Instructor
- Name: Duminda Wijesekera
- Contact Email: dwijesek (at) gmu (dot) edu
- Contact Phone: 703-993-5030
- Office Hours: Thursdays 5.00-6.30 pm, after class and by appt.
- Office Location: Room 436, Research Building
- Best way to ask for help: email the instructor
Course Assistance
- No teaching assistants
- Will list some advanced graduate students who can help with your projects
- Office hrs: TBD
- Office Location: TBD
Syllabus
| Topic |
Week |
| Introduction |
1 |
| Casper, Introduction to CSP |
2 |
| More CSP and FDR |
3-6 |
| Mobile Processes, Pi Calculus and ProVerif |
7-8 |
| Protocol Composition Logic |
9-10 |
| Trusted Computing |
7-9 |
| Comparing Formal and Computational Models |
10 |
Evaluation Criteria
| 4 Projects (require writing some code) |
60% |
| 3 Homework (related to the projects) |
40% |
Notes
- Home-works and projects may be done in groups of 2-3 students.
- The 4 project are in Casper, Google's GO programming Language, FDR and ProVerif
- The 3 home-works are on CSP, Pi Calculus and Trusted Computing
Honor Code
All violations are reported. GMU honor code