Information Technology and Electrical Engineering Doctoral Programme
Date: October 04, 2017
Room: Tellus Arena Frost Club
Date: October 05, 2017
Room: Tellus Arena Aspire
The objective of this course is to give the basic knowledge and the tools of formal verification applied to security protocols. Protocols describe how communication between computers takes place. While some protocols are simple enough to be written down in a few lines, designing correct protocols is notoriously hard.
The goal is to discuss the good design of secure protocols, common kinds of attacks on protocols and how to detect and stop these attacks. Methods for verifying protocols such as deductive-reasoning and model checking are presented and the tools that can be used to automate the formal analysis of protocols are introduced. This course focuses in particular on an automated logic-based technique (deductive-reasoning method) developed by the lecturer Dr. Anca Jurcut et al. at the University of Limerick and University College Dublin in Ireland.
- Security Protocols Design and Analysis
- Formal Verification Techniques
- Automated Verification Techniques
- CDVT/AD Tool Logic - based Verification Technique
- Practical Training: Using CDVT/ AD tool to detect and stop attacks
The students will be given a list of simple security protocols and asked to formal verify these protocols and submit a report.
Credits: 3 ECTS
Anca Jurcut graduated from West University of Timisoara, Romania in 2007 with first class honours Bachelor in Computer Science and Mathematics and she received her Ph.D in Security Engineering from University of Limerick in 2013. After graduation, she has been working as a postdoctoral researcher at University of Limerick and as a Software Engineer in IBM in Dublin. She is currently an Assistant Professor in School of Computer Science at University College Dublin (UCD). Her research interests include Security Protocols Analysis, Mathematical Modelling, Automated Techniques for Formal Verification, Theorem Proving Techniques, Computer Algorithm, and Cryptography. Much of her work has focused on formal verification techniques for security protocols using deductive reasoning methods (modal logics and theorem proving); automation of logics for formal verification; the development of new logic-based techniques and tools for formal verification; the design and analysis of security protocols; formalisation and modelling of design requirements for security protocols, as well as their network environment into a logic theory and the design of formal specification languages for security protocols.
Last updated: 15.9.2017