Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
The Security Lottery: Measuring Client-Side Web Security Inconsistencies
Get PDFTo mitigate a myriad of Web attacks, modern browsers support client-side security policies shipped through HTTP response headers. To enforce these defenses, the servers need to communicate them to the client, a seemingly straightforward process. However, users may access the same site in variegate ways, e.g., using different User-Agents, network access methods, or language settings. All these usage scenarios should enforce the same security policies, otherwise a security lottery would take place: depending on specific client characteristics, different levels of Web application security would be provided to users (inconsistencies). We formalize security guarantees provided through four popular mechanisms and apply this to measure the prevalence of inconsistencies in the security policies of top sites across different client characteristics. Based on our insights, we investigate the security implications of both deterministic and non-deterministic inconsistencies, and show how even prominent services are affected by them
An online notebook resource for reproducible inference, analysis and publication of gene regulatory networks
No full textAn online notebook resource for reproducible inference, analysis and publication of gene regulatory network
Explainable Arguments
Get PDFWe introduce an intriguing new type of argument systems with the additional property of being explainable. Intuitively by explainable, we mean that given any argument under a statement, and any witness, we can produce the random coins for which the Prove algorithm outputs the same bits of the argument.
This work aims at introducing the foundations for the interactive as well as the non-interactive setting. We show how to build explainable arguments from witness encryption and indistinguishability obfuscation. Finally, we show applications of explainable arguments. Notably, we construct deniable chosen-ciphertext secure encryption. Previous deniable encryption scheme achieved only chosen plaintext security
Temporal Causality in Reactive Systems
No full textCounterfactual reasoning is an approach to infer what causes an observed effect by analyzing the hypothetical scenarios where a suspected cause is not present. The seminal works of Halpern and Pearl have provided a workable definition of counterfactual causality for finite settings. In this paper, we propose an approach to check causality that is tailored to reactive systems, i.e., systems that interact with their environment over a possibly infinite duration. We define causes and effects as trace properties which characterize the input and observed output behavior, respectively. We then instantiate our definitions for ω-regular properties and give automata-based constructions for our approach. Checking that an ω-regular property qualifies as a cause can then be encoded as a hyperproperty model checking problem
Counting Small Induced Subgraphs with Hereditary Properties
Get PDFWe study the computational complexity of the problem #IndSub(\Phi) of counting k-vertex induced subgraphs of a graph G that satisfy a graph property \Phi. Our main result establishes an exhaustive and explicit classification for all hereditary properties, including tight conditional lower bounds under the Exponential Time Hypothesis (ETH):
- If a hereditary property \Phi is true for all graphs, or if it is true only for finitely many graphs, then #IndSub(\Phi) is solvable in polynomial time.
- Otherwise, #IndSub(\Phi) is #W[1]-complete when parameterised by k, and, assuming ETH, it cannot be solved in time f(k)*|G|^{o(k)} for any function f.
This classification features a wide range of properties for which the corresponding detection problem (as classified by Khot and Raman [TCS 02]) is tractable but counting is hard. Moreover, even for properties which are already intractable in their decision version, our results yield significantly stronger lower bounds for the counting problem.
As additional result, we also present an exhaustive and explicit parameterised complexity classification for all properties that are invariant under homomorphic equivalence.
By covering one of the most natural and general notions of closure, namely, closure under vertex-deletion (hereditary), we generalise some of the earlier results on this problem. For instance, our results fully subsume and strengthen the existing classification of #IndSub(\Phi) for monotone (subgraph-closed) properties due to Roth, Schmitt, and Wellnitz [FOCS 20]
If You Can’t Get Them to the Lab: Evaluating a Virtual Study Environment with Security Information Workers
Get PDFUsable security and privacy researchers use many study methodologies, including interviews, surveys, and laboratory studies. Of those, lab studies allow for particularly flexible setups, including programming experiments or usability evaluations of software. However, lab studies also come with challenges: Often, it is particularly challenging to recruit enough skilled participants for in-person studies. Especially researchers studying security information workers reported on similar recruitment challenges in the past. Additionally, situations like the COVID-19 pandemic can make in-person lab studies even more challenging. Finally, institutions with limited resources may not be able to conduct lab studies. Therefore, we present and evaluate a novel virtual study environment prototype, called OLab, that allows researchers to conduct lab-like studies remotely using a commodity browser. Our environment overcomes lab-like study challenges and supports flexible setups and comprehensive data collection. In an iterative engineering process, we design and implement a prototype based on requirements we identified in previous work and conduct a comprehensive evaluation including a cognitive walkthrough with usable security experts, a guided and supervised online study with DevOps, and an unguided and unsupervised online study with computer science students. We can confirm that our prototype supports a wide variety of lab-like study setups and received positive feedback from all study participants
Reproducibility and Replicability of Web Measurement Studies
Get PDFWeb measurement studies can shed light on not yet fully understood phenomena and thus are essential for analyzing how the modern Web works. This often requires building new and adjusting existing crawling setups, which has led to a wide variety of analysis tools for different (but related) aspects. If these efforts are not sufficiently documented, the reproducibility and replicability of the measurements may suffer - two properties that are crucial to sustainable research. In this paper, we survey 117 recent research papers to derive best practices for Web-based measurement studies and specify criteria that need to be met in practice. When applying these criteria to the surveyed papers, we find that the experimental setup and other aspects essential to reproducing and replicating results are often missing.
We underline the criticality of this finding by performing a large-scale Web measurement study on 4.5 million pages with 24 different measurement setups to demonstrate the influence of the individual criteria. Our experiments show that slight differences in the experimental setup directly affect the overall results and must be documented accurately and carefully
Subterm-based proof techniques for improving the automation and scope of security protocol analysis
Get PDFDuring the last decades, many advances in the field of automated security protocol analysis have seen the field mature and grow from being applicable to toy examples, to modeling intricate protocol standards and finding real-world vulnerabilities that extensive manual analysis had missed.
However, modern security protocols often contain elements for which such tools were not originally designed, such as protocols that construct, by design, terms of unbounded size, such as counters, trees, and blockchains. Protocol analysis tools such as Tamarin and ProVerif have some very restricted support, but typically lack the ability to effectively reason about dynamically growing unbounded-depth terms.
In this work, we introduce subterm-based proof techniques that are tailored for automated protocol analysis in the Tamarin prover. In several case studies, we show that these techniques improve automation (allow for analyzing more protocols, or remove the need for manually specified invariants), efficiency (reduce proof size for existing analyses), and expressive power (enable new kinds of properties). In particular, we provide the first automated proofs for TreeKEM, S/Key, and Tesla Scheme 2; and we show substantial benefits, most notably in WPA2 and 5G-AKA, two of the largest automated protocol proofs.
Note: An extended abstract of this paper appears at CSF 2023. This is the long version
Developing a Psychometric Scale to Measure One’s Valuation of Other People’s Privacy
Get PDFResearchers invested tremendous efforts in understanding and
measuring people’s perceptions, concerns, attitudes, and behaviors related to privacy risks from data gathering by online platforms, mobile devices, and other technologies. However, technology users often risk other people’s privacy by sharing their data actively (e.g., posting photos taken at public places online) or passively (e.g., granting mobile apps to access stored contacts). Moreover, technologies that continuously sense the environment and record behaviors and activities of everyone around them (e.g., smart assistants) are becoming pervasive. Thus, an instrument to quantify how much one values other people’s privacy is essential to understand technology adoption, attitudes and behaviors related to collecting and sharing data about non-users, inform the design of adaptive privacy enhancing technologies, and developing personalized technological or behavioral interventions to raise awareness and mitigate privacy risks. This abstract details a preliminary study towards developing such as scale. We report the methods of generating the initial item pool and findings from a pilot survey. We hope to get feedback from the community to improve the research design during the poster
presentation
A Weaker Faithfulness Assumption based on Triple Interactions
Get PDFOne of the core assumptions in causal discovery
is the faithfulness assumption—i.e. assuming that
independencies found in the data are due to separations in the true causal graph. This assumption can,
however, be violated in many ways, including xor
connections, deterministic functions or cancelling
paths. In this work, we propose a weaker assumption that we call 2-adjacency faithfulness. In contrast to adjacency faithfulness, which assumes that
there is no conditional independence between each
pair of variables that are connected in the causal
graph, we only require no conditional independence between a node and a subset of its Markov
blanket that can contain up to two nodes. Equivalently, we adapt orientation faithfulness to this
setting. We further propose a sound orientation
rule for causal discovery that applies under weaker
assumptions. As a proof of concept, we derive a
modified Grow and Shrink algorithm that recovers
the Markov blanket of a target node and prove its
correctness under strictly weaker assumptions than
the standard faithfulness assumption