Dr Sasa Radomirovic

Account access graphs have been proposed as a way to model relationships between user credentials, accounts, and methods of access; they capture both multiple simultaneous access routes (e.g., for multi-factor authentication) as well as multiple alternative access routes (e.g., for account recovery). In this paper we extend the formalism with state transitions and tactics. State transitions capture how access may change over time as users or adversaries use access routes and add or remove credentials and accounts. Tactics allow us to model and document attacker techniques or resilience strategies, by writing small programs. We illustrate these ideas using some attacks against mobile authentication and banking applications which have been publicised in 2023.

We develop and explain the design decisions of a framework for the formal specification and analysis of interactions in generalized distributed systems. Our approach is suitable to reason about various types of agents and supports the modeling of synchronous interactions between any finite number of agents. Our proposal provides a common ground for existing modeling techniques for cryptographic protocols and security ceremonies, by generalizing and unifying them in a single formalism. We discuss the specification of security properties in our framework and demonstrate on a short voting ceremony a technique to model our ceremonies in the Tamarin prover.

Multi-party contract signing protocols specify how a number of signers can cooperate in achieving a fully signed contract, even in the presence of dishonest signers. This problem has been studied in different settings, yielding solutions of varying complexity. Here we assume the presence of a trusted third party that will be contacted only in case of a conflict, asynchronous communication, and a total ordering of the protocol steps. Our goal is to develop a lower bound on the number of messages in such a protocol. Using the notion of abort chaining, a specific type of attack on fairness of signing protocols, we derive the lower bound alpha(2) + 1, with alpha > 2 being the number of signers involved. We obtain the lower bound by relating the problem of developing fair signing protocols to the open combinatorial problem of finding shortest permutation sequences. This relation also indicates a way to construct signing protocols which are shorter than state-of-the-art protocols. We illustrate our approach by presenting the shortest three-party fair contract signing protocol.

Cryptographic protocols are the backbone of secure communication over open networks and their correctness is therefore crucial. Tool-supported formal analysis of cryptographic protocol designs increases our confidence that these protocols achieve their intended security guarantees. We propose a method to automatically translate textbook style Alice&Bob protocol specifications into a format amenable to formal verification using existing tools. Our translation supports specification modulo equational theories, which enables the faithful representation of algebraic properties of a large class of cryptographic operators.

We discuss a recently proposed formal proof model for RFID location privacy. We show that protocols which intuitively and in several other models are considered not to be location private, are provably location private in this model. Conversely, we also show that protocols which obviously are location private, are not considered location private in this model. Specifically, we prove a protocol in which every tag transmits the same constant message to not be location private in the proposed model. Then we prove a protocol in which a tag's identity is transmitted in clear text to be weakly location private in the model. (C) 2009 Elsevier B.V. All rights reserved.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in Rill) protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The TAMARIN prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. Previous approaches considered either completely linear protocols or fully parallel broadcasting protocols. We introduce the new class of DAG MPCS protocols which combines parallel and linear execution and allows for parallelism even within a signer role. This generalization is useful in practical applications where the set of signers has a hierarchical structure, such as chaining of service level agreements and subcontracting. Our novel DAG MPCS protocols are represented by directed acyclic graphs and equipped with a labeled transition system semantics. We define the notion of abort-chaining sequences and prove that a DAG MPCS protocol satisfies fairness if and only if it does not have an abort-chaining sequence. We exhibit several examples of optimistic fair DAG MPCS protocols. The fairness of these protocols follows from our theory and has additionally been verified with our automated tool. We define two complexity measures for DAG MPCS protocols, related to execution time and total number of messages exchanged. We prove lower bounds for fair DAG MPCS protocols in terms of these measures.

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.

We present a novel approach for automatic repair of corrupted files that applies to any common file format and does not require knowledge of its structure. Our lightweight approach modifies the execution of a file viewer instead of the file data and makes use of instrumentation and execution hijacking, two techniques from software testing. It uses a file viewer as a black box and does not require access to its source code or any knowledge about its inner workings. We present our implementation of this approach and evaluate it on corrupted PNG, JPEG, and PDF files.

We discuss insider attacks on RFID protocols with a focus on RFID tag privacy and demonstrate such attacks on published RFID protocols. In particular, we show attacks on a challenge-response protocol with IND-CCA1 encryption and on the randomized hashed GPS protocol. We then show that IND-CCA2 encryption can be used to prevent insider attacks and present a protocol secure against insider attacks. The protocol is based solely on elliptic-curve operations.

Attack-defense trees are a novel methodology for graphical security modelling and assessment. They extend the well- known formalism of attack trees by allowing nodes that represent defensive measures to appear at any level of the tree. This enlarges the modelling capabilities of attack trees and makes the new formalism suitable for representing interactions between an attacker and a defender. Our formalization supports different semantical approaches for which we provide usage scenarios. We also formalize how to quantitatively analyse attack and defense scenarios using attributes.

We give an intuitive formal definition of untraceability in the standard Dolev-Yao intruder model, inspired by existing definitions of anonymity. We show how to verify whether communication protocols satisfy the untraceability property and apply our methods to known RFID protocols. We show a previously unknown attack on a published RFID protocol and use our framework to prove that the protocol is not untraceable.

We report on the security claims of an RFID authentication protocol by Li and Ding which was specifically designed for use in supply chains. We show how the protocol's vulnerabilities can be used to track products, relate incoming and outgoing products, and extort supply chain partners. Starting from a discussion of the relevant security requirements for RFID protocols in supply chains, we proceed to illustrate several shortcomings in the protocol with respect to mutual authentication, unlinkability, and desynchronization resistance. We investigate the use of the xor operator in the protocol, suggest possible improvements, and point out flaws in the proofs of the security claims.

Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.

We apply a graphical model to develop a digital loyalty program protocol specifically tailored to small shops with no professional or third-party-provided infrastructure. The graphical model allows us to capture assumptions on the environment the protocol is running in, such as capabilities of agents, available channels and their security properties. Moreover, the model serves as a manual tool to quickly rule out insecure protocol designs and to focus on improving promising designs. We illustrate this by a step-wise improvement of a crude but commercially used protocol to finally derive a light-weight and scalable security protocol with proved security properties and many appealing features for practical use.

We provide the first formal foundation of SAND attack trees which are a popular extension of the well-known attack trees. The SAND attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator SAND. This operator enables the modeling of ordered events. We give a semantics to SAND attack trees by interpreting them as sets of series-parallel graphs and propose a complete axiomatization of this semantics. We define normal forms for SAND attack trees and a term rewriting system which allows identification of semantically equivalent trees. Finally, we formalize how to quantitatively analyze SAND attack trees using attributes.

In random sample voting, only a randomly chosen subset of all eligible voters are selected to vote. This poses new security challenges for the voting protocol used. In particular, one must ensure that the chosen voters were randomly selected while preserving their anonymity. Moreover, the small number of selected voters leaves little room for error and only a few manipulations of the votes may significantly change the outcome. We propose Alethea, the first random sample voting protocol that satisfies end-to-end verifiability and receipt-freeness. Our protocol makes explicit the distinction between human voters and their devices. This allows for more fine-grained statements about the required capabilities and trust assumptions of each agent than is possible in previous work. We define new security properties related to the randomness and anonymity of the sample group and the probability of undetected manipulations. We prove correctness of the protocol and its properties both using traditional paper and pen proofs and with tool support.

The IT industry’s need to distinguish new products with new looks, new experiences, and new user interface designs is bad for cybersecurity. It robs users of the chance to transfer previously acquired security-relevant knowledge to new products and leaves them with a poor mental model of security. Starting from a comparison with physical safety, we explore and sketch a method to help users develop a useful mental model of security in cybersystems. A beneficial side-effect of our methodology is that it makes precise what security requirements the user expects the system to fulfill. This can be used to formally verify the system’s compliance with the user’s expectation.

We present, a, formal model for stateful security protocols. This model is used to define ownership and ownership transfer as concepts as well as security properties. These definitions are based oil an intuitive notion of ownership related to physical ownership. They are aimed at RFID systems, but should be applicable to any scenario sharing the same intuition of ownership. We discuss the connection between ownership and the notion of desynchronization resistance and give the first formal definition of the fatter. We apply our definitions to existing RFID protocols, exhibiting attacks oil desynchronization resistance, secure ownership, and secure ownership transfer.

This work aims to identify the algebraic problems which enable many attacks on RFID protocols. Toward this goal, three emerging types of attacks on RFID protocols, concerning authentication, untraceability, and secrecy are discussed. We demonstrate the types of attacks by exhibiting previously unpublished vulnerabilities in several protocols and referring to various other flawed protocols. The common theme in these attacks is the fact that the algebraic properties of operators employed by the protocols are abused. While the methodology is applicable to any operator with algebraic properties, the protocols considered in this paper make rise of xor, modular addition, and elliptic curve point addition.

Misuse case analysis is a method for the elicitation, documentation, and communication of security requirements. It builds upon the well-established use case analysis method and is one of the few existing techniques dedicated to security requirements engineering. We present an anti-pattern for applying misuse cases, dubbed "orphan misuses." Orphan misuse cases by and large ignore the system at hand, thus providing little insight into its security. Common symptoms include implementation-dependent threats and overly general, vacuous mitigations. We illustrate orphan misuse cases through examples, explain their negative consequences in detail, and give guidelines for avoiding them.

In the context of Dolev-Yao style analysis of security protocols, we investigate the security claims of a recently proposed RFID authentication protocol. We exhibit a flaw which has gone unnoticed in RFID protocol literature and present the resulting attacks on authentication, untraceability, and desynchronization resistance. We analyze and discuss the authors' proofs of security. References to other vulnerable protocols are given.

Verifiability is a key requirement for electronic voting. However, the use of cryptographic techniques to achieve it usually requires specialist knowledge to understand; hence voters cannot easily assess the validity of such arguments themselves. To address this, solutions have been proposed using simple tables and checks, which require only simple verification steps with almost no cryptography. This simplicity comes at a cost: numerous verification checks must be made on the tables to ensure their correctness, raising the question whether the success of all the small verification steps entails the overall goal of end-to-end verifiability while preserving vote secrecy. Do the final results reflect the voters' will? Moreover, do the verification steps leak information about the voters' choices? In this paper, we provide mathematical foundations and an associated methodology for defining and proving verifiability and voter privacy for table-based election protocols. We apply them to three case studies: the Eperio protocol, Scantegrity, and Chaum's Random-Sample Election protocol. Our methodology helps us, in all three cases, identify previously unknown problems that allow an election authority to cheat and modify the election outcome. Furthermore, it helps us formulate and verify the corrected versions.

We introduce derailing attacks, a class of blocking attacks on security protocols. As opposed to blunt, low-level attacks such as persistent jamming, derailing only requires a minimal, application-level intervention from the attacker. We give a simple definition of derailing attacks in an abstract formal model, and demonstrate that derailing attacks are viable in practice through examples from two application domains, namely radio-frequency identification and fair exchange protocols.

In cryptographic protocols, in particular RFID protocols, exclusive-or (XOR) operations are common. Due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. In this paper, we improve the TAMARIN prover and its underlying theory to deal with an equational theory modeling XOR operations. The XOR theory can be combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first verification tool for cryptographic protocols in the symbolic model to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

The primary authentication method for a user account is rarely the only way to access that account. Accounts can often be accessed through other accounts, using recovery methods, password managers, or single sign-on. This increases each account's attack surface, giving rise to subtle security problems. These problems cannot be detected by considering each account in isolation, but require analyzing the links between a user's accounts. Furthermore, to accurately assess the security of accounts, the physical world must also be considered. For example, an attacker with access to a physical mailbox could obtain credentials sent by post. Despite the manifest importance of understanding these interrelationships and the security problems they entail, no prior methods exist to perform an analysis thereof in a precise way. To address this need, we introduce account access graphs, the first formalism that enables a comprehensive modeling and analysis of a user's entire setup, incorporating all connections between the user's accounts, devices, credentials, keys, and documents. Account access graphs support systematically identifying both security vulnerabilities and lockout risks in a user's accounts. We give analysis algorithms and illustrate their effectiveness in a case study, where we automatically detect significant weaknesses in a user's setup and suggest improvement options.

Mankind is actively trying to communicate with extraterrestrial life. However, historically the discovery of new civilizations has led to war, subjugation, and even elimination. With that in mind, we believe that for any attempted contact with extraterrestrials our location must not be revealed. Therefore, we focus on the problem of location-private interstellar communication. We approach this as a security problem and propose to work towards solutions with tools from the domain of secure communications. As a first step, we give proposals for adversary models, security requirements, and security controls.

In voting, disputes arise when a voter claims that the voting authority is dishonest and did not correctly process his ballot while the authority claims to have followed the protocol. A dispute can be resolved if any third party can unambiguously determine who is right. We systematically characterize all relevant disputes for a generic, practically relevant, class of voting protocols. Based on our characterization, we propose a new definition of dispute resolution for voting that accounts for the possibility that both voters and the voting authority can make false claims and that voters may abstain from voting. A central aspect of our work is timeliness: a voter should possess the evidence required to resolve disputes no later than the election's end. We characterize what assumptions are necessary and sufficient for timeliness in terms of a communication topology for our voting protocol class. We formalize the dispute resolution properties and communication topologies symbolically. This provides the basis for verification of dispute resolution for a broad class of protocols. To demonstrate the utility of our model, we analyze a mixnet-based voting protocol and prove that it satisfies dispute resolution as well as verifiability and receipt-freeness. To prove our claims, we combine machine-checked proofs with traditional pen-and-paper proofs.

Establishing a secure communication channel between two parties is a nontrivial problem, especially when one or both are humans. Unlike computers, humans cannot perform strong cryptographic operations without supporting technology, yet this technology may itself be compromised. We introduce a general communication topology model to facilitate the analysis of security protocols in this setting. We use it to completely characterize all topologies that allow secure communication between a human and a remote server via a compromised computer. These topologies are relevant for a variety of applications, including online banking and Internet voting. Our characterization can serve to guide the design of novel solutions for applications and to quickly exclude proposals that cannot possibly offer secure communication.

Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible. In this paper, we provide a model for formalizing and reasoning about these inherent human limitations and their consequences. Specifically, we formalize models of fallible humans in security protocols as multiset rewrite theories. We show how the Tamarin tool can then be used to automatically analyze security protocols involving human errors. We provide case studies of authentication protocols that show how different protocol constructions and features differ in their effectiveness with respect to different kinds of fallible humans. This provides a starting point for a fine-grained classification of security protocols from a usable-security perspective.

Older adults are becoming more technologically proficient and use the internet to participate actively in society. However, current best security practices can be seen as unusable by this population group as these practices do not consider the needs of an older adult. Aim. We aim to develop a better understanding of digitally literate, older adults' online account management strategies and the reasons leading to their adoption. Method. We carry out two user studies (n = 7, n = 5). The first of these gathered information on older adults' account ecosystems and their current online security practice. In the second, we presented security advice to the same group of older adults facilitated by a bespoke web application. We used this to learn more about the reasons behind older adults' security practices by allowing them to reflect on the reported security vulnerabilities in account ecosystems. Results. Our participants are aware of some online security practices, such as not to reuse passwords. Lack of trust in their own memory is a critical factor in their password management and device access control strategies. All consider finance-related accounts as their most important accounts, but few identified the secondary accounts (e.g. emails for account recovery) or devices that provide access to these as very important. Conclusions. Older adults make a conscious choice to implement specific practices based on their understanding of security, their trust in their own abilities and third-parties, and the usability of a given security practice. While they are well-aware of some best security practices, their choices will be different if the best security practice does not work in their personal context.

We introduce and comment on the concept of contextual pseudo identity. A contextual pseudo identity is a soft identity token that is built from both a user's biometric and the context. When it comes to ubiquitous authentication, a contextual pseudo identity promises better security than that offered by traditional biometrics-based identity tokens: the use of context improves the tokens' disposability and renewability, which are two essential properties in the protection of a user's real identity. Our algorithm for generating contextual pseudo identities extends a Fuzzy Embedder so that it accepts both biometric and context-dependent input. We prove that our way of processing the context preserves the security and reliability properties of the Fuzzy Embedder used in our extension. An example shows how a user can utilize contextual pseudo identity to authenticate to and access ubiquitous services.

We give an explicit, general construction for optimistic multi-party contract signing protocols. Our construction converts a sequence over any finite set of signers into a protocol specification for the signers. The inevitable trusted third party's role specification and computations are independent of the signer's role specification. This permits a wide variety of protocols to be handled equally by the trusted third party. We give tight conditions under which the resulting protocols satisfy fairness and timeliness. We provide examples of several classes of protocols and we discuss lower bounds for the complexity of fair protocols, both in terms of bandwidth and minimum number of messages. Our results highlight the connection between optimistic fair contract signing protocols and the combinatorial problem of constructing sequences which contain all permutations of a set as subsequences. This connection is stronger than was previously realized.

The motivation for the current report lies in a number of questions concerning the current state of the art in security protocol design and analysis. Why is it so hard to develop a complete set of security requirements for a particular problem? For instance, even in the seemingly simple case of defining the secrecy property of an encryption algorithm it has taken decades to reach a degree of consensus, and even now new definitions are required in specific contexts. Similarly, even after more than twenty years of research on e-voting, there is still a lack of consensus as to which properties an e-voting protocol should satisfy. What did we learn from this research experience on e-voting? Can we apply the knowledge accumulated in this domain to similar domains and problems? Is there a methodology underlying the process of understanding a security protocol domain?

We introduce and give formal definitions of attack-defense trees. We argue that these trees are a simple, yet powerful tool to analyze complex security and privacy problems. Our formalization is generic in the sense that it supports different semantical approaches. We present several semantics for attack-defense trees along with usage scenarios, and we show how to evaluate attributes.

Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.

We demonstrate two classes of attacks on EC-RAC, a growing set of RFID protocols. Our first class of attacks concerns the compositional approach used to construct a particular revision of EC-RAC. We invalidate the authentication and privacy claims made for that revision. We discuss the significance of the fact that RFID privacy is not compositional in general. Our second class of attacks applies to all versions of EC-RAC and reveals hitherto unknown vulnerabilities in the latest version of EC-RAC. It is a general man-in-the-middle attack executable by a weak adversary. We show a general construction for improving narrow-weak private protocols to wide-weak private protocols and indicate specific improvements for the flaws of EC-RAC exhibited in this document.

A person’s online security setup is tied to the security of their individual accounts. Some accounts are particularly critical as they provide access to other online services. For example, an email account can be used for external account recovery or to assist with single-sign-on. The connections between accounts are specific to each user’s setup and create unique security problems that are difficult to remedy by following generic security advice. In this paper, we develop a method to gather and analyze users’ online accounts systematically. We demonstrate this in a user study with 20 participants and obtain detailed insights on how users’ personal setup choices and behaviors affect their overall account security. We discuss concrete usability and privacy concerns that prevented our participants from improving their account security. Based on our findings, we provide recommendations for service providers and security experts to increase the adoption of security best practices.