ABSTRACT. Game theory on graphs is a basic tool for solving various problems in computer science. In this paper, we propose a new game-theoretic framework for studying the privacy protection of a user who interactively uses a software service. Our framework is based on the idea that an objective of a user using software services should not be known to an adversary because the objective is often closely related to personal information of the user. We propose two new notions, O-indistinguishable strategy (O-IS) and objective-indistinguishability equilibrium (OIE). For a given game and a subset O of winning objectives (or objectives in short), a strategy of a player is O-indistinguishable if an adversary cannot shrink O by excluding any objective from O as an impossible objective. A strategy profile, which is a tuple of strategies of all players, is an OIE if the profile is locally maximal in the sense that no player can expand her set of objectives indistinguishable from her real objective from the viewpoint of an adversary. We show that for a given multiplayer game with Muller objectives, both of the existence of an O-IS and that of OIE are decidable.

ABSTRACT. Attack trees are a graphical formalism for security assessment. They are particularly valued for their explainability and high accessibil- ity without any security or formal-methods expertise. They can be used, for instance, to quantify the global insecurity of a system arising from the unreliability of its parts, graphically explain security bottlenecks, or identify additional vulnerabilities through their systematic decomposi- tion. However, in most cases, the main hindrance in the practical deploy- ment is the need for a domain expert to generate the tree manually or use further models. This paper demonstrates how to learn attack trees from logs, i.e., sets of traces, typically stored abundantly in many application domains. To this end, we design a genetic algorithm and apply them to classes of trees with different expressive power. Our experiments, also on real data, show that comparably simple yet highly accurate trees can be learned efficiently even from small data sets

ABSTRACT. Secure multi-party computation using a physical deck of cards, often called card-based cryptography, has been extensively studied during the past decade. Many card-based protocols to securely compute various Boolean functions have been developed. As each input bit is typically encoded by two cards, computing an $n$-variable Boolean function requires at least $2n$ cards. We are interested in optimal protocols that use exactly $2n$ cards. In particular, we focus on symmetric functions, where the output only depends on the number of 1s in the inputs. In this short paper, we formulate the problem of developing $2n$-card protocols to compute $n$-variable symmetric Boolean functions by classifying all such functions into several NPN-equivalence classes. We then summarize existing protocols that can compute some representative functions from these classes, and also solve some of the open problems by developing protocols to compute particular functions in the cases $n=4$, 5, 6, and 7.

ABSTRACT. Kleene algebras are one of the basic algebraic structures used in computer science, involving iteration, or Kleene star. An important subclass of Kleene algebras is formed by *-continuous ones. In his 2002 paper, Dexter Kozen pinpointed complexity of various logical theories for Kleene algebras, both in the general and in the *-continuous case. Those complexity results range from equational theories to Horn theories, or reasoning from hypotheses. In the middle, there are fragments of Horn theories, with restrictions on hypotheses. For the case when the hypotheses are commutativity conditions, i.e., commutation equations for designated pairs of atoms, however, Kozen mentioned the complexity result ($\Pi^0_1$-completeness) only for the *-continuous case, while the general case remained an open question. This was the only gap in Kozen's table of results, and the present paper fills this gap. Namely, we prove that reasoning from commutativity conditions on the class of all Kleene algebras is $\Sigma^0_1$-complete. In particular, this problem is undecidable.

ABSTRACT. Numerous proof methods have been proposed to establish language properties such as type soundness, confluence, strong normalization and others. However, literature does not provide a study on the complexity of carrying out these proof methods.

This paper provides an investigation on the complexity of carrying out the "syntactic approach" to type soundness (progress and type preservation theorem) for a class of functional languages, and characterizes the complexity of its proofs as a function of the number of expression constructors, number of typing rules, reduction rules, and other common quantities of operational semantics.

Although we do not claim to provide \emph{the} complexity of this approach, this paper provides the first example of complexity analysis of a programming language proof method.