Viinistu, Estonia, March 3 - 6, 2025
Professor at DMIF, University of Udine, Italy
The inherent complexity of modern information systems, arising from composition of concurrent, distributed, and heterogeneous components, poses significant challenges to security and analysis. In this course we examine the role of formal methods in developing models and tools suitable for rigorous verification, with a focus on the concepts of composition and interface.
The course is divided into two parts. First, we introduce ProVerif, a leading automatic cryptographic protocol verifier within the formal Dolev-Yao model. We then present a methodology for formally modeling and verifying multi-factor authentication (MFA) schemes, using eIDAS digital identity cards as a practical example. This methodology employs an interface-based threat model to comprehensively analyze potential vulnerabilities and enumerate threat scenarios based on attacker's capabilities. Using Italy's CIE (Carta d'Identit? Elettronica) as a case study, we demonstrate how to automatically generate ProVerif models of these scenarios, revealing vulnerabilities. We propose and formally verify minor protocol modifications to address these vulnerabilities.
The second part of the course focuses on containerized systems, the foundation of modern service-oriented architectures. We present a formal model for these systems based on Bigraphical Reactive Systems (BRSs). This formal representation facilitates the analysis and manipulation of containerized systems using graph-theoretic techniques. Finally, we introduce DBCChecker, a prototype tool that, given descriptions of container interfaces, behaviors, and compositions, constructs a formal model analyzable by ProVerif, enabling the verification of critical security properties like integrity and confidentiality.
Last changed
March 4, 2025 12:14 EET (GMT +02:00)
by local organisers