skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Simplifying Game-Based Definitions: Indistinguishability up to Correctness and Its Application to Stateful AE
Often the simplest way of specifying game-based cryptographic definitions is apparently barred because the adversary would have some trivial win. Disallowing or invalidating these wins can lead to complex or unconvincing definitions. We suggest a generic way around this difficulty. We call it indistinguishability up to correctness, or IND|C. Given games G and H and a correctness condition C we define an advantage measure Adv^indc_{G,H,C} wherein G/H distinguishing attacks are effaced to the extent that they are inevitable due to C. We formalize this in the language of oracle silencing, an alternative to exclusion-style and penalty-style definitions. We apply our ideas to a domain where game-based definitions have been cumbersome: stateful authenticated-encryption (sAE). We rework existing sAE notions and encompass new ones, like replay-free AE permitting a specified degree of out-of-order message delivery.  more » « less
Award ID(s):
1717542
PAR ID:
10141383
Author(s) / Creator(s):
;
Date Published:
Journal Name:
Advances in Crytology -- CRYPTO 2018
Volume:
10992
Page Range / eLocation ID:
3-32
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Often the simplest way of specifying game-based cryptographic definitions is apparently barred because the adversary would have some trivial win. Disallowing or invalidating these wins can lead to complex or unconvincing definitions. We suggest a generic way around this difficulty. We call it indistinguishability up to correctness, or IND|C. Given games G and H and a correctness condition C we define an advantage measure Adv^indc_{G,H,C} wherein G/H distinguishing attacks are effaced to the extent that they are inevitable due to C. We formalize this in the language of oracle silencing, an alternative to exclusion-style and penalty-style definitions. We apply our ideas to a domain where game-based definitions have been cumbersome: stateful authenticated-encryption (sAE). We rework existing sAE notions and encompass new ones, like replay-free AE permitting a specified degree of out-of-order message delivery. 
    more » « less
  2. Abstract—Deploying machine learning models in production may allow adversaries to infer sensitive information about training data. There is a vast literature analyzing different types of inference risks, ranging from membership inference to reconstruction attacks. Inspired by the success of games (i.e. probabilistic experiments) to study security properties in cryptography, some authors describe privacy inference risks in machine learning using a similar game-based style. However, adversary capabilities and goals are often stated in subtly different ways from one presentation to the other, which makes it hard to relate and compose results. In this paper, we present a game-based framework to systematize the body of knowledge on privacy inference risks in machine learning. We use this framework to (1) provide a unifying structure for definitions of inference risks, (2) formally establish known relations among definitions, and (3) to uncover hitherto unknown relations that would have been difficult to spot otherwise. Index Terms—privacy, machine learning, differential privacy, membership inference, attribute inference, property inference 
    more » « less
  3. An ordered graph is a graph with a linear ordering on its vertices. The online Ramsey game for ordered graphs $$G$$ and $$H$$ is played on an infinite sequence of vertices; on each turn, Builder draws an edge between two vertices, and Painter colors it red or blue. Builder tries to create a red $$G$$ or a blue $$H$$ as quickly as possible, while Painter wants the opposite. The online ordered Ramsey number $$r_o(G,H)$$ is the number of turns the game lasts with optimal play. In this paper, we consider the behavior of $$r_o(G,P_n)$$ for fixed $$G$$, where $$P_n$$ is the monotone ordered path. We prove an $$O(n \log n)$$ bound on $$r_o(G,P_n)$$ for all $$G$$ and an $O(n)$ bound when $$G$$ is $$3$$-ichromatic; we partially classify graphs $$G$$ with $$r_o(G,P_n) = n + O(1)$$. Many of these results extend to $$r_o(G,C_n)$$, where $$C_n$$ is an ordered cycle obtained from $$P_n$$ by adding one edge. 
    more » « less
  4. Recent breakthroughs in deep-learning (DL) approaches have resulted in the dynamic generation of trace links that are far more accurate than was previously possible. However, DL-generated links lack clear explanations, and therefore non-experts in the domain can find it difficult to understand the underlying semantics of the link, making it hard for them to evaluate the link's correctness or suitability for a specific software engineering task. In this paper we present a novel NLP pipeline for generating and visualizing trace link explanations. Our approach identifies domain-specific concepts, retrieves a corpus of concept-related sentences, mines concept definitions and usage examples, and identifies relations between cross-artifact concepts in order to explain the links. It applies a post-processing step to prioritize the most likely acronyms and definitions and to eliminate non-relevant ones. We evaluate our approach using project artifacts from three different domains of interstellar telescopes, positive train control, and electronic healthcare systems, and then report coverage, correctness, and potential utility of the generated definitions. We design and utilize an explanation interface which leverages concept definitions and relations to visualize and explain trace link rationales, and we report results from a user study that was conducted to evaluate the effectiveness of the explanation interface. Results show that the explanations presented in the interface helped non-experts to understand the underlying semantics of a trace link and improved their ability to vet the correctness of the link. 
    more » « less
  5. Garbage collectors provide memory safety, an important step toward program correctness. However, correctness of the collector itself can be challenging to establish, given both the style in which such systems are written and the weakly-ordered memory accesses of modern hardware. One way to maximize benefits is to use a framework in which effort can be focused on the correctness of small, modular critical components from which various collectors may be composed. Full proof of correctness is likely impractical, so we propose to gain a degree of confidence in collector correctness by applying model checking to critical kernels within a garbage collection framework. We further envisage a model framework, paralleling the framework nature of the collector, in hope that it will be easy to create new models for new collectors. We describe here a prototype model structure, and present results of model checking both stop-the-world and snapshot-at-the-beginning concurrent marking. We found useful regularities of model structure, and that models could be checked within possible time and space budgets on capable servers. This suggests that collectors built in a modular style might be model checked, and further that it may be worthwhile to develop a model checking framework with a domain-specific language from which to generate those models. 
    more » « less