Ivan Kurtev

Leonard Tudorache, Ivan Kurtev, Mark van den Brand

Security is critical for everything relying on modern digital systems. Because almost all digital interactions are governed by the Internet and cryptographic protocols, these protocols must serve as reliable mechanisms that guarantee core security properties, such as confidentiality and integrity. Formal verification of these protocols is a critical step in securing interconnected systems. Tools such as ProVerif and Tamarin are widely employed to perform automated verification. However, their effective use demands specialized domain knowledge, creating a significant learning curve for security protocol designers who often have a security, rather than a formal verification background. We therefore need structured, accessible resources to help protocol designers to express their design and requirements in the language of the formal verification tools. To address this, we introduce a systematic and evidence-based taxonomy of security properties. This taxonomy is derived from a literature review of 53 recent studies (2022-2025) that used ProVerif and Tamarin, providing an up-to-date view of verified properties. We systematically categorize and define these properties, providing both informal definitions for intuitive comprehension and rigorous formal definitions expressed in first-order logic for clarity and consistency. We further detail modeling patterns and implement executable examples in both ProVerif and Tamarin, collected in an open repository. This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models.

Arda Goknil, Ivan Kurtev, Klaas van den Berg

Software systems usually operate in a dynamic context where their requirements change continuously and new requirements emerge frequently. A single requirement hardly exists in isolation: it is related to other requirements and to the software development artifacts that implement it. When a requirements change is introduced, the requirements engineer may have to manually analyze all requirements and architectural elements for a single change. This may result in neglecting the actual impact of a change. We aim at improving change impact analysis in software architecture for requirements changes by using formal semantics of requirements relations, requirements changes and traces between Requirements & Architecture. In our previous work we presented a technique for change impact analysis in requirements. The technique uses the formal semantics of requirements relations and changes. Its output is a set of candidate requirements for the impact with proposed changes and a propagation path in the requirements model. In this paper we present a complementary technique which propagates requirements changes to software architecture and finds out which architectural elements are impacted by these changes. The formalization of requirements relations, changes and traces between R&A is used to determine candidate architectural elements for the impact of requirements changes in the architecture. The tool support is an extension of our Tool for Requirements Inferencing and Consistency Checking (TRIC). Our approach helps in the elimination of some false positive impacts in change propagation. We illustrate our approach in an industrial example which shows that the formal semantics of requirements relations, changes and traces enables the identification of candidate architectural elements with the reduction of some false positive impacts.