Breaking Unlinkability of the ICAO 9303 Standard for e-Passports using Bisimilarity

in Breaking Unlinkability of the ICAO 9303 Standard for e-Passports using Bisimilarity (2019, September 23)

We clear up confusion surrounding privacy claims about the ICAO 9303 standard for e-passports. The ICAO 9303 standard includes a Basic Access Control (BAC) protocol that should protect the user from being ... [more ▼]

We clear up confusion surrounding privacy claims about the ICAO 9303 standard for e-passports. The ICAO 9303 standard includes a Basic Access Control (BAC) protocol that should protect the user from being traced from one session to another. While it is well known that there are attacks on BAC, allowing an attacker to link multiple uses of the same passport, due to differences in implementation; there still remains confusion about whether there is an attack on unlinkability directly on the BAC protocol as specified in the ICAO 9303 standard. This paper clarifies the nature of the debate, and sources of potential confusion. We demonstrate that the original privacy claims made are flawed, by uncovering attacks on a strong formulation of unlinkability. We explain why the use of the bisimilarity equivalence technique is essential for uncovering our attacks. We also clarify what assumptions lead to proofs of formulations of unlinkability using weaker notions of equivalence. Furthermore, we propose a fix for BAC within the scope of the standard, and prove that it is correct, again using a state-of-the-art approach to bisimilarity. [less ▲]

Global Types with Internal Delegation

in Theoretical Computer Science (2019)

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This ... [more ▼]

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This means that delegation is inherently an inter-session mechanism, which requires session interleaving. Hence delegation falls outside the descriptive power of global types, which specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. Here we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (internal delegation) and may be captured by its global type. To increase flexibility in the use of delegation, our calculus uses connecting communications, which allow optional participants in the branches of choices. By these means, we are able to express conditional delegation. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property. [less ▲]

Graphical Models for Security - 6th International Workshop, Revised Papers

Scientific Conference (2019)

The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement

in Proc.\ 5th International Workshop on Graphical Models for Security (GraMSec'18) (2018, July 08)

Semantics for specialising attack trees based on linear logic

in Fundamenta Informaticae (2017), 153(1-2), 57-86

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an ... [more ▼]

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV , featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains. [less ▲]

Private Names in Non-Commutative Logic

in 27th International Conference on Concurrency Theory (CONCUR 2016) (2016)

SPEC: An Equivalence Checker for Security Protocols

in Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings (2016)

Minimal type inference for Linked Data consumers

in Journal of Logical and Algebraic Methods in Programming (2015), 84(4), 485-504

Behavioural analysis of sessions using the calculus of structures

in In Perspectives of System Informatics, 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27 (2015)

Non-interleaving Operational Semantics for Geographically Replicated Databases

in 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, {SYNASC} 2013, Timisoara, Romania, September 23-26, 2013 (2013)