Demo Data from SIGIR 2026 / reviewers in the wild / expert
Esfandiar Mohammadi
dblp:77/8938
· DBLP profile ↗
24ranked-venue papers
0as first author
7since 2021 · last 2026
0000-0002-2799-8128ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Security and privacy · 20 · 5 since 2021Artificial intelligence and machine learning · 1 · 1 since 2021Computer networks · 1Databases, data management, data science and information retrieval · 1 · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 1 · 1 since 2021Theory of computation · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Network and information security
10 papers |
Privacy and data protection · 48% Network security · 45% Web and mobile security · 5% | |
| Artificial intelligence
1 paper |
Efficient and distributed learning · 100% |
Topics — the 23 heaviest of 24, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Network security
anonymity networks |
2.0 | 5 | 2025 | Mixnets on a Tightrope: Quantifying the Leakage of Mix Networks Using a Provably Optimal Heuristic Adversary · SP 2025 Deniable Upload and Download via Passive Participation · NSDI 2019 Anonymity Trilemma: Strong Anonymity, Low Bandwidth Overhead, Low Latency - Choose Two · IEEE Symposium on Security and Privacy 2018 |
Privacy and data protection
differential privacy |
1.4 | 3 | 2024 | S-BDT: Distributed Differentially Private Boosted Decision Trees · CCS 2024 PrivacyBuDe: Privacy Buckets Demo Tight Differential Privacy Guarantees made Simple · CCS 2018 Tight on Budget?: Tight Bounds for r-Fold Approximate Differential Privacy · CCS 2018 |
Privacy and data protection › information leakage
information leakage quantification |
0.9 | 1 | 2025 | Mixnets on a Tightrope: Quantifying the Leakage of Mix Networks Using a Provably Optimal Heuristic Adversary · SP 2025 |
Network security › anonymity networks
mix networks |
0.9 | 1 | 2025 | Mixnets on a Tightrope: Quantifying the Leakage of Mix Networks Using a Provably Optimal Heuristic Adversary · SP 2025 |
Network security › anonymity networks
receiver anonymity |
0.9 | 1 | 2025 | Mixnets on a Tightrope: Quantifying the Leakage of Mix Networks Using a Provably Optimal Heuristic Adversary · SP 2025 |
Machine learning › Efficient and distributed learning
distributed training |
0.8 | 1 | 2024 | S-BDT: Distributed Differentially Private Boosted Decision Trees · CCS 2024 |
Privacy and data protection
anonymization |
0.8 | 1 | 2024 | $DPM: $ Clustering Sensitive Data through Separation · CCS 2024 |
Privacy and data protection
anonymity |
0.4 | 2 | 2015 | POSTER: In the Net of the Spider: Measuring the Anonymity-Impact of Network-level Adversaries Against Tor · CCS 2015 (Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path Selection · CCS 2014 |
Network security › anonymity networks
tor |
0.4 | 2 | 2015 | POSTER: In the Net of the Spider: Measuring the Anonymity-Impact of Network-level Adversaries Against Tor · CCS 2015 (Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path Selection · CCS 2014 |
Privacy and data protection › privacy-enhancing technologies
deniable communication |
0.4 | 1 | 2019 | Deniable Upload and Download via Passive Participation · NSDI 2019 |
Network security › anonymity networks
anonymous communication |
0.3 | 1 | 2018 | Anonymity Trilemma: Strong Anonymity, Low Bandwidth Overhead, Low Latency - Choose Two · IEEE Symposium on Security and Privacy 2018 |
Privacy and data protection › differential privacy › relaxed differential privacy
approximate differential privacy |
0.3 | 1 | 2018 | Tight on Budget?: Tight Bounds for r-Fold Approximate Differential Privacy · CCS 2018 |
Privacy and data protection › differential privacy › privacy accounting
composition theorems |
0.3 | 1 | 2018 | Tight on Budget?: Tight Bounds for r-Fold Approximate Differential Privacy · CCS 2018 |
Privacy and data protection › differential privacy
privacy accounting |
0.3 | 1 | 2018 | PrivacyBuDe: Privacy Buckets Demo Tight Differential Privacy Guarantees made Simple · CCS 2018 |
Web and mobile security › mobile security
android application analysis |
0.2 | 1 | 2016 | Computational Soundness for Dalvik Bytecode · CCS 2016 |
Cryptographic protocols and secure computation › protocol verification
computational soundness |
0.2 | 1 | 2016 | Computational Soundness for Dalvik Bytecode · CCS 2016 |
Web and mobile security
mobile security |
0.2 | 1 | 2016 | Computational Soundness for Dalvik Bytecode · CCS 2016 |
Privacy and data protection › anonymity
anonymity metric |
0.2 | 1 | 2015 | POSTER: In the Net of the Spider: Measuring the Anonymity-Impact of Network-level Adversaries Against Tor · CCS 2015 |
Network security › anonymity networks
path selection |
0.2 | 1 | 2014 | (Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path Selection · CCS 2014 |
Network security
traffic analysis |
0.1 | 1 | 2019 | Deniable Upload and Download via Passive Participation · NSDI 2019 |
Program analysis › static analysis
information flow analysis |
0.1 | 1 | 2016 | Computational Soundness for Dalvik Bytecode · CCS 2016 |
Program analysis
static analysis |
0.1 | 1 | 2016 | Computational Soundness for Dalvik Bytecode · CCS 2016 |
Network management and operations
network monitoring |
0.1 | 1 | 2014 | (Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path Selection · CCS 2014 |
Methods — techniques the papers use, named apart from their topics
subsampling · 1.5rényi differential privacy · 1.5multivariate gaussian noise · 1.5gradient boosting · 1.5sampling · 0.9provably optimal heuristic adversary · 0.9privacy loss distribution · 0.9separation-based clustering · 0.8hypothesis testing · 0.3concentrated differential privacy · 0.3symbolic abstraction · 0.2computational soundness · 0.2anonymity framework · 0.2anoa · 0.2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | DP-Hype: Federated Differentially Private Hyperparameter SearchabstractThe tuning of hyperparameters in federated machine learning can substantially impact model performance. When the hyperparameters are tuned on sensitive data, privacy becomes an important challenge and to this end, differential privacy has emerged as the de facto standard for provable privacy. A standard setting when performing federated learning tasks is that clients agree on a shared setup, i.e., find a compromise from a set of hyperparameters, like a model's learning rate. Yet, prior work on privacy-preserving hyperparameter tuning is tailored to specific learning tasks, does not take into account the privacy leakage of aggregated results, or offers a sub-optimal privacy-utility trade-off. In this work, we present our algorithm DP-Hype, which performs a federated and privacy-preserving hyperparameter search by conducting a federated voting based on local hyperparameter evaluations of clients. In this way, DP-Hype selects hyperparameters that lead to a compromise supported by the majority of clients, while maintaining scalability and independence from specific learning tasks. We prove that DP-Hype preserves the strong notion of differential privacy called client-level differential privacy and, importantly, show that its privacy guarantees do not depend on the number of hyperparameters. We also provide bounds on its utility guarantees, that is, the probability of finding good hyperparameters, and implement DP-Hype as a submodule in the popular Flower framework for federated machine learning. In addition, we evaluate performance on multiple benchmark data sets in iid as well as multiple non-iid settings and demonstrate high utility of DP-Hype even under small privacy budgets. Johannes Liebenow, Thorsten Peinemann, Esfandiar Mohammadi |
Proc. Priv. Enhancing Technol. | 3 |
| 2025 | Mixnets on a Tightrope: Quantifying the Leakage of Mix Networks Using a Provably Optimal Heuristic AdversaryabstractMixnets are widely believed to hide communication metadata of individuals. We show that there are various pitfalls when designing mixnet topologies and routing strategies, in particular when choosing mixnets with low delays. We introduce a tool that empirically evaluates such leakage in mixnets and show that this tool precisely estimates this leakage for recipient anonymity, up to an error introduced by sampling. First, we introduce a novel generic attack strategy that we even prove to be optimal for breaking recipient anonymity. In contrast to prior work, our attack strategy incorporates the severity of each observation's leakage, via its so-called privacy loss. Second, our tool provides a lower bound on an attacker's advantage against recipient anonymity by sampling a large set of observations; if a significant number of observations with high privacy loss is observed, the tool outputs a lower bound on the leakage by providing a lower bound on the mass of the tail of the distribution of privacy losses. From the literature, we study the topology and routing strategies of the Karaoke and Atom protocols, provide bounds on their leakage, and recommend design choices based on the analysis. Sebastian Meiser 0001, Debajyoti Das 0001, Moritz Kirschte, Esfandiar Mohammadi, Aniket Kate |
SP | 4 |
| 2024 | $DPM: $ Clustering Sensitive Data through Separation
Johannes Liebenow, Yara Schütt, Tanya Braun, Marcel Gehrke, Florian Thaeter, Esfandiar Mohammadi |
CCS | 6 |
| 2024 | S-BDT: Distributed Differentially Private Boosted Decision TreesabstractWe introduce S-BDT: a novel (𝜀, 𝛿)-differentially private distributed gradient boosted decision tree (GBDT) learner that improves the protection of single training data points (privacy) while achieving meaningful learning goals, such as accuracy or regression error (utility).S-BDT uses less noise by relying on non-spherical multivariate Gaussian noise, for which we show tight subsampling bounds for privacy amplification and incorporate that into a Rényi filter for individual privacy accounting.We experimentally reach the same utility while saving 50% in terms of epsilon for 𝜀 ≤ 0.5 on the Abalone regression dataset (dataset size ≈ 4𝐾), saving 30% in terms of epsilon for 𝜀 ≤ 0.08 for the Adult classification dataset (dataset size ≈ 50𝐾), and saving 30% in terms of epsilon for 𝜀 ≤ 0.03 for the Spambase classification dataset (dataset size ≈ 5𝐾).Moreover, we show that for situations where a GBDT is learning a stream of data that originates from different subpopulations (non-IID), S-BDT improves the saving of epsilon even further. CCS Concepts• Theory of computation → Theory of database privacy and security; • Computing methodologies → Boosting; Online learning settings. Thorsten Peinemann, Moritz Kirschte, Joshua Stock, Carlos Cotrini Jiménez, Esfandiar Mohammadi |
CCS | 5 |
| 2024 | Divide and Funnel: A Scaling Technique for Mix-NetworksabstractWhile many anonymous communication (AC) protocols have been proposed to provide anonymity over the internet, scaling to a large number of users while remaining provably secure is challenging. We tackle this challenge by proposing a new scaling technique to improve the scalability/anonymity of AC protocols that distributes the computational load over many nodes without completely disconnecting the paths different messages take through the network. We demonstrate that our scaling technique is useful and practical through a core sample anonymous broadcast protocol, Streams, that offers provable security guarantees and scales for a million messages. The scaling technique ensures that each node in the system does the computation-heavy public key operation only for a tiny fraction of the total messages routed through the Streams network while maximizing the mixing/shuffling in every round. Our experimental results show that Streams can scale well even if the system has a load of one million messages at any point in time, with a latency of 16 seconds while offering provable “one-in-a-billion” unlinkability, and can be leveraged for applications such as anonymous microblogging and network-level anonymity for blockchains. We also illustrate by examples that our scaling technique can be useful to other AC protocols to improve their scalability and privacy, and can be interesting to protocol developers. Debajyoti Das 0001, Sebastian Meiser 0001, Esfandiar Mohammadi, Aniket Kate |
CSF | 3 |
| 2024 | Differentially Private Inductive MinerabstractProtecting personal data about individuals, such as event traces in process mining, is an inherently difficult task since an event trace leaks information about the path in a process model that an individual has triggered. Yet, prior anonymization methods of event traces like k-anonymity or event log sanitization struggled to protect against such leakage, in particular against adversaries with sufficient background knowledge. In this work, we provide a method that tackles the challenge of summarizing sensitive event traces by learning the underlying process tree in a privacy-preserving manner. We prove via the so-called Differential Privacy (DP) property that from the resulting summaries no useful inference can be drawn about any personal data in an event trace. On the technical side, we introduce a differentially private approximation (DPIM) of the Inductive Miner. Experimentally, we compare our DPIM with the Inductive Miner on 14 real-world event traces by evaluating well-known metrics: fitness, precision, simplicity, and generalization. The experiments show that our DPIM not only protects personal data but also generates faithful process trees that exhibit little utility loss above the Inductive Miner. Max Schulze, Yorck Zisgen, Moritz Kirschte, Esfandiar Mohammadi, Agnes Koschmider |
ICPM | 4 |
| 2023 | Towards Privacy and Utility in Tourette TIC Detection Through Pretraining Based on Publicly Available Video Data of Healthy SubjectsabstractData privacy is typically particularly difficult to achieve in medical applications of machine learning, despite its importance in this area. The datasets are often small, which is why machine learning models such as neural networks tend to memorize information about the training data. This allows confidential and sensitive information about patients to be extracted from the model. Further challenging achieving data privacy is that the best possible utility must be ensured. In this work, we aim to detect tics based on video data of patients with Gilles de la Tourette syndrome. Facial landmarks were used as a lower-dimensional representation of the video data. Through membership inference attacks, we show that training a simple neural network directly on sensitive training data leaks information about the training data, and that this can be prevented by suitable pretraining on a large amount of unlabeled public data of healthy subjects. The proposed approach can not only reduce the attack accuracy to 52.15 %, but also achieves a high tic detection accuracy of 86.53 %. Nele Sophie Brügge, Esfandiar Mohammadi, Alexander Münchau, Tobias Bäumer, Christian Frings, Christian Beste, Veit Rößner, Heinz Handels |
ICASSP | 2 |
| 2020 | Comprehensive Anonymity Trilemma: User Coordination is not enoughabstractAbstract For anonymous communication networks (ACNs), Das et al. recently confirmed a long-suspected trilemma result that ACNs cannot achieve strong anonymity, low latency overhead and low bandwidth overhead at the same time. Our paper emanates from the careful observation that their analysis does not include a relevant class of ACNs with what we call user coordination where users proactively work together towards improving their anonymity. We show that such protocols can achieve better anonymity than predicted by the above trilemma result. As the main contribution, we present a stronger impossibility result that includes all ACNs we are aware of. Along with our formal analysis, we provide intuitive interpretations and lessons learned. Finally, we demonstrate qualitatively stricter requirements for the Anytrust assumption (all but one protocol party is compromised) prevalent across ACNs. Debajyoti Das 0001, Sebastian Meiser 0001, Esfandiar Mohammadi, Aniket Kate |
Proc. Priv. Enhancing Technol. | 3 |
| 2019 | Deniable Upload and Download via Passive Participation
David M. Sommer 0001, Aritra Dhar, Luka Malisa, Esfandiar Mohammadi, Daniel Ronzani, Srdjan Capkun |
NSDI | 4 |
| 2019 | Privacy Loss Classes: The Central Limit Theorem in Differential PrivacyabstractAbstract Quantifying the privacy loss of a privacy-preserving mechanism on potentially sensitive data is a complex and well-researched topic; the de-facto standard for privacy measures are ε-differential privacy (DP) and its versatile relaxation (ε, δ)-approximate differential privacy (ADP). Recently, novel variants of (A)DP focused on giving tighter privacy bounds under continual observation. In this paper we unify many previous works via the privacy loss distribution (PLD) of a mechanism. We show that for non-adaptive mechanisms, the privacy loss under sequential composition undergoes a convolution and will converge to a Gauss distribution (the central limit theorem for DP). We derive several relevant insights: we can now characterize mechanisms by their privacy loss class, i.e., by the Gauss distribution to which their PLD converges, which allows us to give novel ADP bounds for mechanisms based on their privacy loss class; we derive exact analytical guarantees for the approximate randomized response mechanism and an exact analytical and closed formula for the Gauss mechanism, that, given ε, calculates δ, s.t., the mechanism is (ε, δ)-ADP (not an over-approximating bound). David M. Sommer 0001, Sebastian Meiser 0001, Esfandiar Mohammadi |
Proc. Priv. Enhancing Technol. | 3 |
| 2018 | Tight on Budget?: Tight Bounds for r-Fold Approximate Differential PrivacyabstractMany applications, such as anonymous communication systems, privacy-enhancing database queries, or privacy-enhancing machine-learning methods, require robust guarantees under thousands and sometimes millions of observations. The notion of r-fold approximate differential privacy (ADP) offers a well-established framework with a precise characterization of the degree of privacy after r observations of an attacker. However, existing bounds for r-fold ADP are loose and, if used for estimating the required degree of noise for an application, can lead to over-cautious choices for perturbation randomness and thus to suboptimal utility or overly high costs. We present a numerical and widely applicable method for capturing the privacy loss of differentially private mechanisms under composition, which we call privacy buckets. With privacy buckets we compute provable upper and lower bounds for ADP for a given number of observations. We compare our bounds with state-of-the-art bounds for r-fold ADP, including Kairouz, Oh, and Viswanath's composition theorem (KOV), concentrated differential privacy and the moments accountant. While KOV proved optimal bounds for heterogeneous adaptive k-fold composition, we show that for concrete sequences of mechanisms tighter bounds can be derived by taking the mechanisms' structure into account. We compare previous bounds for the Laplace mechanism, the Gauss mechanism, for a timing leakage reduction mechanism, and for the stochastic gradient descent and we significantly improve over their results (except that we match the KOV bound for the Laplace mechanism, for which it seems tight). Our lower bounds almost meet our upper bounds, showing that no significantly tighter bounds are possible. Sebastian Meiser 0001, Esfandiar Mohammadi |
CCS | 2 |
| 2018 | PrivacyBuDe: Privacy Buckets Demo Tight Differential Privacy Guarantees made SimpleabstractComputing differential privacy guarantees is an important task for a wide variety of applications. The tighter the guarantees are, the more difficult it seems to be to compute them: naive bounds are simple additions, whereas modern composition theorems require either a search over a potentially confusing parameter space (for the composition theorem of Kairouz, Oh, and Visvanath), require computing many moments (for Rényi DP) or finding parameters of a function that limits the privacy loss (for concentrated DP). The best known approach for tight differential privacy bounds, called Privacy Buckets, provides requires running a fairly complex implementation of numerical approximations. In this work, we provide an easy-to-use interface for computing state-of-the-art differential privacy guarantees by simply accessing a website. Guarantees for the widely used Laplace mechanism and for the similarly popular Gauss mechanism can be computed by simply stating the scale parameter of the noise, the sensitivity, and the number of compositions. Privacy guarantees for more complex distributions can be computed by uploading two histograms. This work bridges the gap between the best known theoretical results for computing differential privacy guarantees and privacy analysts and users benefiting from such guarantees. David M. Sommer 0001, Sebastian Meiser 0001, Esfandiar Mohammadi |
CCS | 3 |
| 2018 | Anonymity Trilemma: Strong Anonymity, Low Bandwidth Overhead, Low Latency - Choose TwoabstractThis work investigates the fundamental constraints of anonymous communication (AC) protocols. We analyze the relationship between bandwidth overhead, latency overhead, and sender anonymity or recipient anonymity against the global passive (network-level) adversary. We confirm the trilemma that an AC protocol can only achieve two out of the following three properties: strong anonymity (i.e., anonymity up to a negligible chance), low bandwidth overhead, and low latency overhead. We further study anonymity against a stronger global passive adversary that can additionally passively compromise some of the AC protocol nodes. For a given number of compromised nodes, we derive necessary constraints between bandwidth and latency overhead whose violation make it impossible for an AC protocol to achieve strong anonymity. We analyze prominent AC protocols from the literature and depict to which extent those satisfy our necessary constraints. Our fundamental necessary constraints offer a guideline not only for improving existing AC systems but also for designing novel AC protocols with non-traditional bandwidth and latency overhead choices. Debajyoti Das 0001, Sebastian Meiser 0001, Esfandiar Mohammadi, Aniket Kate |
IEEE Symposium on Security and Privacy | 3 |
| 2017 | CoverUp: Privacy Through "Forced" Participation in Anonymous Communication NetworksabstractMany privacy-enhancing technologies, in particular anonymous communication networks (ACNs) as a key building block, suffer from a lack of a sufficient number of participants. Without high user participation, ACNs are vulnerable to traffic analysis attacks. The only ACN with a high number of participants (around 1.5 million users) is Tor. Yet, Tor is prone to traffic analysis attacks traffic pattern attacks. While other ACNs have been proposed that are even secure against global attackers, they are not scalable and suffer from a low number of participants, since even a perfect ACN can at most hide a user among all participating users. These ACNs are in a vicious circle: the lack of participants leads to low degree of anonymity, and a low degree of anonymity makes these ACNs unattractive for users. In this work, we break this vicious cycle by studying the question: Can an anonymous communication network be strengthened by "forced" participation? What privacy guarantees and performance can such an ACN provide? We develop CoverUp, a system that "forces" visitors of highly accessed websites (entry servers) to become involuntary participants of an ACN. CoverUp triggers users to participate in a centralized, constant-rate mix by leveraging basic functionality of their browsers to execute (JavaScript) code served by the entry servers. Candidates for entry servers could be universities or news sites. They would let a distinct CoverUp server provide (via an iframe) JavaScript code to the end-users' browsers, which in turn makes them participate in the ACN via a mix server. Visitors of these entry servers' websites become (involuntary) participants of an ACN, creating cover traffic for voluntary participants. For voluntary participants, we developed a browser extension that renders their CoverUp requests indistinguishable from the cover traffic of involuntary participants. David M. Sommer 0001, Aritra Dhar, Luka Malisa, Esfandiar Mohammadi, Daniel Ronzani, Srdjan Capkun |
AsiaCCS | 4 |
| 2016 | Computational Soundness for Dalvik BytecodeabstractAutomatically analyzing information flow within Android applications that rely on cryptographic operations with their computational security guarantees imposes formidable challenges that existing approaches for understanding an app's behavior struggle to meet. These approaches do not distinguish cryptographic and non-cryptographic operations, and hence do not account for cryptographic protections: f(m) is considered sensitive for a sensitive message m irrespective of potential secrecy properties offered by a cryptographic operation f. These approaches consequently provide a safe approximation of the app's behavior, but they mistakenly classify a large fraction of apps as potentially insecure and consequently yield overly pessimistic results. In this paper, we show how cryptographic operations can be faithfully included into existing approaches for automated app analysis. To this end, we first show how cryptographic operations can be expressed as symbolic abstractions within the comprehensive Dalvik bytecode language. These abstractions are accessible to automated analysis and can be conveniently added to existing app analysis tools using minor changes in their semantics. Second, we show that our abstractions are faithful by providing the first computational soundness result for Dalvik bytecode, i.e., the absence of attacks against our symbolically abstracted program entails the absence of any attacks against a suitable cryptographic program realization. We cast our computational soundness result in the CoSP framework, which makes the result modular and composable. Michael Backes 0001, Robert Künnemann, Esfandiar Mohammadi |
CCS | 3 |
| 2015 | POSTER: In the Net of the Spider: Measuring the Anonymity-Impact of Network-level Adversaries Against TorabstractRecently, the live-monitor MATor for formally analyzing user anonymity within the Tor network has been proposed (CCS'14). However, this monitor only considers adversaries that compromise part of the Tor network itself, not Internet infrastructural adversaries. In this work we present a formal technique for analyzing Tor against malicious or overly curious network infrastructure. Michael Backes 0001, Simon Koch 0001, Sebastian Meiser 0001, Esfandiar Mohammadi, Christian Rossow |
CCS | 4 |
| 2015 | Symbolic Malleable Zero-Knowledge ProofsabstractZero-knowledge (ZK) proofs have become a central building block for a variety of modern security protocols. Modern ZK constructions, such as the Groth-Sahai proof system, offer novel types of cryptographic flexibility: a participant is able to re-randomize existing ZK proofs to achieve, for instance, message unlink ability in anonymity protocols, she can hide public parts of a ZK proof statement to meet her specific privacy requirements, and she can logically compose ZK proofs in order to construct new proof statements. ZK proof systems that permit these transformations are called malleable. However, since these transformations are accessible also to the adversary, analyzing the security of these protocols requires one to cope with a much more comprehensive attacker model -- a challenge that automated protocol analysis thus far has not been capable of dealing with. In this work, we introduce the first symbolic abstraction of malleable ZK proofs. We further prove the computational soundness of our abstraction with respect to observational equivalence, which enables the computationally sound verification of privacy properties. Finally, we show that our symbolic abstraction is suitable for ProVerif, a state-of-the-art cryptographic protocol verifier, by verifying an improved version of the anonymous webs of trust protocol. Michael Backes 0001, Fabian Bendun, Matteo Maffei, Esfandiar Mohammadi, Kim Pecina |
CSF | 4 |
| 2015 | Computational Soundness for Interactive PrimitivesabstractWe present a generic computational soundness result for interactive cryptographic primitives. Our abstraction of interactive primitives leverages the Universal Composability (UC) framework, and thereby offers strong composability properties for our computational soundness result: given a computationally sound Dolev-Yao model for non-interactive primitives, and given UC-secure interactive primitives, we obtain computational soundness for the combined model that encompasses both the non-interactive and the interactive primitives. Our generic result is formulated in the CoSP framework for computational soundness proofs and supports any equivalence property expressible in CoSP such as strong secrecy and anonymity. In a case study, we extend an existing computational soundness result by UC-secure blind signatures. We obtain computational soundness for blind signatures in uniform bi-processes in the applied $$\pi $$ -calculus. This enables us to verify the untraceability of Chaum’s payment protocol in ProVerif in a computationally sound manner. Michael Backes 0001, Esfandiar Mohammadi, Tim Ruffing |
ESORICS (1) | 2 |
| 2014 | (Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path SelectionabstractIn this paper we present MATor: a framework for rigorously assessing the degree of anonymity in the Tor network. The framework explicitly addresses how user anonymity is impacted by real-life characteristics of actually deployed Tor, such as its path selection algorithm, Tor consensus data, and the preferences and the connections of the user. The anonymity assessment is based on rigorous anonymity bounds that are derived in an extension of the AnoA framework (IEEE CSF 2013). We show how to apply MATor on Tor's publicly available consensus and server descriptor data, thereby realizing the first real-time anonymity monitor. Based on experimental evaluations of this anonymity monitor on Tor Metrics data, we propose an alternative path selection algorithm that provides stronger anonymity guarantees without decreasing the overall performance of the Tor network. Michael Backes 0001, Aniket Kate, Sebastian Meiser 0001, Esfandiar Mohammadi |
CCS | 4 |
| 2014 | TUC: Time-Sensitive and Modular Analysis of Anonymous CommunicationabstractThe anonymous communication protocol Tor constitutes the most widely deployed technology for providing anonymity for user communication over the Internet. Several frameworks have been proposed that show strong anonymity guarantees, none of these, however, are capable of modeling the class of traffic-related timing attacks against Tor, such as traffic correlation and website fingerprinting. In this work, we present TUC: the first framework that allows for establishing strong anonymity guarantees in the presence of time-sensitive adversaries that mount traffic-related timing attacks. TUC incorporates a comprehensive notion of time in an asynchronous communication model with sequential activation, while offering strong compositionality properties for security proofs. We apply TUC to evaluate a novel countermeasure for Tor against website fingerprinting attacks. Our analysis relies on a formalization of the onion routing protocol that underlies Tor and proves rigorous anonymity guarantees in the presence of traffic-related timing attacks. Michael Backes 0001, Praveen Manoharan 0001, Esfandiar Mohammadi |
CSF | 3 |
| 2013 | AnoA: A Framework for Analyzing Anonymous Communication ProtocolsabstractProtecting individuals' privacy in online communications has become a challenge of paramount importance. To this end, anonymous communication (AC) protocols such as the widely used Tor network have been designed to provide anonymity to their participating users. While AC protocols have been the subject of several security and anonymity analyses in the last years, there still does not exist a framework for analyzing complex systems such as Tor and their different anonymity properties in a unified manner. In this work we present AnoA: a generic framework for defining, analyzing, and quantifying anonymity properties for AC protocols. AnoA relies on a novel relaxation of the notion of (computational) differential privacy, and thereby enables a unified quantitative analysis of well-established anonymity properties, such as sender anonymity, sender unlinkability, and relationship anonymity. While an anonymity analysis in AnoA can be conducted in a purely information theoretical manner, we show that the protocol's anonymity properties established in AnoA carry over to secure cryptographic instantiations of the protocol. We exemplify the applicability of AnoA for analyzing real-life systems by conducting a thorough analysis of the anonymity properties provided by the Tor network against passive attackers. Our analysis significantly improves on known anonymity results from the literature. Michael Backes 0001, Aniket Kate, Praveen Manoharan 0001, Sebastian Meiser 0001, Esfandiar Mohammadi |
CSF | 5 |
| 2013 | Privacy-Preserving Accountable Computation
Michael Backes 0001, Dario Fiore 0001, Esfandiar Mohammadi |
ESORICS | 3 |
| 2012 | Provably Secure and Practical Onion RoutingabstractThe onion routing network Tor is undoubtedly the most widely employed technology for anonymous web access. Although the underlying onion routing (OR) protocol appears satisfactory, a comprehensive analysis of its security guarantees is still lacking. This has also resulted in a significant gap between research work on OR protocols and existing OR anonymity analyses. In this work, we address both issues with onion routing by defining a provably secure OR protocol, which is practical for deployment in the next generation Tor network. We start off by presenting a security definition (an ideal functionality) for the OR methodology in the universal compos ability (UC) framework. We then determine the exact security properties required for OR cryptographic primitives (onion construction and processing algorithms, and a key exchange protocol) to achieve a provably secure OR protocol. We show that the currently deployed onion algorithms with slightly strengthened integrity properties can be used in a provably secure OR construction. In the process, we identify the concept of predictably malleable symmetric encryptions, which might be of independent interest. On the other hand, we find the currently deployed key exchange protocol to be inefficient and difficult to analyze and instead show that a recent, significantly more efficient, key exchange protocol can be used in a provably secure OR construction. In addition, our definition greatly simplifies the process of analyzing OR anonymity metrics. We define and prove forward secrecy for the OR protocol, and realize our (white-box) OR definition from an OR black-box model assumed in a recent anonymity analysis. This realization not only makes the analysis formally applicable to the OR protocol but also identifies the exact adversary and network assumptions made by the black box model. Michael Backes 0001, Ian Goldberg 0001, Aniket Kate, Esfandiar Mohammadi |
CSF | 4 |
| 2010 | Computationally Sound Abstraction and Verification of Secure Multi-Party ComputationsabstractWe devise an abstraction of secure multi-party computations in the applied $\pi$-calculus. Based on this abstraction, we propose a methodology to mechanically analyze the security of cryptographic protocols employing secure multi-party computations. We exemplify the applicability of our framework by analyzing the SIMAP sugar-beet double auction protocol. We finally study the computational soundness of our abstraction, proving that the analysis of protocols expressed in the applied $\pi$-calculus and based on our abstraction provides computational security guarantees. Michael Backes 0001, Matteo Maffei, Esfandiar Mohammadi |
FSTTCS | 3 |