Journal of Computer Security

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.

Machine learning algorithms, when applied to sensitive data, pose a distinct threat to privacy. A growing body of prior work demonstrates that models produced by these algorithms may leak specific private information in the training data to an attacker, either through the models’ structure or their observable behavior. This article examines the factors that can allow a training set membership inference attacker or an attribute inference attacker to learn such information. Using both formal and empirical analyses, we illustrate a clear relationship between these factors and the privacy risk that arises in several popular machine learning algorithms.

We find that overfitting is sufficient to allow an attacker to perform membership inference and, when the target attribute meets certain conditions about its influence, attribute inference attacks. We also explore the connection between membership inference and attribute inference, showing that there are deep connections between the two that lead to effective new attacks. We show that overfitting is not necessary for these attacks, demonstrating that other factors, such as robustness to norm-bounded input perturbations and malicious training algorithms, can also significantly increase the privacy risk. Notably, as robustness is intended to be a defense against attacks on the integrity of model predictions, these results suggest it may be difficult in some cases to simultaneously defend against privacy and integrity attacks.

Symbolic models for security protocol verification were pioneered by Dolev and Yao in their seminal work. Since then, although inspired by the same ideas, many variants of the original model were developed. In particular, a common assumption is that the attacker has complete control over the network and can therefore intercept any message. This assumption has been interpreted in slightly different ways depending on the particular models: either any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker – the scheduling between which exact parties the communication happens is left to the attacker. This difference may seem unimportant at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, for indistinguishability properties, we prove that these two interpretations lead to incomparable semantics. We also introduce and study a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. This new semantics yields strictly stronger equivalence relations. Moreover, we identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of the three semantics in the DeepSec tool and compare their performances on several classical examples.

Information Flow Control (IFC) is a form of dependence analysis that tracks and prohibits dependence of public outputs on secret inputs. Such a dependence analysis is often carried out using a type system. IFC type systems can track dependence (via confidentiality labels) at varying levels of granularity. On one extreme, there are fine-grained type systems that track dependence at the level of individual values. They label individual values. On the other extreme, there are coarse-grained type systems that track dependence at the level of entire computations. These type systems do not label individual values but instead label entire sub-computations.

An important foundational question is one of the relative expressiveness of these two classes of IFC type systems. In this paper we show that, despite the glaring differences in how they track dependence, the two classes of type systems are actually equally expressive. We do this by showing translations from FG, a fine-grained IFC type system derived from SLAM (In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (1998)), to SLIO ∗ , a coarse-grained IFC type system derived from HLIO (In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP) (2015)), and vice-versa. The translation from SLIO ∗ to FG is straightforward since FG tracks dependence at a granularity finer than SLIO ∗ does. However, the translation from FG to SLIO ∗ is quite involved and relies extensively on label quantification. We further examine the reason for this complexity using a slight variant of SLIO ∗ , called CG, to which FG can be translated more easily.

As a separate, more foundational contribution we show how to extend logical relation models of information flow to languages with higher-order state. Specifically, we build world-indexed (Kripke) logical relations for FG, SLIO ∗ and CG, which we use to prove these type systems sound and also to prove the translations between them correct.