Petar Vukmirović
email: p.vukmirovic@vu.nl

Alexander Bentkamp
email: a.bentkamp@vu.nl

Jasmin Blanchette
email: j.c.blanchette@vu.nl

Simon Cruanes

Visa Nummelin
email: visa.nummelin@vu.nl

Sophie Tourret
email: sophie.tourret@inria.fr

Making Higher-Order Superposition Work

Superposition is among the most successful calculi for firstorder logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.

Introduction

In recent decades, superposition-based first-order automatic theorem provers have emerged as useful reasoning tools. They dominate at the annual CASC [START_REF] Sutcliffe | The CADE ATP System Competition-CASC[END_REF] theorem prover competitions, having always won the first-order theorem division. They are also used as backends to proof assistants [START_REF] Czajka | Hammer for Coq: Automation for dependent type theory[END_REF][START_REF] Kaliszyk | HOL(y)Hammer: Online ATP service for HOL Light[END_REF][START_REF] Paulson | Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers[END_REF], automatic higher-order theorem provers [START_REF] Steen | The higher-order prover Leo-III[END_REF], and software verifiers [START_REF] Filliâtre | Why3-where programs meet provers[END_REF]. The superposition calculus has only recently been extended to higher-order logic, resulting in λ-superposition [START_REF] Bentkamp | Superposition with lambdas[END_REF], which we developed together with Waldmann, as well as combinatory superposition [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF] by Bhayat and Reger.

Both higher-order superposition calculi were designed to gracefully extend first-order reasoning. As most steps in higher-order proofs tend to be essentially first-order, extending the most successful first-order calculus to higher-order logic seemed worth trying. Our first attempt at corroborating this conjecture was in 2019: Zipperposition 1.5, based on λ-superposition, finished third in the higherorder theorem division of CASC-27 [START_REF] Sutcliffe | The CADE-27 automated theorem proving system competition-CASC-27[END_REF], 12 percentage points behind the winner, the tableau prover Satallax 3.4 [START_REF] Brown | Reducing higher-order theorem proving to a sequence of SAT problems[END_REF].

Studying the competition results, we discovered that higher-order tableaux have some advantages over higher-order superposition. To bridge the gap, we developed techniques and heuristics that simulate the behavior of a tableau prover in the context of saturation. We implemented them in Zipperposition 2, which took part in CASC-J10 in 2020. This time, Zipperposition won the division, solving 84% of problems, a whole 20 percentage points ahead of the next best prover, Satallax 3.4. In this paper, we describe the main techniques that explain this reversal of fortunes. They range from preprocessing to backend integration.

Interesting patterns can be observed in various higher-order encodings of problems. We show how we can exploit these to simplify problems (Sect. 3). By working on formulas rather than clauses, tableau techniques take a more holistic view of a higher-order problem. Delaying the clausification through the use of calculus rules that act on formulas achieves the same effect in superposition. We further explore the benefits of this approach (Sect. 4).

The main drawback of λ-superposition compared with combinatory superposition is that it relies on rules that enumerate possibly infinite sets of unifiers. We describe a mechanism that interleaves performing infinitely branching inferences with the standard saturation process (Sect. 5). The prover retains the same behavior as before on first-order problems, smoothly scaling with increasing numbers of higher-order clauses. We also propose some heuristics to curb the explosion induced by highly prolific λ-superposition rules (Sect. 6).

Using first-order backends to finish the proof is common practice in higherorder reasoning. Since λ-superposition coincides with standard superposition on first-order clauses, invoking backends may seem redundant; yet Zipperposition is nowhere as efficient as E [START_REF] Schulz | Faster, higher, stronger: E 2.3[END_REF] or Vampire [START_REF] Kovács | First-order theorem proving and Vampire[END_REF], so invoking a more efficient backend does make sense. We describe how to achieve a balance between allowing native higher-order reasoning and delegating reasoning to a backend (Sect. 7).

Finally, we compare Zipperposition 2 with other provers on all monomorphic higher-order TPTP benchmarks [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure-from CNF to TH0, TPTP v6.4.0[END_REF] to perform a more extensive evaluation than at CASC (Sect. 8). Our evaluation corroborates the competition results.

Background and Setting

We focus on monomorphic higher-order logic, but the techniques can easily be extended with polymorphism. Indeed, Zipperposition already supports some techniques polymorphically.

Higher-Order Logic. We define terms s, t, u, v inductively as free variables F, X, bound variables x, y, z, . . . , constants f, g, a, b, . . . , applications s t, and λabstractions λx. s. The syntactic distinction between free and bound variables gives rise to loose bound variables (e.g., y in λx. y a) [START_REF] Nipkow | Functional unification of higher-order patterns[END_REF]. We let s t n stand for s t 1 . . . t n and λx n . s for λx 1 . . . . λx n . s. Every β-normal term can be written as λx m . s t n , where s is not an application; we call s the head of the term. If the type of a term t is of the form

τ 1 → • • • → τ n → o,
where o is the distinguished Boolean type and n ≥ 0, we call t a predicate. A literal l is an equation s ≈ t or a disequation s ≈ t. A clause is a finite multiset of literals, interpreted and written disjunctively l 1 ∨ • • • ∨ l n . Logical symbols that may occur within terms are written in boldface: ¬ ¬ ¬, ∧ ∧ ∧, ∨ ∨ ∨, → → →, ↔ ↔ ↔, . . . . Predicate literals are encoded as (dis)equations with based on their sign; for example, even(x) becomes even(x) ≈ , and ¬ even(x) becomes even(x) ≈ .

Higher-Order Calculi. The λ-superposition calculus is a refutationally complete inference system and redundancy criterion for Boolean-free extensional polymorphic clausal higher-order logic. The calculus relies on complete sets of unifiers (CSUs). The CSU for s and t with respect to a set of variables V , denoted by CSU V (s, t), is a set of unifiers such that for any unifier of s and t, there exist substitutions σ ∈ CSU V (s, t) and θ such that (X) = σ(θ(X)) for all variables X ∈ V . The set X is used to distinguish between important and auxiliary variables. We usually omit it. A pragmatic, incomplete extension of λ-superposition with interpreted Booleans is described by Vukmirović and Nummelin [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF]. This forms the basis of most of this work. Recently, a refutationally complete extension was developed by Bentkamp et al. [START_REF] Bentkamp | Superposition for full higher-order logic[END_REF]; it is not considered here.

By contrast, the combinatory superposition calculus avoids CSUs by using a form of first-order unification, but essentially it enumerates higher-order terms using rules that instantiate applied variables with partially applied combinators from the complete combinator set {S, K, B, C, I}. This calculus is the basis of Vampire 4.5 [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF], which finished closely behind Satallax 3.4 at CASC-J10.

A different, very successful calculus is Satallax's SAT-guided tableaux [START_REF] Backes | Analytic tableaux for higher-order logic with choice[END_REF]. Satallax was the leading higher-order prover of the 2010s. Its simple and elegant tableaux avoid deep superposition-style rewriting inferences. Nevertheless, our working hypothesis for the past six years has been that superposition would likely provide a stronger basis for higher-order reasoning. Other competing higher-order calculi include SMT (implemented in CVC4 [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF][START_REF] Barrett | CVC4[END_REF]) and extensional paramodulation (implemented in Leo-III [START_REF] Steen | The higher-order prover Leo-III[END_REF]).

Zipperposition. Zipperposition [START_REF] Bentkamp | Superposition with lambdas[END_REF][START_REF] Cruanes | Extending superposition with integer arithmetic, structural induction, and beyond[END_REF] is a higher-order theorem prover based on a pragmatic extension of λ-superposition. It was conceived as a testbed for rapidly experimenting with extensions of first-order superposition, but over time, it has assimilated many of E's techniques and heuristics. Zipperposition 2 also implements combinatory superposition.

Several of our techniques extend the given clause procedure [30, Section 2.3], the standard saturation procedure. It partitions the proof state into a set P of passive clauses and a set A of active clauses. Initially, P contains all input clauses, and A is empty. At each iteration, a given clause C from P is moved to A (i.e., it is activated ), all inferences between C and clauses in A are performed, and the conclusions are added to P . Because Zipperposition fully simplifies clauses only when they are activated, it implements a DISCOUNT-style loop [START_REF] Denzinger | DISCOUNT-a distributed and learning equational prover[END_REF].

Experimental Setup. To assess our techniques, we carried out experiments with Zipperposition 2. We used all 2606 monomorphic higher-order problems from the TPTP library [START_REF] Sutcliffe | The TPTP problem library and associated infrastructure-from CNF to TH0, TPTP v6.4.0[END_REF], version 7.2.0, as benchmarks. Although some techniques support polymorphism, we uniformly used the monomorphic benchmarks. We fixed a base configuration of Zipperposition parameters as a baseline for all comparisons. Then, in each experiment, we varied the parameters associated with a specific technique to evaluate it. The experiments were run on StarExec [START_REF] Stump | Starexec: A cross-community infrastructure for logic solving[END_REF] servers, equipped with Intel Xeon E5-2609 CPUs clocked at 2.40 GHz. Unless otherwise stated, we used a CPU time limit of 20 s, roughly the time each configuration is given in the portfolio mode used for CASC. The raw evaluation results are available online. 53 Preprocessing Higher-Order Problems

The TPTP library contains thousands of higher-order problems. Despite their diversity, they have a markedly different flavor from the TPTP first-order problems. Notably, they extensively use the definition role to identify universally quantified equations (or equivalences) that define symbols.

Definitions can be replaced by rewrite rules, using the orientation given in the input problem. If there are multiple definitions for the same symbol, only the first one is replaced by a rewrite rule. Then, whenever a clause is picked in the given clause procedure, it will be rewritten using the collected rules. Since the TPTP format enforces no constraints on definitions, rewriting might diverge. To ensure termination, we limit the number of applied rewrite steps. In practice, most TPTP problems are well behaved: Only one definition is given for each symbol, and the definitions are acyclic. Instead of rewriting a clause when it is activated, we can rewrite the input formulas as a preprocessing step. This ensures that the input clauses will be fully simplified when the proving process starts and no defined symbols will occur in clauses, which usually helps the heuristics.

Eagerly unfolding the definitions and β-reducing can eliminate all of a problem's higher-order features, making it amendable to first-order methods. However, this can inflate the problem beyond recognition and compromise the refutational completeness of superposition.

To keep completeness, we can try to orient the definitions using the term order that parameterized superposition and rely on demodulation to simplify the proof state. Usually, the Knuth-Bendix order (KBO) [START_REF] Knuth | Simple word problems in universal algebras[END_REF] is used. It compares terms by first comparing their weights, which is the sum of all the weights assigned to the symbols it contains. Given a symbol weight assignment W, we can update it so that it orients acyclic definitions from left to right assuming that they are of the form f X m ≈ λy n . t, where the only free variables in t are X m , no free variable repeats or appears applied in t, and f does not occur in t. Then we traverse the symbols f that are defined by such equations following the dependency relation, starting with a symbol f that does not depend on any other defined symbol. For each f, we set W(f) to w + 1, where w is the maximum weight of the right-hand sides of f's definitions, computed using W. By construction, for each equation the left-hand side is heavier. Thus, the equations are orientable from left to right.

Evaluation and Discussion. The base configuration treats axioms annotated with definition as rewrite rules, and it preprocesses the formulas using the rewrite rules. We also tested the effects of disabling this preprocessing (-preprocess), disabling the special treatment of definition axioms (-RW), and disabling the special treatment of definition while using adjusted KBO Fig. 2: Effect of clausification and lightweight AVATAR weights as described above (-RW+KBO). The results are given in Figure 1. In all of the figures in this paper, each cell gives the number of proved problems; the highest number is typeset in bold. Clearly, treating definition axioms as rewrite rules greatly improves performance. Using adjusted KBO weights is not as strong, although it proves 15 problems not proved using other configurations.

Reasoning about Formulas

Higher-order logic identifies terms and formulas. To prove a problem, we often need to instantiate a variable with the right predicate. Finding this predicate can be easier if the problem is not clausified. Consider the conjecture ∃ ∃ ∃f. f p q ↔ ↔ ↔ p∧ ∧ ∧q.

Expressed in this form, the formula is easy to prove by taking f := λx y. x ∧ ∧ ∧ y. By contrast, guessing the right instantiation for the negated, clausified form F p q ≈ ∨ p ≈ ∨ q ≈ , F p q ≈ ∨ p ≈ , F p q ≈ ∨ q ≈ is more challenging. One of the strengths of higher-order tableau provers is that they do not clausify the input problem. This might explain Satallax's dominance in the THF division of CASC competitions until CASC-J10.

We studied techniques to incrementally clausify formulas during proof search in incomplete [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF] and complete [START_REF] Bentkamp | Superposition for full higher-order logic[END_REF] extensions of λ-superposition. Both approaches include the same set of (outer ) delayed clausification rules that clausify top-level logical symbols, proceeding outside in; for example, a clause C ∨ (p ∧ ∧ ∧ q) ≈ is transformed into C ∨ p ≈ ∨ q ≈ . The complete approach requires additional inference rules; it also supports inner delayed clausification. We focus on the pragmatic, incomplete approach and do not consider inner clausification due to its poor performance [START_REF] Bentkamp | Superposition for full higher-order logic[END_REF].

Delayed clausification rules can be used as inference rules (which add conclusions to the passive set) or as simplification rules (which delete premises and add conclusions to the passive set). Inferences are more flexible because they produce all intermediate clausification states, whereas simplifications produce fewer clauses. Since clausifying equivalences can destroy a lot of syntactic structure [START_REF] Ganzinger | Superposition with equivalence reasoning and delayed clause normal form transformation[END_REF], we never apply simplifying clausification rules on them.

We discuss two tableau-inspired approaches for reasoning about formulas. First, we study how clause-splitting techniques interfere with delayed clausification. Second, we discuss heuristic instantiation of quantifiers during saturation.

Zipperposition supports a lightweight variant of AVATAR [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF], an architecture that partitions the search space by splitting clauses into variable-disjoint subclauses. This variant of AVATAR is described by Ebner et al. [START_REF] Ebner | Unifying splitting[END_REF]. Combining lightweight AVATAR and delayed clausification makes it possible to split a clause (ϕ

1 ∨ ∨ ∨ • • • ∨ ∨ ∨ ϕ n ) ≈
, where the ϕ i 's are arbitrarily complex formulas that share no free variables with each other, into clauses ϕ i ≈ .

To finish the proof, it suffices to derive ⊥ under each assumption ϕ i ≈ . Since the split is performed at the formula level, this technique resembles tableaux, but it exploits the strengths of superposition, such as its powerful redundancy criterion and simplification machinery, to close the branches.

Interleaving clausification and saturation allows us to simulate another tableau technique. Whenever dynamic clausification replaces the predicate variable x in a clause of the form (∀ ∀ ∀x. ϕ) ≈ ∨ C with a fresh variable X, resulting in ϕ{x → X} ≈ ∨ C, we can create additional clauses in which x is replaced with t ∈ Inst, where Inst is a set of heuristically chosen terms. This set contains λ-abstractions whose bodies are formulas and which occur in activated clauses, and primitive instantiations [START_REF] Vukmirović | Boolean reasoning in a higher-order superposition prover[END_REF]-that is, imitations (in the sense of higher-order unification) of logical symbols that approximate the shape of a predicate that can instantiate a predicate variable.

However, as a new term t can be added to Inst after a clause with a quantified variable of the same type as t has been activated, we must also keep track of the clauses ϕ{x → X} ≈ ∨ C, so that when Inst is extended, we instantiate the saved clauses. Conveniently, instantiated clauses are not recognized as subsumed, since Zipperposition uses an optimized but incomplete subsumption algorithm.

Given a disequation f s n ≈ f t n , the abstraction of s i is λx. u ≈ ≈ ≈ v, where u is obtained by replacing s i with x in f s n and v is obtained by replacing s i with x in f t n . For f s n ≈ f t n , the analogous abstraction is λx.

¬ ¬ ¬ (u ≈ ≈ ≈ v).
Adding abstractions of the conjecture literals to Inst can provide useful instantiations for formulas such as induction principles for datatypes. As the conjecture is negated, the equation's polarity is inverted in the abstraction. Consider the TPTP problem DAT056^2 [START_REF] Sultana | LEO-II and Satallax on the Sledgehammer test bench[END_REF], whose clausified negated conjecture is ap xs (ap ys zs) ≈ ap (ap xs ys) zs, where ap is the append operator defined recursively on its first argument and xs, ys, and zs are of list type. Abstracting xs from the disequation yields t = λx. ap x (ap ys zs) ≈ ≈ ≈ ap (ap x ys) zs, which is added to Inst. Included in the problem is the induction axiom for the list datatype:

∀ ∀ ∀p. (p nil ∧ ∧ ∧ (∀ ∀ ∀x xs. p xs → → → p (cons x xs))) → → → ∀ ∀ ∀xs. p xs,
where nil and cons have the usual meanings. Instantiating p with t and using the ap definition, we can prove ∀ ∀ ∀x. ap x (ap ys zs) ≈ ≈ ≈ ap (ap x ys) zs, from which we easily derive a contradiction.

Evaluation and Discussion. The base configuration uses immediate clausification (IC), an approach that applies a standard clausification algorithm [START_REF] Nonnengart | Computing small clause normal forms[END_REF] both as a preprocessing step and whenever predicate variables are instantiated. Zipperposition's lightweight AVATAR is disabled in the base configuration. To test the merits of delayed clausification, we vary base's parameters along two axes: We choose immediate clausification (IC), delayed clausification as inference (DCI), or delayed clausification as simplification (DCS), and we either enable (+LA) or disable (-LA) the lightweight AVATAR. The base configuration does not use instantiation with terms from Inst.

Figure 2 shows that using delayed clausification as simplification greatly increases the success rate, while using delayed clausification as inference has the opposite effect. Manually inspecting the proofs found by the DCS configuration, we noticed that a main reason for its success is that it does not simplify away equivalences. Overall, the lightweight AVATAR harms performance, but the sets of problems proved with and without it are vastly different. For example, the IC+LA configuration proves 60 problems not proved by IC-LA.

The Boolean instantiation technique presented above requires delayed clausification. To test its effects, we enabled it in the best configuration from Figure 2, DCS-LA. With this change, Zipperposition proves 1744 problems, 36 of which cannot be proved by any other configuration in the same figure. Boolean instantiation is the only way in which Zipperposition 2 can prove higher-order problems requiring reasoning about induction axioms (e.g., DAT056^2).

Enumerating Infinitely Branching Inferences

As an optimization and to simplify the implementation, Leo-III [START_REF] Steen | Extensional paramodulation for higher-order logic and its effective implementation Leo-III[END_REF] and Vampire 4.4 [START_REF] Bhayat | Restricted combinatory unification[END_REF] (which uses a predecessor of combinatory superposition) compute only a finite subset of the possible conclusions for inferences that require enumerating a CSU. Not only is this a source of incompleteness, but choosing the cardinality of the computed subset is a difficult heuristic choice. Small sets can result in missing the unifier necessary for the proof, whereas large sets make the prover spend a long time in the unification procedure, generate useless clauses, and possibly get sidetracked into the wrong parts of the search space.

We propose a modification to the given clause procedure to seamlessly interleave unifier computation and proof state exploration. Given a complete unification procedure, which may yield infinite streams of unifiers, our modification fairly enumerates all conclusions of inferences relying on elements of a CSU. Under some reasonable assumptions, it behaves exactly like the standard given clause procedure on purely first-order problems. We also describe heuristics that help achieve a similar performance as when using incomplete, terminating unification procedures without sacrificing completeness.

Given the undecidability of the question as to whether there exists a next CSU element in a stream of unifiers, the request for the next conclusion might not terminate, effectively bringing the theorem prover to a halt. Our modified given clause procedure expects the unification procedure to return a lazily computed stream [START_REF] Okasaki | Purely functional data structures[END_REF]Sect. 4.2], each element of which is either ∅ or a singleton set containing a unifier. To avoid getting stuck waiting for a unifier that may not exist, the unification procedure should return ∅ after it performs a number of operations without finding a unifier.

The complete unification procedure by Vukmirović et al. [START_REF] Vukmirović | Efficient full higher-order unification[END_REF] returns such a stream. Other procedures such as Huet's [START_REF] Huet | A unification algorithm for typed lambda-calculus[END_REF] and Jensen and Pietrzykowski's [START_REF] Jensen | Mechanizing omega-order type theory through unification[END_REF] can easily be adapted to meet this requirement. Based on the stream of unifiers interspersed with ∅, we can construct a stream of inferences similarly interspersed with ∅ of which any finite prefixes can be computed in finite time.

To support such streams in the given clause procedure, we extend it to represent the proof state not only by the active (A) and passive (P ) clause sets, but also by a priority queue Q containing the inference streams. Each stream is associated with a weight, and Q is sorted in order of increasing weight. Elsewhere [START_REF] Bentkamp | Superposition with lambdas[END_REF] Initially, all input clauses are put into P , and A and Q are empty. Unlike in the standard given clause procedure, inference results are represented as clause streams. The first element is inserted into P , and the rest of the stream is stored in Q with some positive integer weight computed from the inference rule.

To eventually consider inference conclusions from streams in Q as given clauses, we extract elements from, or probe, streams and move any obtained clauses to P . Analogously to the traditional pick-given ratio [START_REF] Mccune | Otter-the CADE-13 competition incarnations[END_REF][START_REF] Schulz | E-a brainiac theorem prover[END_REF], we use a parameter K fair (by default, K fair = 70) to ensure fairness: Every K fair th iteration, FairProbe probes an increasing number of oldest streams, which achieves dovetailing. In all other iterations, HeuristicProbe attempts to extract up to K best clauses from the most promising streams (by default, K best = 7). In each attempt, the most promising stream in Q is chosen. If its first element is ∅, the rest of the stream is inserted into Q, and a new stream is chosen. This is repeated until either K retry occurrences of ∅ have been met (by default, K retry = 20) or the stream yields a singleton set. Setting K retry > 0 increases the chance that HeuristicProbe will return K best clauses, as desired. Finally, if P becomes empty, ForceProbe searches relentlessly for a clause in Q, as a fallback.

The function ExtractClause extracts an element from a nonempty stream not in Q and inserts the remaining stream into Q with an increased weight, calculated as follows. Let n be the number of times the stream was chosen for probing. If probing results in ∅, the stream's weight is increased by max {2, n -16}. If probing results in a clause C whose penalty is p, the stream's weight is increased by p • max {1, n -64}. The penalty of a clause is a number assigned by Zipperposition based on features such as the depth of its derivation and the rules used in it. The constants 16 and 64 increase the chance that newer streams are picked, which is desirable because their first clauses are expected to be useful.

All three probing functions are invoked by GivenClause, which forms the body of the saturation loop. It differs from the standard given clause procedure in three ways: First, the proof state includes Q in addition to P and A. Second, new inferences involving the given clause are added to Q instead of being performed immediately. Third, inferences in Q are periodically performed lazily to fill P .

GivenClause eagerly stores the first element of a new inference stream in P to imitate the standard given clause procedure. If the underlying unification procedure behaves like the standard first-order unification algorithm on higherorder logic's first-order fragment, our given clause procedure coincides with the standard one. The unification procedure by Vukmirović et al. terminates on the first-order and other fragments [START_REF] Nipkow | Functional unification of higher-order patterns[END_REF], and for problems outside these fragments, it immediately returns ∅ to avoid computing complicated unifiers eagerly.

Evaluation and Discussion. When the unification procedure of Vukmirović et al. was implemented in Zipperposition, it was observed that Zipperposition is the only competing higher-order prover that proves all Church numeral problems from the TPTP, never spending more than 5 seconds on the problem [START_REF] Vukmirović | Efficient full higher-order unification[END_REF].

Consider the TPTP problem NUM800^1, which requires finding a function

F such that F c 1 c 2 ≈ ≈ ≈ c 2 ∧ ∧ ∧ F c 2 c 3 ≈ ≈ ≈ c 6
, where c n abbreviates the Church numeral for n, λs z. s n (z). To prove it, it suffices to take F to be the multiplication operator λx y s z. x (y s) z. However, this unifier is only one out of many available for each occurrence of F .

In an independent evaluation setup on the same set of 2606 problems used in this paper, Vukmirović et al. compared a complete, nonterminating variant and a pragmatic, terminating variant of the unification procedure [START_REF] Vukmirović | Efficient full higher-order unification[END_REF]Sect. 7]. The pragmatic variant was used directly-all the inference conclusions were put immediately in P , bypassing Q. The complete variant, which relies on possibly infinite streams and is much more prolific, proved only 15 problems less than the most competitive pragmatic variant. Furthermore, it proved 19 problems not proved by the pragmatic variant. This shows that our given clause procedure, with its heuristics, allows the prover to defer exploring less promising branches of the unification and uses the full power of a complete higher-order unifier search to solve unification problems that cannot be solved by a crippled procedure.

Among the competing higher-order theorem provers, only Satallax uses infinitely branching calculus rules. It maintains a queue of "commands" that contain instructions on how to create a successor state in the tableau. One command describes infinite enumeration of all closed terms of a given function type. Each execution of this command makes progress in the enumeration. Unlike evaluation of streams representing elements of CSU, each command execution is guaranteed to make progress in enumerating the next closed functional term, so there is no need to ever return ∅.

Controlling Prolific Rules

To support higher-order features such as function extensionality and quantification over functions, many refutationally complete calculi employ highly prolific rules. For example, λ-superposition uses a rule FluidSup [START_REF] Bentkamp | Superposition with lambdas[END_REF] that very often applies to two clauses if one of them contains a term of the form F s n , where n > 0. We describe three mechanisms to keep rules like these under control.

First, we limit applicability of the prolific rules. In practice, it often suffices to apply prolific higher-order rules only to initial or shallow clauses-clauses with a shallow derivation depth. Thus, we added an option to forbid the application of a rule if the derivation depth of any premise exceeds a limit.

Second, we penalize the streams of expensive inferences. The weight of each stream is given an initial value based on characteristics of the inference premises such as their derivation depth. For prolific rules such as FluidSup, we increment this value by a parameter K incr . Weights for less prolific variants of this rule, such as DupSup [START_REF] Bentkamp | Superposition with lambdas[END_REF], are increased by a fraction of K incr (e.g., K incr /3 ).

Third, we defer the selection of prolific clauses. To select the given clause, most saturating provers evaluate clauses according to some criteria and select the clause with the lowest evaluation. For this choice to be efficient, passive clauses are organized into a priority queue ordered by their evaluations. Like E, Zipperposition maintains multiple queues, ordered by different evaluations, that are visited in a round-robin fashion. It also uses E's two-layer evaluation functions, a variant of which has recently been implemented in Vampire [START_REF] Gleiss | Layered clause selection for theory reasoning (short paper)[END_REF]. The two layers are clause priority and clause weight. Clauses with higher priority are preferred, and the weight is used for tie-breaking. Intuitively, the first layer crudely separates clauses into priority classes, whereas the second one uses heuristic weights to prefer clauses within a priority class. To control the selection of prolific clauses, we introduce new clause priority functions that take into account features specific to higher-order clauses.

The first new priority function PreferHOSteps (PHOS) assigns a higher priority if rules specific to λ-or combinatory superposition were used in the clause derivation. Since most of the other clause priority functions tend to defer higherorder clauses, having a clause queue that prefers the results of higher-order inferences might be necessary to find a proof more efficiently. A simpler function, which prefers clauses containing λ-abstractions, is PreferLambda (PL).

We also introduce the priority function ByNormalizationFactor (BNF), inspired by the observation that a higher-order inference that applies a complicated substitution to a clause is usually followed by a βη-normalization step. If βη-normalization greatly reduces the size of a clause, it is likely that this substitution simplifies the clause (e.g., by removing a variable's arguments). Thus, this function prefers clauses that were produced by βη-normalization, and among those it prefers the ones with larger size reductions.

Another new priority function is PreferShallowAppVars (PSAV). This prefers clauses with lower depths of the deepest occurrence of an applied variable-that is, C[X a] is preferred over C[f (X a)]. This function tries to curb the explosion of both λ-and combinatory superposition: Applying a substitution to a top-level applied variable often reduces this applied variable to a term with a constant head, which likely results in a less explosive clause. Among the functions that rely on properties of applied variables we implemented PreferDeepAppVars (PDAV), which returns the priority opposite of PSAV, and ByAppVarNum (BAVN), which prefers clauses with fewer occurrences of applied variables.

Evaluation and Discussion. In the base configuration, Zipperposition visits several clause queues, one of which uses the constant priority function ConstPrio (CP). To evaluate the new priority functions, we replaced the queue ordered by CP with the queue ordered by one of the new functions, leaving the clause weight intact. The results are shown in Figure 3. It shows that the expensive priority FluidSup is disabled in base because it is so explosive. To test if increasing inference stream weights makes a difference on the success rate, we enabled FluidSup and used different weight increments K incr for FluidSup inference queues. The results are shown in Figure 4. As expected, using a low increment with FluidSup is detrimental to performance. However, as the column for K incr = 16 shows, nor should we use too high an increment, since that delays useful FluidSup inferences. Interestingly, even though the configuration with K incr = 1 proves the least problems overall, it proves 7 problems not proved by base, which is more than any other configuration we tried.

Controlling the Use of Backends

Cooperation with efficient first-order theorem provers is an essential feature of higher-order theorem provers such as Leo-III [START_REF] Steen | Extensional paramodulation for higher-order logic and its effective implementation Leo-III[END_REF]Sect. 4.4] and Satallax [START_REF] Brown | Reducing higher-order theorem proving to a sequence of SAT problems[END_REF]. Those provers invoke first-order backends repeatedly during a proof attempt and spend a substantial amount of time in backend collaboration. Since λ-superposition generalizes a highly efficient first-order calculus, we expect that future efficient λ-superposition implementations will not benefit much from backends. Experimental provers such as Zipperposition can still gain a lot. We present some techniques for controlling the use of backends.

In his thesis [START_REF] Steen | Extensional paramodulation for higher-order logic and its effective implementation Leo-III[END_REF]Sect. 6.1], Steen extensively evaluates the effects of using different first-order backends on the performance of Leo-III. His results suggest that adding only one backend already substantially improves the performance. To reduce the effort required for integrating multiple backends, we chose Ehoh [START_REF] Vukmirović | Extending a brainiac prover to lambda-free higher-order logic[END_REF] as our single backend. Ehoh is an extension of the highly optimized superposition prover E with support for higher-order features such as partial application, applied variables, and interpreted Booleans. On the one hand, Ehoh provides the efficiency of E while easing the translation from full higher-order logic: The only missing syntactic feature is λ-abstraction. On the other hand, Ehoh's higher- In a departure from Leo-III and other cooperative provers, we invoke the backend at most once during a run of the prover. This is because most competitive higher-order provers use a portfolio mode in which many configurations are run for a short time, and we want to leave enough time for native higher-order reasoning. Moreover, multiple backend invocations tend to be wasteful, because currently each invocation starts with no knowledge of the previous ones.

Only a carefully chosen subset of the available clauses are translated and sent to Ehoh. Let I be the set of input clauses. Given a proof state, let M = P ∪ A, and let M ho denote the subset of M that contains only clauses that were derived using at least one λ-superposition-specific inference rule. We order the clauses in M ho by increasing derivation depth, using syntactic weight to break ties. Then we choose all clauses in I and the first K size clauses from M ho for use with the backend reasoner. We leave out clauses in M \(I∪M ho ) because Ehoh can rederive them. We also expect large clauses with deep derivations to be less useful.

The remaining step is the translation of λ-abstractions. We support two translation methods: λ-lifting [START_REF] Johnsson | Lambda lifting: Transforming programs to recursive equations[END_REF] and SKBCI combinators [START_REF] Turner | Another algorithm for bracket abstraction[END_REF]. For SKBCI, we omit the combinator definition axioms, because they are very explosive [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF]. A third mode simply omits clauses containing λ-abstractions.

Evaluation and Discussion. In Zipperposition, we can adjust the CPU time allotted to Ehoh, Ehoh's own proof search parameters, the point when Ehoh is invoked, the number K size of selected clauses from M ho , and the λ translation method. We fix the time limit to 5 s, use Ehoh in auto mode, and focus on the last three parameters. In base, collaboration with Ehoh is disabled.

Ehoh is invoked after K time •t CPU seconds, where 0 ≤ K time < 1 and t is the total CPU time allotted to Zipperposition. Figure 5 shows the effect of varying K time when K size = 32 and λ-lifting is used. The evaluation confirms that using a highly optimized backend such as Ehoh greatly improves the performance of a less optimized prover such as Zipperposition. The figure indicates that it is preferable to invoke the backend early. We have indeed observed that if the backend Fig. 8: Comparison of competing higher-order theorem provers is invoked late, small clauses with deep derivations tend to be present by then. These clauses might have been used to delete important shallow clauses already. But due to their derivation depth, they will not be translated. In such situations, it is better to invoke the backend before the important clauses are deleted. Figure 6 quantifies the effects of the three λ-abstraction translation methods. We fixed K time = 0.25 and K size = 32. The clear winner is λ-lifting. Omitting clauses with λ-abstractions performs comparably to SKBCI combinators.

Figure 7 shows the effect of K size on performance, with K time = 0.25 and λ-lifting. We find that including a small number of higher-order clauses with the lowest weight performs better than including a large number of such clauses.

Comparison with Other Provers

Different choices of parameters lead to noticeably different sets of proved problems. In an attempt to use Zipperposition 2 to its full potential, we have created a portfolio mode that runs up to 50 configurations in parallel during the allotted time. To provide some context, we compare Zipperposition 2 with the latest versions of all higher-order provers that competed at CASC-J10: CVC4 1.8 [START_REF] Barrett | CVC4[END_REF], Leo-III 1.5 [START_REF] Steen | The higher-order prover Leo-III[END_REF], Satallax 3.5 [START_REF] Brown | Reducing higher-order theorem proving to a sequence of SAT problems[END_REF], and Vampire 4.5 [START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF]. Note that Vampire's higher-order schedule is optimized for running on a single core.

We use the same 2606 monomorphic higher-order TPTP 7.2.0 problems as elsewhere in this paper, but we try to replicate the CASC setup more faithfully. CASC-J10 was run on 8-core CPUs with a 120 s wall-clock limit and a 960 s CPU limit. Since we run the experiments on 4-core CPUs, we set the wall-clock limit to 240 s and keep the same CPU limit. Leo-III, Satallax, and Zipperposition are cooperative provers. We also run them in uncooperative mode, without their backends, to measure their intrinsic strength. Figure 8 summarizes the results.

Among the cooperative provers, Zipperposition is the one that depends the least on its backend, and its uncooperative mode is only one problem behind Satallax's cooperative mode. This confirms our hypothesis that λ-superposition is a suitable basis for automatic higher-order reasoning. This also suggests that the implementation of this calculus in a modern first-order superposition prover such as E or Vampire would achieve markedly better results. Moreover, we believe that there are still techniques inspired by tableaux, SAT solving, and SMT solving that could be adapted and integrated in saturation provers.

Discussion and Conclusion

Back in 1994, Kohlhase [27,Sect. 1.3] was optimistic about the future of higherorder automated reasoning:

The obstacles to proof search intrinsic to higher-order logic may well be compensated by the greater expressive power of higher-order logic and by the existence of shorter proofs. Thus higher-order automated theorem proving will be practically as feasible as first-order theorem proving is now as soon as the technological backlog is made up.

For higher-order superposition, the backlog consisted of designing calculus extensions, heuristics, and algorithms that mitigate its weaknesses. In this paper, we presented such enhancements, justified their design, and evaluated them. We explained how each weak point in the higher-order proving pipeline could be improved, from preprocessing to reasoning about formulas, to delaying unpromising or explosive inferences, to invoking a backend. Our evaluation indicates that higher-order superposition is now the state of the art in higher-order reasoning.

Higher-order extensions of first-order superposition have been considered by Bentkamp et al. [START_REF] Bentkamp | Superposition with lambdas[END_REF][START_REF] Bentkamp | Superposition for lambda-free higher-order logic[END_REF] and Bhayat and Reger [START_REF] Bhayat | Restricted combinatory unification[END_REF][START_REF] Bhayat | A combinator-based superposition calculus for higher-order logic[END_REF]. They introduced proof calculi, proved them refutationally complete, and suggested optional rules, but they hardly discussed the practical aspects of higher-order superposition. Extensions of SMT are discussed by Barbosa et al. [START_REF] Barbosa | Extending SMT solvers to higher-order logic[END_REF]. Bachmair and Ganzinger [START_REF] Bachmair | Non-clausal resolution and superposition with selection and redundancy criteria[END_REF], Manna and Waldinger [START_REF] Manna | A deductive approach to program synthesis[END_REF], and Murray [START_REF] Murray | Completely non-clausal theorem proving[END_REF] have studied nonclausal resolution calculi.

In contrast, there is a vast literature on practical aspects of first-order reasoning using superposition and related calculi. The literature evaluates various procedures and techniques [START_REF] Hoder | Comparing unification algorithms in first-order theorem proving[END_REF][START_REF] Reger | Playing with AVATAR[END_REF], literal and term order selection functions [START_REF] Hoder | Selecting the selection[END_REF], and clause evaluation functions [START_REF] Gleiss | Layered clause selection for theory reasoning (short paper)[END_REF][START_REF] Schulz | Performance of clause selection heuristics for saturationbased theorem proving[END_REF], among others. Our work joins the select club of papers devoted to practical aspects of higher-order reasoning [START_REF] Benzmüller | Can a higher-order and a firstorder theorem prover cooperate?[END_REF][START_REF] Färber | Internal guidance for Satallax[END_REF][START_REF] Steen | There is no best β-normalization strategy for higherorder reasoners[END_REF][START_REF] Wisniewski | Effective normalization techniques for HOL[END_REF].

As a next step, we plan to implement the described techniques in Ehoh [START_REF] Vukmirović | Extending a brainiac prover to lambda-free higher-order logic[END_REF], the λ-free higher-order extension of E. We expect the resulting prover to be substantially more efficient than Zipperposition. Moreover, we want to investigate the proofs found by provers such as CVC4 and Satallax but missed by Zipperposition. Finding the reason behind why Zipperposition fails to prove specific problems will likely result in useful new techniques.

Fig. 5 :Fig. 6 :Fig. 7 :

 567 Fig. 5: Effect of the backend invocation point K time

  , Bentkamp et al. described an older version of this extension. Here we present a newer version in more detail, including heuristics to postpone unpromising streams. The pseudocode of the modified procedure is as follows: function ExtractClause(Q, stream) maybe clause ← pop and compute the first element of stream if stream is not empty then add stream to Q with an increased weight return maybe clause |Q|) if Q and collected clauses are empty then status ← Satisfiable else status ← Unknown return (status, collected clauses)

	else
	A ← A ∪ {given}
	for stream in streams of inferences between given and other ∈ A do
	if stream is not empty then P ← P ∪ExtractClause(Q, stream)
	i ← i + 1
	if i mod K fair = 0 then P ← P ∪ FairProbe(Q, i/K fair )
	else P ← P ∪ HeuristicProbe(Q)
	else
	(status, forced clauses) ← ForceProbe(Q)
	P ← P ∪ forced clauses
	return status
	function GivenClause(P , A, Q)
	(status, i ) ← (Unknown, 0)
	while status = Unknown do
	if P is not empty then
	given ← pop a chosen clause from P and simplify it
	if given is the empty clause then status ← Unsatisfiable

function HeuristicProbe(Q) (collected clauses, i ) ← (∅, 0) while i < K best and Q is not empty do (maybe clause, j ) ← (∅, 0) while j < K retry and Q is not empty and maybe clause = ∅ do stream ← pop the lowest weight stream in

Q maybe clause ← ExtractClause(Q, stream) j ← j + 1 collected clauses ← collected clauses ∪ maybe clause i ← i +

1 return collected clauses function FairProbe(Q, num oldest) collected clauses ← ∅ oldest streams ← pop num oldest oldest streams from Q for stream in oldest streams do collected clauses ← collected clauses ∪ ExtractClause(Q, stream) return collected clauses function ForceProbe(Q) collected clauses ← ∅ while Q is not empty and collected clauses = ∅ do collected clauses ← FairProbe(Q,

  Effect of the FluidSup weight increment K incr on performance functions PHOS and BNF, which require inspecting the proof of clauses, hardly help. Simple functions such as PL are more effective: Compared with base, PL loses one problem overall but proves 22 new problems.

	base (CP) BAVN	PL		PSAV PHOS BNF PDAV
	1638	1640 1637 1637 1632 1594 1520
	Fig. 3: Effect of the priority function on performance
	base (∞)	16	8	4	2	1
	1638	1619 1621 1618 1612 1610
	Fig. 4:

https://doi.org/10.5281/zenodo.4534829

Acknowledgment. We are grateful to the maintainers of StarExec for letting us use their service. Ahmed Bhayat and Giles Reger guided us through details of Vampire 4.5. Ahmed Bhayat, Michael Färber, Mathias Fleury, Predrag Janičić, Mark Summerfield, and the anonymous reviewers suggested content, textual, and typesetting improvements. We thank them all.

Vukmirović, Bentkamp, and Blanchette's research has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Blanchette and Nummelin's research has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward) and the Incidental Financial Support scheme.


C Fonteneau

J Motsch

M Babel

O Déforges

A Hierarchical Selective Encryption Technique in a Scalable Image Codec

Modern still image codecs furnish more than just good distortion-rate performances. They must also provide some services. Scalability in resolution and quality, error resilience and embedded bitstreams were among the first one to be available. There is still room for enhancement, especially when it comes to security-oriented features. Image encryption is one of the aspect of image security. This paper presents the embedding of an encryption service in a multiresolution lossless codec. Partial encryption is performed using ciphering only the keystone part of the codec algorithm, a quadtree decomposition. This results in a hierarchical encryption scheme, showing to be a good tradeoff between encryption speed, selective access and robustness.

Selective image encryption

Nowadays, huge amount of digital visual data are stored on different media and are exchanged over various networks . Often, these visual data contain private, confidential or proprietary informations or are associated with economical interests. As a consequence, techniques especially designed for these data are required so that to provide security functionalities such as privacy, integrity, or authentication. Multimedia security [START_REF] Uhl | Image and Video Encryption[END_REF] is aimed towards these technologies and applications.

Besides watermarking, steganography, and techniques for assessing data integrity and authenticity, providing confidentiality and privacy for visual data is among the most important topics in the area of multimedia security. Applications range from digital rights management to secured personal communications.

Contrary to classical encryption [START_REF] Schneier | Applied Cryptography[END_REF], security may not be the most important aim for an encryption system for images. Depending on the type of applications, other properties (such as speed or bitstream compliance after encryption) might be equally important as well. In that context, naive or hard encryption consists in putting in the whole image data bitstream into a standard encryption system, without taking care of its nature. However, considering the typical size of a digital image compared to that of a text message, the naive algorithm usually cannot meet the speed requirements for real-time digital image processing or transmission applications. In contrast, soft or selective encryption trades off security for computational complexity. They are designed to protect multimedia content and fulfil the security requirements for a particular multimedia application. Research is focused on fast encryption procedures specifically tailored to the target environment.

There are two levels of security for digital image encryption: low level and high-level security encryption. In low-level security encryption, the encrypted image1 has degraded visual quality compared to that of the original one, but the content of the image is still visible and understandable to the viewers. In the high-level security case, the content is completely scrambled and the image just looks like random noise. In this case, the image is not understandable to the viewers at all.

Selective encryption [START_REF] Van Droogenbroeck | Techniques for a selective encryption of uncompressed and compressed images[END_REF]aims at avoiding the en-cryption of all bits of a digital image and yet ensuring a secure encryption. The key point is to encrypt only a small part of the bitstream to obtain a fast method. The canonical framework for selective encryption is presented on figure 1a. The image is first compressed. Afterwards, the algorithm only encrypts part of the bitstream with a well-proven ciphering technique: incidentally, a message (a watermark) can be added at this step. To ensure full compliance with any decoder, the bitstream should only be altered at carefully chosen places. With the decryption key, the receiver decrypts the bitstream and decompresses the image. When the decryption key is unknown, the receiver will still be able to decompress the image, but this image will significantly differs from the original, as depicted in figure 1b. Methods for selective encryption [START_REF] Yang | Data, image and video encryption[END_REF] proposed recently include DCT-based methods, Fourier-based methods, SCAN-based methods, chaos-based methods and quadtree-based methods. These methods have to be fast to meet the applications requirements and try to keep the compression ratio as good as without encryption.

In this paper, we introduce a hierarchical encryption technique using the compressed bitstream produced by a scalable lossless codec. It allows selective access management and low level security. Encryption is fast and provide a good trade-off between security, visual quality and distortion. Section 2 introduces the technique while section 3 shows experimental results. Finally, section 4 presents briefly future work.

Selective encryption of LARcompressed images

The LAR codec is a multipurpose coding solution for still images. It provides scalability both in resolution and quality, embedded bitstream from lossy to lossless coding, with computational low complexity, using grayscale and color imaging with stateof-the-art distortion-rate performances. This codec adapts resolution to the local activity of the image. Low resolutions correspond to smooth areas, and high resolutions correspond to high frequency areas (edges). That adaptation is described by a blockbased quadtree partition, with block size from 2x2 to 64x64 pixels. A hierarchical decomposition framework allows scalability in quality and resolution, as depicted in figure 2a, where a conditional pyramid is used.

From a selective encryption point of view, the emphasis will be put on the description of the LAR bitstream. This bitstream embodies 3 interleaved components:

• The quadtree partition bitstream. A binary information is required at the decoder in order to construct the quadtree partition. This data is progressively sent level by level. Figure 2b illustrates that progressive coding.

• The flat LAR bitstream used to reconstruct an image of variable-size blocks. This bitstream is constructed during a first descent of the pyramid, conditioned by the quadtree partitioning.

• The texture bitstream that encodes the remaining details. This bitstream is built during a sec-ond descend of the pyramid, conditioned by the quadtree partition of remaining undecomposed blocks and the flat bitstream. As the conditional pyramid relies on a quadtree partition, this partition needs to be transmitted without error. Previous work on error resilience dealt with that aspectand showed that the decoder was still able to decode erroneous bitstream. In that case, visual quality was very low, even when few bits of the quadtree were wrongly transmitted. Further work introduced a zero cost security mechanism, relying on the size of the quadtree partition search space.

Following that path, we propose to selectively en-crypt different levels of the quadtree partition description, as depicted on figure 1c. One typical usecase of that scheme is selective access to an image database. This hierarchical selective encryption technique has the following properties:

• Encryption is performed on a level basis. Different keys are used to encrypt each level of the quadtree partition, and one or several levels can be encrypted. This allows a fine management of the visual information revealed to the decoder.

• Encryption and decryption are performed using a classical cryptosystem, symmetric or asymmetric depending on the target application requirements, in speed or security. It allows for flexibility and standard compliance.

• Encryption can be performed offline on the compressed bitstream or online, during compression.

• Encryption is performed on a small part of the bitstram, especially when images are losslessly coded.

Experimental results

The selective encryption scheme has been applied to natural images, using the Advanced Encryption Standard (AES [START_REF] Daemen | The desing of Rijndael AES -The Advanced Encryption Standard[END_REF]) cryptosystem, with a key length of 256 bits, in ECB (Electronic CodeBook) mode. This system is a 128-bits block cipher adopted as a standard. It has been analyzed extensively and is now widely used worldwide as was the case with its predecesoor, the Data Encryption Standard (DES). AES is one of the most popular algorithms used in symmetric key cryptography. This part of the scheme furnished basic cryptographic security. The following results show the ability of our hierarchical selective encryption scheme. Figure 3 shows an example of encryption, where the smallest block decomposition is encrypted. When small blocks are modified by the selective encryption, it appears that the overall quality is still acceptable. Nevertheless, the encrypted picture is of no use, as for printing. From a distortion point of view, it appears that encrypting higher level (smaller blocks) increases the PSNR, and at the same time, the encrypting cost. From a security point of view, as the level increases, the search space for a brute force attack increases drastically. In example, the entropy of the quadtree partition for lena at level 1 is 61 bits, resulting in a search space of 2 61 differents partition, while at level 4, the entropy is 8886 bits. Encryption at level 1 is weaker than at level 4, but the obtainable quality after decryption is still bad, making that useless. Encryption at level 4 is stronger, but the visual quality is better. In that case, it is very difficult to break the encryption scheme to obtain the lossless image.

Future work

Our proposal of a hierarchical selective encryption based on LAR codec presents good results in terms of security, speed or any tradeoff between them. Nevertheless, some aspects need to be further investigated. As usual with cryptosystems, the possibility of attacks is to be considered, both on the underlying cryptosystem, as AES, or on the coding side. For that purpose, further work is necessary to evaluate the computing cost of brute force attacks, quantifying the information available to the attacker. Another point is encrypting the LAR flat bitstream instead of the quadtree partition bitstream. Last point is to develop a complete secure framework, from client to image database, with hierarchical key management.

  LAR hierarchical selective encryption

Figure 1 :

 1 Figure 1: Selective encryption frameworks

Figure 2 :

 2 Figure 2: Hierarchical LAR

  Partition (c) Encr. Part. (d) Encr. Image

Figure 3 :

 3 Figure 3: Selective encryption on lena at level 3.

Figure 4 :Figure 5 :Figure 5

 455 Figure 4: Selective encryption on lena at decreasing levels

the image decrypted without the decryption key