- Summer school: Formal methods for Information Security
Summer school: Formal methods for Information Security
- 18-20 June, 2025
- Tarragona (Spain)
Confirmed speakers
- Prof. Achim D. Brucker, University of Exeter
- Prof. Santiago Escobar, Universitat Politècnica de València
- Dr. Ross Horne, University of Strathclyde
- Prof. Sjouke Mauw, University of Luxembourg
- Prof. Sasa Radamirovic, Heriot-Watt University
- Dr. Felix Stutz, University of Luxemburg
- Dr. Rolando Trujillo, Universitat Rovira i Virgili
- Prof. Tim Willemse, Eindhoven University of Technology
Program
The three-day program is taught in English and consists of keynotes and tutorials.| Day 1 (Wednesday) | Day 2 (Thursday) | Day 3 (Friday) | |
|---|---|---|---|
| 08:15 – 08:45 | Registration | ||
| 08:45 – 09:00 | Presentation | ||
| 09:00 - 10:30 | Keynote by Prof. Achim D. Brucker. “Formal Verification and AI Safety” | Keynote by Dr. Ross Horne. “How can we avoid conflicts of interest?” | Keynote by Prof. Sjouke Mauw. “Distance-bounding protocols: a gentle introduction” |
| 10:30 - 11:00 | Coffee Break | ||
| 11:00 - 12:30 | Keynote by Prof. Sasa Radomirovic. “Modelling with Account Access Graphs” | Keynote by Dr. Rolando Trujillo. "Memory erasure protocols for low-cost IoT devices" | Keynote by Prof. Santiago Escobar. "Protocol Analysis using Maude-NPA" |
| 13:00 - 14:30 | Lunch Break | ||
| 14:30 - 16:00 | Tutorial by Dr. Felix Stutz on “Formal Verification of Security Protocols using ProVerif” (Part 1) | Tutorial by Prof. Tim Willemse on “Formal Verification of Systems using mCRL2” (Part 1) | |
| 16:00 - 16:30 | Coffee Break | ||
| 16:30 - 18:00 | Tutorial by Dr. Felix Stutz on “Formal Verification of Security Protocols using ProVerif” (Part 2) | Tutorial by Prof. Tim Willemse on “Formal Verification of Systems using mCRL2” (Part 2) | Social Activity (Paddle surf, Kayak) at "Reial Club Nàutic de Tarragona" (until about 18h30) |
| 18:15 - 20:15 | Visit tour from "El Seminari" | ||
| 20:30 - 22:30 | Joint dinner at the "Filosofia Restaurant" | ||
Abstracts and bios
Achim D. Brucker
Talk Title: Formal Verification of AI for Safety and Security Abstract: Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural networks are susceptible if small changes applied to their input result in misclassification. Situations in which such a slight input change, often hardly noticeable by a human expert, results in a misclassification are called adversarial attacks. Such attacks can be life-threatening if, for example, they occur in image classification systems used in autonomous cars or medical diagnosis. Systems employing neural networks, e.g., for safety or security critical functionality, are a particular challenge for formal verification, which usually expects a program or algorithm that can be analyzed. Such a program or algorithm does, per se, not exist for neural networks. In this talk, I will start with an introduction into the area of formal verification of systems based on machine learning in general, and neural networks in particular. After that, I will present our ongoing work in developing a verification approach for neural networks in Isabelle/HOL. This is joint work with Amy Stell (University of Exeter, UK). Bio: Achim D. Brucker, Professor in Computer Science (Chair in Cybersecurity) and Head of the Cybersecurity Group at the University of Exeter, UK. He has over 20 years of professional experience in cybersecurity in general, and, in particular, in research and development of safety and security critical systems. In his work, he particularly focuses on techniques, methods, and tools for ensuring the safety, security, correctness, and trustworthiness of advanced systems. His industry experience includes being a Security Architect and Security Testing Strategist for SAP SE. In this role, he defined the risk-based security testing strategy of SAP that combines static, dynamic, and interactive security testing methods and integrates them deeply into SAP Secure Software Development Life Cycle. He also led the team implementing this new security testing strategy across all development locations of SAP world-wide effort supporting over 25000 developers. He continues to work closely with industry, e.g., as technical advisor and member of the Advisory Board of Anzen Technology Systems Ltd. His research interests cover broad areas of Formal Methods (Verification, Computational Logic), Cybersecurity (including Privacy, Information Security, Software Security, Hardware Security), and Software Engineering (e.g., Program Verification, Semantics of Programming or Specification Languages). He is interested in both, theoretical/foundational and applied research and innovation. His work experience in both industry and academia reflects his unique combination of applied and theoretical work. He is supporting security initiatives and events that build bridges industry, academia, and local communities. Amongst others, he is a member of the Steering Committees of the South West Cyber Security Cluster and BSides Exeter.Sasa Radomirovic
Talk title: Formal Modeling with Account Access Graphs Abstract: An account ecosystems is a user's or organisation's collection of digital assets, accounts, apps, devices, and their interconnections. The presence of some combinations of these interconnections has been exploited in attacks that range from account takeovers to cryptocurrency theft, while the absence of other combinations has led to the inadvertent loss of access to crucial accounts and crypto wallets. The industry influences the connectivity between accounts, apps, and devices by introducing or removing specific access methods to accounts, such as various authentication and account recovery options. Users build their account ecosystems by strategic, guided or careless choice of these access methods and their connections. Each user and organisation has thus a unique, complex and constantly evolving account ecosystem. This poses a significant challenge for the protection of their digital assets. Account access graphs are a formal model to represent a user's or organisation's account ecosystem. In this presentation I will show how to model account ecosystems with account access graphs and several methods to analyse their integrity and availability properties under different threat models. Bio: Sasa Radomirovic is a Professor of Computer Science at Heriot-Watt University. He was previously at the University of Surrey, the University of Dundee, and ETH Zurich. He received a PhD in number theory from Rutgers University, USA and worked as a postdoc at NTNU Norway, CRM Barcelona, and the University of Luxembourg. His research is on formal modeling and verification in cyber security with a focus on cryptographic protocols, threat modeling, and authentication.Felix Stutz
Tutorial title: Formal Verification of Security Protocols using ProVerif Abstract: Security protocols are crucial in our modern world, underpinning virtually all computer network communication. Hence, it is not only important to properly design such protocols but to verify their correctness. Since pen-and-paper proofs are often error-prone or infeasible, the need for greater assurance has driven the development of automated security protocol verification tools. This tutorial provides an introduction to modelling and verifying security protocols - with practical application to ProVerif, a mature tool in this space. For example, using the tool's feedback, we will iteratively design security protocols to satisfy key properties such as authentication, deriving general design principles along the way. Bio: Felix Stutz is a postdoctoral researcher in the Security and Trust of Software Systems group at the University of Luxembourg. His main research focuses on formal methods for message-passing programs and security protocols. He conducted his doctoral research at the Max Planck Institute for Software Systems and obtained his PhD from the University of Kaiserslautern-Landau. Felix holds a Master's degree from Saarland University and has undertaken research internships at MIT CSAIL and Imperial College London.Ross Horne
Talk Title: How can we avoid conflicts of interest? Abstract: Ethical security policies ensure confidentiality properties that respect conflicts of interest. They pre-dates computerised systems, for example, Chinese Walls are used to avoid insider trading. Still today, insider trading is a major issue with companies fined hundreds of millions of Euros in 2024 alone. Conflicts of interests can also arise in computer systems such as Cloud computing and other decentralised architectures, where multiple organisations share infrastructure and resources. A famous paper by Brewer and Nash proposed a formal security policy model inspired by ethical Chinese Wall policies, where a policy model ensures that security policies that conform to the model guarantee the security properties of the model. The semantics for the Brewer-Nash model was however underspecified, leaving scope for multiple interpretations of what accesses are permitted and what the intended security goals are. We have addressed this by developing a formal model by scrutinising the proposal of Brewer and Nash. An interesting feature of these models is that write access can be revoked when a subject (the entity accessing data) reads too much information. I'll argue that this problem is too important to be left underspecified and that our methodology can bring more confidence and flexibility to policies while respecting conflicts of interest. Bio: Dr. Ross Horne is a Senior Lecturer in the Department of Computer & Information Sciences at the University of Strathclyde, Glasgow. They are affiliated with the StrathCyber and Mathematically Structured Programming (MSP) research groups. Their research focuses on the security and privacy of communication protocols in digital society, particularly where it is unclear whether attackers can manipulate systems, for example, to impersonate users or infer sensitive behavior. They use formal threat models and logical methods to identify and mitigate such risks. Beyond protocol analysis, Dr. Ross Horne is broadly interested in interdisciplinary methods for understanding cyber threats, and has contributed to concurrency theory as a foundation for reasoning about distributed and multi-party systems.Rolando Trujillo Rasua
Title: Memory erasure protocols for low-cost IoT devices Abstract: A Proof of Secure Erasure (PoSE) is a communication protocol where a verifier seeks evidence that a prover has erased the memory on a given device within the time frame of the protocol execution. This talk is an introduction to PoSE protocols, their analysis, and their performance in a practical setting. Bio: Dr. Rolando Trujillo Rasua a Ramon y Cajal is a researcher at Rovira i Virgili University (URV) and a multiple medallist in Mathematical Olympiads. Prior to joining the URV, he held a senior lecturer position at Deakin University (Australia) and a postdoctoral position at the University of Luxembourg. His work appears in the most important publication venues in computer security, such as ACM CCS, S&P, ESORICS and CSF, and his research interests span the areas of formal methods, computer security and privacy protection.Tim Willemse
Tutorial title: Formal Verification of Systems using mCRL2 Abstract: Software can be very tricky to implement correctly as there often are many possible execution orders due to concurrency. Modelling and analysing the software using model checking can help to quickly identify and fix issues that would otherwise be hard to detect and sometimes hard to reproduce. In this tutorial we introduce process algebras and their underlying theory for reasoning about software behaviour, and modal logics such as Hennessy-Milner logic and the modal mu-calculus to reason about the behaviour. In particular, we will use the mCRL2 language and toolset, which is open source and has no restrictions on its use (see https://mcrl2.org), and show how the toolset and its languages can be used to analyse problems of various sizes and complexity. Bio: Tim Willemse is an Associate Professor and chair of the "Formal System Analysis" group of the Department of Mathematics and Computer Science at Eindhoven University of Technology (TU/e). Tim obtained his PhD (TU/e) in 2003. His research focusses on applying, developing and scaling formal methods for designing correct and reliable systems. His research receives financial support from organisations such as NWO and the European Commission, and commercial parties, including ASML and Canon Production Printing.Sjouke Mauw
Talk Title: Distance-bounding protocols: a gentle introduction Abstract: What do traditional keys, train tickets and coins have in common? They are increasingly being replaced by digital solutions, such as electronic car keys, smart tickets and contactless payment systems. Unfortunately, various physical properties that are easily verified in the traditional setting are significantly harder to achieve in the digital world. An example is the proximity of a lock and its key. In the physical world, in order to open a lock, the key needs to be physically inserted into it. However, proximity is much harder to ensure using digital means only, because digital communications can be easily relayed over large distances. A special class of security protocols, called distance-bounding protocols are the computer scientist's answer to such relay attacks. Bio: Sjouke Mauw is full professor and head of the SaToSS research group on Security and Trust of Software Systems at the University of Luxembourg. Until 2007 he worked at the Eindhoven University of Technology and at CWI (Center of Mathematics and Computer Science) in Amsterdam. His research focuses on formalising and applying formal reasoning to real-world security problems and trust issues.Santiago Escobar
Title: Protocol Analysis using Maude-NPA Abstract: In this course we give an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the symbolic analysis of cryptographic protocols. It searches backwards from an insecure pattern configuration and it is able to find an attack, given enough resources, or prove the absence of any attack, when the search space is finite, which happens quite often thanks to many optimisation techniques. Several properties can be checked with Maude-NPA: secrecy, authentication, and indistinguishability for an active Dolev-Yao intruder model and an unbounded number of sessions. Maude-NPA takes into account the algebraic properties of the crypto systems involved (e.g., exclusive-or, Diffie-Hellman, Bilinear Pairings, etc.) in order to give a more complete representation of both the protocol and the attackers capabilities. During the development of the tool we have also defined new theoretical and practical frameworks such as variant-based unification, logical model checking, asymmetric unification, or state-space optimisations that will be presented during the course. Maude-NPA has been recently extended to handle properties checked using SMT solvers: such as time and space constraints. Bio: Santiago Escobar is a Full Professor at the Universitat Politècnica de València, where he earned his PhD in Computer Science in 2003. He is a leading researcher in program verification, cybersecurity, and protocol analysis, with over 100 publications and extensive involvement in international conferences. He has supervised five PhD theses and over 50 undergraduate and master's projects. Prof. Escobar is a long-time contributor to the Maude-NPA cryptographic protocol analyzer, developed with collaborators from the US Navy and the University of Illinois. He is also part of the Maude programming language team, used by organizations such as NASA and Microsoft for safety-critical verification. His applied cybersecurity work includes collaborations with Stadler Rail, Nunsys, and Laberit, as well as active involvement in the Spanish cybersecurity research network RENIC. He has held visiting positions in the US, Europe, and Asia, and collaborates with institutions including JAIST, NASA Langley, SRI International, ETH Zurich, POSTECH, and the University of Oslo.Before the summer school
Don't forget to bring your laptop for the afternoon tutorial sessions.Tutorial: Modelling and Verifying Security Protocols with ProVerif
As the title suggests, we will work with ProVerif, a security protocol verification tool, during this tutorial. We would kindly ask you to install the software on your computer before the summer school so that we do not need to waste time on installation issues. The software can be found on this website under the section 'Downloads'. Make sure that the commandproverif is accessible from any folder (or at least from the ones where you will work on later). In many systems, you will need to update your PATH variable.
To test your installation, you can find a protocol specification in the source code under examples/pitype/secr-auth. After unpacking, for instance, execute the following:
proverif DenningSacco.pv
Confirm the expected outputs:
Verification summary:
Query not attacker(secretA[]) is true.
Query not attacker(secretB[]) is false.
Query inj-event(endBparam(x,y)) ==> inj-event(beginBparam(x,y)) is false.
Query inj-event(endBkey(x,y,z)) ==> inj-event(beginBkey(x,y,z)) is false.
Tutorial: Formal Verification of Systems using mCRL2
Please, install the mCRL2 toolset (Release 202407.1). See https://mcrl2.org/web/home/download.htmlRegistration
Tuition fee
- 100 EUR for early registrations (before June 4, 2025)
- 200 EUR for late registrations (after June 4, 2025)
Cancellations
Cancellation requests should be sent by e-mail to congressos@fundacio.urv.cat.- Cancellation requests received up to and including 06/06/2025: the registration fee will be refunded. The Congress Office will retain 10% of the registration fee as a handling fee.
- Cancellation requests received after, the registration fee will not be refunded.
Venue
The workshop will be held at the “Centre Tarraconense El Seminari”, located in the old town of Tarragona, close to the Cathedral. Address: C/ Sant Pau 4 — 43003 — Tarragona. Tarragona is a beautiful city on Spain’s Mediterranean coast, full of history and amazing places to visit. Located in the south of Catalonia, its Roman ruins, like the amphitheatre right by the sea, are a UNESCO World Heritage Site and a must-see. The city also has fantastic beaches, a lovely old town with narrow streets and cozy squares, and delicious food, especially fresh seafood and local wines.How to arrive
The closest big airport is Barcelona-El Prat (BCN), located just 85 kilometres away. The bus is the most convenient way to get from the Airport to Tarragona. The current timetable offers a direct bus from Barcelona airport to Tarragona almost every hour. Tickets cost €15.95 one way. The company operating this bus line is Bus Plana. Taxis are always available just outside the arrival area of the airport. The current price is around 130 Euros. Please, confirm this price with the taxi driver before starting your trip. If you’re already in Barcelona, regional trains from Sants station get you to Tarragona centre in one hour. However, due to scheduled work on the railways, this service may experience significant disruptions. For this reason, we recommend taking a high-speed train although they don't stop in the city centre but at the Camp de Tarragona station. From there you can take a taxi to Tarragona (20 minutes and 30 euros approx.) or the bus transfer.Contact Us
For more information, please email depeng.chen@fundacio.urv.cat.FAQ
- What criteria are used to select participants? Participants are selected based on their background and academic level. Preference is given to those who are studying or have experience in the topic of the Summer School. A basic understanding of the field is required, and early-stage Bachelor’s students may not be eligible. This ensures active participation in the interactive sessions.
- What if I have dietary restrictions? Please include any dietary needs in your application. We will do our best to accommodate them, and a vegetarian option will always be available.
- What should I bring? Bring your own laptop. Course materials and meals are provided as part of the fee. You will also receive presentations and handouts from speakers after the event.
- Will I receive a certificate of participation? Yes, a certificate will be issued to participants who attend all days of the Summer School.
- What if I need to cancel my participation? Refunds are not available if you cancel after confirming and paying. However, you can nominate a substitute with similar qualifications. Refunds may be possible if there’s enough time to adjust event plans (e.g., transport and catering).
