The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.

Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently, Barthe, Hsu and Liao have proposed a new way of giving semantics to separation logic formulas in which separating conjunction is interpreted in terms of probabilistic independence. The latter is taken in its exact form, i.e., two events are independent if and only if the joint probability is the product of the probabilities of the two events. There is indeed a literature on weaker notions of independence which are computational in nature, i.e. independence holds only against efficient adversaries and modulo a negligible probability of success. The aim of this work is to explore the nature of computational independence in a cryptographic scenario, in view of the aforementioned advances in separation logic. We show on the one hand that the semantics of separation logic can be adapted so as to account for complexity bounded adversaries, and on the other hand that the obtained logical system is useful for writing simple and compact proofs of standard cryptographic results in which the adversary remains hidden. Remarkably, this allows for a fruitful interplay between independence and pseudorandomness, itself a crucial notion in cryptography.

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete - they capture all functions - but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To circumvent this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.

We extend the analysis of collision-resistant hash functions in the Linicrypt model presented by McQuoid, Swope & Rosulek (TCC 2019) in order to characterize preimage awareness, a security property defined by Dodis, Ristenpart & Shrimpton (Eurocrypt 2009), who also demonstrate its utility in the construction of indifferentiable hash functions. We present a simple and efficiently-checkable property of Linicrypt programs which characterizes preimage awareness. Finally, we show that this characterization may be efficiently automated and as an example, use it to enumerate all preimage-aware compression functions which use two calls to the random oracle. This includes several functions shown to be preimage aware by Dodis et. al. using hand-crafted proofs.

Abstract The class of Basic Feasible Functionals $$\mathtt{BFF}$$ BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of $$\mathtt{BFF}$$ BFF based on a typed programming language of terms. These terms may perform calls to imperative procedures, which are not recursive. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. $$\mathtt{BFF}$$ BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of $$\mathtt{BFF}$$ BFF , thus solving a problem opened for more than 20 years.

The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.

The class of Basic Feasible Functionals BFF2 is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF2 based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not restrain strongly the expressive power of the language.

This paper provides an alternate characterization of second-order polynomial-time computability, with the goal of making second-order complexity theory more approachable. We rely on the usual oracle machines to model programs with subroutine calls. In contrast to previous results, the use of higher-order objects as running times is avoided, either explicitly or implicitly. Instead, regular polynomials are used. This is achieved by refining the notion of oracle-poly-time computability introduced by Cook. We impose a further restriction on oracle interactions to force feasibility. Both the restriction and its purpose are very simple: it is well-known that Cook's model allows polynomial depth iteration of functional inputs with no restrictions on size, and thus does not preserve poly-time computability. To mend this we restrict the number of lookahead revisions, that is the number of times a query whose size exceeds that of any previous query may be asked. We prove that this leads to a class of feasible functionals and that all feasible problems can be solved within this class if one is allowed to separate a task into efficiently solvable subtasks. Formally, the closure of our class under lambda-abstraction and application are the basic feasible functionals. We also revisit the very similar class of strongly poly-time computable operators previously introduced by Kawamura and Steinberg. We prove it to be strictly included in our class and, somewhat surprisingly, to have the same closure property. This is due to the nature of the limited recursion operator: it is not strongly poly-time but decomposes into two such operations and lies in our class.

This paper introduces two models for influence in networks, and presents some upper and lower bounds for time needed to reach stability in these models. The first, called the Majority Model, is an expansion on the “Democrats and Republicans Model” that uses cascades to initialize the influence network rather than randomly assigning each node an initial opinion. By slightly modifying a network introduced by Frischknect, Keller, and Wattenhofer [10] to fit the specifications of the Majority Model, we show that Frischknecht et al.'s lower bound for stability of Ω(n3/2) on the Democrats and Republicans Model also holds in the Majority Model. The second model, called the Certainty Model, is the same as the Majority Model but with the addition of a variable for a node's certainty in its own opinion. Each node weights the opinions of its neighbors by their respective certainties and moves to the mass center of all of these opinions. For the Certainty Model we obtain two upper bounds related to time to stability. The first is a bound of O(d) for the time to reach stability once all nodes have gained an opinion, where d is the diameter of the graph. The second is a bound of O(n) on the time required for all nodes to gain an opinion.

Let Zn[i] be the ring of Gaussian integers modulo a positive integer n. Very recently, Camarero and Martinez et al. showed that for every prime number p > 5 such that p ≡ ±5 (mod 12), the Cayley graph ςp= Cay(Zp[i], S2), where S2is the set of units of Zp[i], induces a two-quasi-perfect Lee code over Zpm, where m = 2[p/4]. They also conjectured that ςpis a Ramanujan graph for every prime p, such that p ≡ 3 (mod 4). In this paper, we solve this conjecture. Our main tools are Deligne's bound from 1977 for estimating a particular kind of trigonometric sum and a result of Lovász from 1975 (or of Babai from 1979) which gives the eigenvalues of Cayley graphs of finite Abelian groups. Our proof techniques may motivate more work in the interactions between spectral graph theory, character theory, and coding theory, and may provide new ideas toward the famous Golomb-Welch conjecture on the existence of perfect Lee codes.

The dynamic graph connectivity problem is the following: given a graph on a fixed set of n nodes which is undergoing a sequence of edge insertions and deletions, answer queries of the form q(a, b): “Is there a path between nodes a and b?” While data structures for this problem with polylogarithmic amortized time per operation have been known since the mid-1990's, these data structures have Θ(n) worst case time. In fact, no previously known solution has worst case time per operation which is . We present a solution with worst case times O(log4 n) per edge insertion, O(log5 n) per edge deletion, and O (log n/log log n) per query. The answer to each query is correct if the answer is “yes” and is correct with high probability if the answer is “no”. The data structure is based on a simple novel idea which can be used to quickly identify an edge in a cutset. Our technique can be used to simplify and significantly speed up the preprocessing time for the emergency planning problem while matching previous bounds for an update, and to approximate the sizes of cutsets of dynamic graphs in time Õ(min{|S|, |V \ S|}) for an oblivious adversary.

The growing need to address privacy concerns when social network data is released for mining purposes has recently led to considerable interest in various techniques for graph anonymization. In this paper, we study the following problem: Given a social network modeled as an edge-labeled graph G, we aim to make a pre-specifled subset of vertices of G k-label sequence anonymous with the minimum number of edge additions. Here, the label sequence of a vertex is the sequence of labels of edges incident to it. The contributions of this paper are two fold: We provide a framework to show hardness results for different variants of social network anonymization using a common approach. We start by showing that k-label sequence anonymity of arbitrary labeled graphs is hard, and use this result to prove NP-hardness results for many other recently proposed notions of graph anonymization. Secondly, we present interesting algorithms and hardness for bipartite graphs. For unlabeled bipartite graphs, we show k-degree anonymity is in P for all k ≥ 2. For labeled bipartite graphs, we show that k-label sequence anonymity is in P for k = 2 but it is NP-hard for k ≥ 3.

Computational Indistinguishability Logic (CIL) is a logic for reasoning about cryptographic primitives in computational models. It captures reasoning patterns that are common in provable security, such as simulations and reductions. CIL is sound for the standard model, but also supports reasoning in the random oracle and other idealized models.

We resolve two long-standing open problems in distributed computation by describing polylogarithmic protocols for Byzantine agreement and leader election in the asynchronous full information model with a nonadaptive malicious adversary. All past protocols for asynchronous Byzantine agreement had been exponential, andnoprotocol for asynchronous leader election had been known. Our protocols tolerate up to (1/3 − ϵ) ⋅nfaulty processors, for any positive constant ϵ. They are Monte Carlo, succeeding with probability 1 −o(1) for Byzantine agreement, and constant probability for leader election. A key technical contribution of our article is a new approach for emulating Feige's lightest bin protocol, even with adversarial message scheduling.

We consider the problem of computing Byzantine Agreement in a synchronous network with n processors each with a private random string, where each pair of processors is connected by a private communication line. The adversary is malicious and non-adaptive, i.e., it must choose the processors to corrupt at the start of the algorithm. Byzantine Agreement is known to be computable in this model in an expected constant number of rounds.We consider a scalable model where in each round each uncorrupted processor can send to any set of log n other processors and listen to any set of log n processors. We define the loss of a computation to be the number of uncorrupted processors whose output does not agree with the output of the majority of uncorrupted processors. We show that if there are t corrupted processors, then any protocol which has probability at least 1/2 +1/log n of loss less than t 2/3 32fn1/3log5/3n requires at least f rounds.

We present two logical systems for reasoning about cryptographic constructions which are sound with respect to standard cryptographic definitions of security. Soundness of the first system is proved using techniques from nonstandard models of arithmetic. Soundness of the second system is proved by an interpretation into the first system. We also present examples of how these systems may be used to formally prove the correctness of some elementary cryptographic constructions.

We define notions of resource-bounded continuity and sequentiality for type-two functionals with total inputs, and prove that in the resource-bounded model there are continuous functionals which cannot be efficiently simulated by sequential functionals. We also show that for some naturally defined classes of continuous functionals an efficient simulation is possible.

We introduce a typed programming formalism, type-2 inflationary tiered loop programs or ITLP 2 , that characterizes the type-2 basic feasible functionals. ITLP 2 is based on Bellantoni and Cook's (1992) and Leivant's (1995) type-theoretic characterization of polynomial-time, and turns out to be closely related to Kapron and Cook's (1991; 1996) machine-based characterization of the type-2 basic feasible functionals.

We define notions of resource-bounded continuity and sequentiality for type-two functionals with total inputs, and prove that in the resource-bounded model there are continuous functionals which cannot be efficiently simulated by sequential functionals. We also show that for some naturally defined classes of continuous functionals, an efficient simulation is possible.

K. Mehlhorn introduced a class of polynomial-time-computable operators in order to study poly-time reducibilities between functions. This class is defined using a generalization of A. Cobham's definition of feasibility for type-1 functions to type-2 functionals. Cobham's feasible functions are equivalent to the familiar poly-time functions. We generalize this equivalence to type-2 functionals. This requires a definition of the notion “poly time in the length of type-1 inputs.” The proof of this equivalence is not a simple generalization of the proof for type-1 functions; it depends on the fact that Mehlhorn’s class is closed under a strong form of simultaneous limited recursion on notation and requires an analysis of the structure of oracle queries in time-bounded computations.

The primary aim of this paper is to introduce higher type analogues of some familiar parallel complexity classes, and to show that these higher type classes can be characterised in significantly different ways. Recursion-theoretic, proof-theoretic and machine-theoretic characterisations are given for various classes, providing evidence of their naturalness.>

It is shown that a 0-1 law holds for propositional modal logic, both for structure validity and for frame validity. In the case of structure validity, the result follows easily from the well-known 0-1 law for first-order logic. However, the proof gives considerably more information. It leads to an elegant axiomatization for almost-sure structure validity, and sharper complexity bounds. Since frame validity can be reduced to a II/sub 1//sup 1/ formula, the 0-1 law for frame validity helps delineate when 0-1 laws exist for second-order logics.>

A. Cobham (1964) presented a machine-independent characterization of computational feasibility, via inductive definition. R. Constable (1973) was apparently the first to consider the notion of feasibility for type 2 functionals. K. Mehlhorn's (1976) study of feasible reducibilities proceeds from Constable's work. Here, a class of polytime operators is defined, using a generalization of Cobham's definition. The authors provide an affirmative answer to the question of whether there is a natural machine based definition of Mehlhorn's class.>

The authors define a simple typed while-programming language that generalizes the sort of simple language used in computability texts to define the familiar numerical computable functions and corresponds roughly to the mu -recursion of R.O. Gandy (1967). This language does not fully capture the notion of higher type computability. The authors define run times for their programs and prove that the feasible functionals of S. Cook and A. Urquhart (1988) are precisely those functionals computable by typed while-programs with run times feasibly length-bounded. The authors introduce the notion of a bounded typed loop program and prove that a finite type functional is feasible if it is computable by a bounded typed loop program.>

Abstract The language of propositional modal logic is extended by the introduction of sequents. Validity of a modal sequent on a frame is defined, and modal sequent-axiomatic classes of frames are introduced. Through the use of modal algebras and general frames, a study of the properties of such classes is begun.