Narjes Berregeb

Riadh Robbana
email: narjes.robbana@insat.rnu.tn

Ashish Tiwari
email: tiwari@csl.sri.com

Towards automated proofs of observational properties

Keywords: observational, contexts, rewriting

Observational theories are a generalization of first-order theories where two objects are observationally equal if they cannot be distinguished by experiments with observable results. Such experiments, called contexts, are usually infinite. Therefore, we consider a special finite set of contexts, called cover-contexts, "covering" all the observable contexts. Then, we show that to prove that two objects are observationally equal, it is sufficient to prove that they are equal (in the classical sense) under these cover-contexts. We give methods based on rewriting techniques, for constructing such cover-contexts for interesting classes of observational specifications.

Introduction

A fundamental aim of formal specifications is to provide a rigorous basis to establish software correctness. Intuitively, a program is correct w.r.t its initial specification if it satisfies all the properties required by this specification. Behavioural abstraction provides a suitable basis for a more adequate notion of correctness. In a behavioural or observational theory, two objects are viewed as being identical if they cannot be ditinguished by observable experiments. Thus, for proving the correctness of a program, behavioural (or observational) concepts allow to abstract away from internal implementation details, and to focus only on its observable behaviour.

For instance, in the field of object-oriented programming, an observable experiment consists of an application of a method that returns certain visible attributes of that object. The actual implementation of the object is not crucial as long as the visible attributes returned by certain methods (and the iterative application of these methods) satisfy the program specification. When formalized using algebraic specifications, method names map to a sorted signature and the observable experiments map to contexts (terms over the signature with a "hole" for the invisible object) with visible sorts.

The idea that the semantics of a specification must describe the behaviour of an abstract datatype is due to [START_REF] Guttag | The specification and application to programming of abstract data types[END_REF]. A lot of work has been devoted to the semantical aspects of observability and provability 1365-8050 c 2004 Discrete Mathematics and Theoretical Computer Science (DMTCS), Nancy, France of observational equivalence, see for example [BBK94, Rei95, JR97, HB99, GM99]. In the framework of algebraic specifications, experiments with observable results are represented by particular terms called observable contexts. The main difficulty when dealing with proofs of observational properties is that the number of observable contexts is often infinite, and it had been shown in [START_REF] Schoett | Two impossibly theorems on behavioural specifications[END_REF] that there is no finite axiomatization of the behavioural equality in first-order logic.

In the framework of initial algebras, an algorithm was given in [START_REF] Berregeb | Observational proofs with critical contexts[END_REF] for constructing a finite set of contexts, that allows to describe the whole set of observable contexts. It applies to specifications represented by a left-linear system. We consider this construction in a more general framework (the semantic we use is not limited to only initial algebra), give more intuitions about it, and show that it can be used by any first order theorem prover for proving observational properties. We call the contexts obtained cover-contexts. Then, to prove that two terms are observationally equal, it is sufficient to prove that they are equal (in the classical sense) under these cover-contexts. We also show that the algorithm applies to an interesting class of non left-linear (equational) specifications with observable sorts. Finally, we consider the general case of non left-linear rewriting systems, we propose a procedure which outputs a cover-context set when it terminates.

Related work

Hennicker [START_REF] Hennicker | Context induction: a proof principle for behavioural abstractions and algebraic implementations[END_REF] has proposed an induction principle, called context induction, which is a proof principle for behavioural abstractions. A context c is viewed as a particular term containing exactly one variable; therefore, the subterm ordering defines a Noetherian relation on the set of observable contexts. Consequently, the principle of structural induction induces a proof principle for properties of contexts of observable sort, which is called context induction. This approach provides a uniform proof method for the verification of behavioural properties. It has been implemented in the system ISAR [START_REF] Bauer | Proving the correctness of algebraic implementations by the isar system[END_REF]. However in concrete examples, this verification is a non trivial task and requires human guidance: the system often needs a generalization of the current induction assertion before each nested context induction, so as to achieve the proof.

Malcolm and Goguen [START_REF] Goguen | A hidden agenda[END_REF] suggested doing coinduction proofs by first defining a relation, showing it is a behavioural or hidden congruence, and then showing behavioural equivalence of two terms by showing that they are congruent. This technique, which they call "hidden coinduction," is easily automated only in certain cases where the specification satisfies additional strong restrictions. Note that checking if a relation is a hidden congruence involves establishing observational equivalence. Moreover, if the candidate relation is not a hidden congruence, then users have to find another candidate to complete the proof. The same problems appear in the approach of Bidoit and Hennicker [START_REF] Bidoit | Behavioural theories and the proof of behavioural properties[END_REF] where users have to provide partial congruences.

Several other proof tools have been developed to aid coinductive proofs, but all of them require the user to supply an appropriate relation which the system can then prove to be a bisimulation. In the work of [START_REF] Dennis | Using a generalisation critic to find bisimultations for coinductive proofs[END_REF], an automatic method is given to construct a bisimulation relation, however it uses heuristics and can fail on some examples.

In [START_REF] Matsumoto | Test set coinduction: Toward automated verification of behavioural properties[END_REF], an algorithm is proposed to generate the contextual equality, which coincides with the behavioural equivalence, by eliminating the redundant observational contexts using rewriting techniques. However, this algorithm applies to specifications with only one hidden sort.

Basic notions

We assume that the reader is familiar with the basic concepts of algebraic specifications [START_REF] Wirsing | Algebraic specifications[END_REF], term rewriting and equational reasoning. A many sorted signature Σ is a pair (S, F) where S is a set of sorts and F is a set of function symbols. We assume a partition of F into two subsets C and D of constructors symbols and defined function symbols. Let X be a family of sorted variables and let T (F, X) be the set of sorted terms. Let var(t) denote the set of variables appearing in t. A term is linear if all its variables occur only once. If var(t) is empty then t is a ground term. The set of all ground terms is also denoted by T (F). A term in T (C, X) is called a constructor term. Let A be an arbitrary non empty set, and let

F A = { f A | f ∈ F} such that if f is of arity n, then f A is a function from A n to A. The pair (A, F A ) is called a Σ-
algebra, and A is the carrier of the algebra. For sake of simplicity, we will write A to denote the Σ-algebra when F and F A are non ambiguous. A substitution η assigns terms of appropriate sorts to variables. The domain of η is denoted by dom(η). If t is a term, then tη denotes the application of η to t. If η replaces every variable by a ground term, then η is a ground substitution. We denote by ≡ the syntactic equivalence between objects.

Let N * be the set of finite sequences of positive integers. For any term t, Pos(t) ⊆ N * denotes the set of positions of t, and the expression t/u denotes the subterm of t at position u. The root position is denoted by ε. The depth of a position u, denoted by |u|, is the length of the corresponding sequence. We denote by t(u) the symbol of t at position u. A position u in a term t is said to be a strict position if t(u) ∈ F. Let u and v two positions, if there exists a position w such that uw=v then u ≺ v. We write t[s] u to indicate that s is a subterm of t at position u. We use also the notation t[s 1 , . . . , s n ] to indicate that the term t contains the subterms s 1 , . . . , s n . The depth of a term t is defined as follows:

|t| = 0 if t is a constant or a variable, otherwise, | f (t 1 , . . . ,t n )| = 1 + max i |t i |.
An equation is a formula of the form l = r. It will be called a rewrite rule and written l → r if interest is in the left to right use of this equation. The term l is the left-hand side of the rule. A rewrite rule l → r is left-linear if l is linear. A rewrite system is a set of rewriting rules. Let t be a term and u a position in t. We write: t → R s if there exists a rule l → r in R and a substitution σ such that t/u = lσ, s/u = rσ and t/v = s/v for any position v such that u ≺ v. A term t is irreducible (or in normal form) if there is no term s such that t → R s. A rewrite system R is said to be terminating if there is no infinite derivation t 1 → R t 2 → R • • • starting from any term t 1 . If ≻ is a reduction ordering † on terms such that l ≻ r for every l → r ∈ R, then R is terminating. A term t is ground reducible if all its ground instances are reducible. A valid property

t 1 = t 2 in R, is denoted by R |= t 1 = t 2 . A theorem t 1 = t 2 of R, is denoted by R ⊢ t 1 = t 2 . An operator f ∈ D is sufficiently complete iff for all t 1 , . . . ,t n ∈ T (C), there exists t ∈ T (C) such that f (t 1 , . . . ,t n ) * → t. A rewriting system R is sufficiently complete if each f ∈ D is sufficiently complete.

Observational Semantics

The notion of observations has been introduced as a means for describing what is observed in a given algebra. Various techniques have been proposed: observations based on sorts, operators, terms or formula (see [START_REF] Bernot | Behavioural approaches to algebraic specifications: a comparative study[END_REF] for a survey). The semantics we choose is based on a relaxing of the satisfaction relation. The notion of context is fundamental in all approaches based on such observational semantics. An observational property is obtained by taking into account only observable information. To show that it is valid, one has to show its validity in all observable contexts. Definition 1 (Context) Let T (F, X) be a term algebra and (S, F) be its signature.

• a context over F is a non ground term c ∈ T (F, X) with one distinguished occurrence of a variable called the contextual variable of c. To indicate the contextual variable z s occurring in c, we often write c[z s ] instead of c, where s is the sort of z s .

• a context reduced to a variable z s of sort s is called an empty context variable of sort s.

• the application of a context c[z s ] to a term t ∈ T (F, X) of sort s, denoted by c[t], is defined by the substitution of z s by t in c[z s

]. In this case, the context c is said to be applicable to t.

• by assumption, var(c) will denote the set of variables occurring in c except the contextual variable of c. A context c is ground if var(c) = / 0. We denote by |c| the depth of c.

• a subcontext (resp. strict subcontext) of c, is a context which is a subterm (resp. strict subterm) of c, having the same contextual variable as c.

Notations Let c[z s ] and c ′ [z ′ s ′
] be contexts such that c ′ is of sort s, let t be a term and σ be a substitution such that z s ∈ dom(σ). We use the following notations:

• c[(c ′ [t])] = (c[c ′ ])[t] = c[c ′ [t]] • (c[t])σ = (cσ)[tσ] = c[t]σ
Definition 2 (Specification, Observable specification) A specification (or equational specification) SP is a triple (S, F, E) where (S, F) is a signature and E is a set of equations. An observational specification SP obs is a couple (SP, S obs ) such that SP = (S, F, E) is a specification and S obs ⊆ S is the set of observable sorts.

In the following we denote by SP obs = (SP, S obs ) an observational specification, where SP = (S, F, E). We denote by R the rewriting system associated with SP. 1 is an observational specification where S obs = {nat}. Definition 3 (Observable context) An observable context is a context whose sort belongs to S obs . The set of observable contexts is denoted by C obs .

Example 1 The Stack specification in Figure

Example 2 Consider the specification in Figure 1, there are infinitely many observable contexts:

• top(z stack ),
• top(pop(z stack )), . . . ,

• top(pop(. . . (pop(z stack )) . . .)), . . . ,

• top(push(i, z stack )),

• top(push(i, pop(z stack ))), . . . . The notion of observational validity is based on the idea that two objects are equal if they cannot be distinguished by observable contexts.

Definition 4 (Observational validity) Let t 1 ,t 2 be two terms. We say that t 1 = t 2 is observationally valid, and denote it by

E |= obs t 1 = t 2 , iff for all ground c obs ∈ C obs , E |= c obs [t 1 ] = c obs [t 2 ].
We say that t 1 and t 2 are observationally equal and denote it by t

1 = obs t 2 , iff E |= obs t 1 = t 2 . Note that if E |= t 1 = t 2 then E |= obs t 1 = t 2 ,
but the converse may not be true. Observational theories generalize first-order theories: if S obs = S then the satisfaction relation |= obs is equal to |=.

Example 3 Consider the Stack specification in Figure 1. It is easy to see that push(top(s), pop(s)) = s is not satisfied (in the classical sense), because push(top(Nil), pop(Nil)) = Nil is not valid. However, it is observationally satisfied if we just observe the elements of the sequences push(top(s), pop(s)) and s.

This can be formally shown by considering all observable ground contexts.

Cover-contexts

The main problem of proving observational properties is that the number of observable ground contexts is often infinite. We introduce in this section the notion of cover-contexts which allow to describe finitely the often infinite set of observable ground contexts.

Definition 5 (Cover-tree) A cover-tree T s is a tree such that:

• The root is a contextual variable z s with s ∈ S obs

• The successors of a node which is a non observable context c[z s ] of sort s i , are all the contexts of the form f (x 1 , . . . , x i-1 , c, x i+1 , . . . , x n ), where:

-f ∈ F, f : s 1 × . . . × s i-1 × s i × s i+1 × . . . × s n → s ′ -c is of sort s i , (s i ∈ S obs ).
-

Fig. 2: A cover-tree for the stack specification

Example 4 A cover-tree T stack for the stack specification is given in Figure 2.

Note that such cover-tree is often infinite. Each node is a context embedding its predecessor contexts in the same branch, and each leaf is an observable context. An interesting point is that, for proving that a = obs b where a and b have a sort s ∈ S obs , it is sufficient to consider a finite set of contexts {c 1 , c 2 , . . . , c n } such that at least one context c i occurs in each path starting from the root z s . In fact, if we have c i [a] = c i [b] for each c i , 1 ≤ i ≤ n, then we can deduce c obs [a] = c obs [b] for each observable context c obs , since by construction of T s , the contexts c i (1 ≤ i ≤ n) are subcontexts of all possible observable contexts. For example, if t 1 and t 2 are terms of sort stack, we can show if t 1 = obs t 2 by considering only the set of contexts {top(z stack ), pop(z stack ), push(x, z stack )}. We can also consider the set {top(z stack ),top(pop(z stack )), pop(pop(z stack )), push(x, pop(z stack )), push(x, z stack )}. Note that there usually are infinitely many possibilities for choosing a set of contexts like {c 1 , c 2 , . . . , c n }. An interesting refinement is to consider in T s , not the whole set of contexts c[z s ], but only contexts that can be embedded in an observable ground irreducible context. We call such contexts cover-contexts. In other terms, instead of reasoning on the set of all observable contexts, we consider just an equivalent subset which is the set of ground observable and irreducible contexts.

Definition 6 (Quasi ground reducibility) A context c is quasi ground reducible if for all ground substitutions τ such that dom(τ) = var(c), cτ is reducible.

Example 5 The context top(push(x, z stack )) is quasi ground reducible. But the context top(z stack ) is not quasi ground reducible.

Definition 7 (Cover-context set) A cover-context set is a finite set of contexts CC

= {c 1 , c 2 , . . . , c n } such that:
i/ for each c i ∈ CC, there exists an observable context c obs such that c obs [c i ] is not quasi ground reducible.

ii/ for each ground irreducible observable context c obs , there exists c i ∈ CC, c ′ obs ∈ C obs and a ground substitution τ, such that c obs = c ′ obs [c i ]τ.

Property i expresses the minimality of CC: only contexts that can be embedded in an observable ground irreducible context are retained. Property ii expresses the completeness of CC: each ground observable context is "covered", in some sense, by a context c of CC.

The following lemma shows that cover-contexts are sufficient for proving an observational property in first-order logic.

Lemma 1 Let R be a terminating rewriting system such that var(r) ⊆ var(l) for each rule l → r in R, and let S obs denotes the observable sorts.

Then, R

|= obs t 1 = t 2 if R |= c[t 1 ] = c[t 2
] for all c ∈ CC.

Proof:

Let c obs be an observable ground context. If c obs is irreducible, then there exists a context c ∈ CC, a context c ′ obs ∈ C obs and a ground substitution τ such that c obs = c ′ obs [c]τ (by second property of a covercontext set). We have

R |= c[t 1 ] = c[t 2 ] (by hypothesis), and therefore, R |= (c ′ obs [c]τ)[t 1 ] = (c ′ obs [c]τ)[t 2 ]. Thus, R |= c obs [t 1 ] = c obs [t 2 ].
If c obs is reducible, then there exists an irreducible term t such that R |= c obs [z] = t (since R is terminating). There are three cases here:

(i) If the variable z does not occur in t, then clearly R |= c obs [t 1 ] = t and R |= c obs [t 2 ] = t, and hence R |= c obs [t 1 ] = c obs [t 2 ].
(ii) If the variable z occurs exactly once in t, then t = c ′ obs [z], where c ′ obs is an observable irreducible ground context. In this case, the argument given above shows that

R |= c ′ obs [t 1 ] = c ′ obs [t 2 ], and hence R |= c obs [t 1 ] = c obs [t 2 ].
(iii) Finally, if the variable z occurs more than once in t, then we consider the context t 1 obtained by replacing all but one occurrences of z by t 1 . Then we have:

c obs [t 1 ] → * R t 1 [t 1 ].
If t 1 is reducible, we normalize it by R to t ′ and if z occurs more than once in t ′ , we consider the term t 2 obtained by replacing all but one occurrences of z by t 1 . We repeat the process. If this process does not terminate, then we have an infinite derivation c obs [

t 1 ] → * R t 1 [t 1 ] → * R t 2 [t 1 ] → * R • • •
, which is impossible since R is terminating. Therefore, the above process terminates with an irreducible term u which contains at most one occurrence of z. Thus, this reduces to either case i or case ii above.

✷ 6 Computation of cover-context sets for left-linear systems

Let us first introduce some useful definitions. We define sdepth(R) as the maximal depth of strict positions in left-hand sides of R. We define depth(R) as the maximal depth of positions in left-hand sides of R.

The idea of the computation is the following: for all non observable sorts s, we construct a cover-tree T s of depth equal to sdepth(R). Then we consider the set L of all the leaves of all T s . Starting from the non quasi ground reducible observable contexts of L, we add all contexts of L that can be embedded in one of those observable contexts, to give a non quasi ground reducible and observable context. The algorithm is given in Figure 3. This computation terminates since the trees T s are finite, for all s ∈ S obs .

Since the depth of the cover-trees T s is sdepth(R), the cover-contexts constructed will have a depth smaller than or equal to sdepth(R). However, we can reduce the number of cover-contexts by considering only subcontexts (for example of depth smaller than or equal to 1) of the constructed cover-contexts. Example 7 illustrates this idea.

The Ground reducibility is decidable for equational rewriting systems [START_REF] Plaisted | Semantic confluence and completion method[END_REF]. The test of ground reducibility relies on a special finite set of terms called test set. A test set is defined as a finite set T S(R) of irreducible terms, such that a term is ground reducible iff all its instances by substitutions in T S(R) are reducible. Several algorithms have been proposed for computing a test set, for left-linear rewrite systems (for example see [START_REF] Jouannaud | Automatic proofs by induction in theories without constructors[END_REF][START_REF] Shmid | Towards an efficient construction of test sets for deciding ground reducibility[END_REF]). For non left-linear systems, the computation is more complex than the left-linear case but applies to any rewrite system (for example see [START_REF] Kapur | On sufficient completeness and related properties of term rewriting systems[END_REF][START_REF] Kounalis | Testing for the ground (co-)reducibility property in term-rewriting systems[END_REF][START_REF] Shmid | Towards an efficient construction of test sets for deciding ground reducibility[END_REF]). The constructed test set verifies some important properties (see [START_REF] Kounalis | Testing for the ground (co-)reducibility property in term-rewriting systems[END_REF]):

1/ (finiteness): T S(R) is a finite set.

2/ (minimality): For any term t in T S(R), there exists a ground substitution τ such that tτ is ground and irreducible.

3/ (completeness): For any ground irreducible term s, there exists a term t in T S(R) and a ground substitution τ such that s = tτ.

4/ (transnormality): Every non ground term in T S(R) has an infinite number of ground irreducible instances.

5/ (coverage): Any non ground term t in T S(R) is of depth equal or greater than depth(R).

In the case of a left-linear rewrite system, only conditions 1, 2, 3 and 5 are necessary, besides condition 5 is simplified as follows: Any non ground term t in T S(R) is of depth equal to sdepth(R).

Test substitutions allow to instantiate variables of a context c (or a term t) by elements of the test set whose variables are renamed in order to check the existence of a ground irreducible instance of the context c (or the term t).

Definition 8 (Test substitution) A test substitution for a context c (resp. a term t) is a substitution that instantiates all the variables in var(c) (resp. the variables in var(t)) by terms taken from the test set (whose variables have been renamed).

Test sets are used to test ground reduciblity, this property can be expressed as follows: Let t be a term and σ be a test substitution such that tσ is irreducible, then there exists a ground substitution ρ such that tσρ is ground and irreducible. The proof of this property in the left-linear case is based on the fact that for all variable x in t, |xσ| = sdepth(R), so, no subterm of tσρ can match a left-hand-side of a rule in R. In the non left-linear case, the proof uses the transnormality property to build an irreducible instance ρ such that tσρ is ground and irreducible (see for example [START_REF] Kounalis | Testing for the ground (co-)reducibility property in term-rewriting systems[END_REF]).

The Quasi ground reducibility is decidable for equational rewriting systems [START_REF] Kaplan | On the decidability of quasi-reducibility[END_REF]. To test whether a context c[z s ] is quasi ground reducible, we apply all test substitutions to c[z s ] and show that they are reducible.

Lemma 2 A context c[z s ] is quasi ground reducible iff for all test substitutions σ such that dom(σ) = var(c), c[z s ]σ is reducible.

for each non observable sort s, construct a cover-tree T s of depth sdepth(R). let LV be the set of leaves of all cover-trees T s .

L := S c∈LV expand(c) where expand(c) is c if c is observable, otherwise expand(c) is obtained from c by instantiating its variables (except the contextual variable) in all possible ways by terms, such that the new obtained contexts have all their variables at the same depth sdepth(R).

CC 0 := {c ∈ L|c is observable and not quasi ground reducible} ∪ {z s | s is observable} L 0 := {c ∈ L|c is not observable}

repeat CC i+1 := CC i ∪ {c ∈ L i |∃c i ∈ CC i such that c i [c] is not quasi ground reducible} L i+1 := L i \CC i+1 until CC i+1 = CC i output CC i

Fig. 3: Computation of cover-contexts for a left-linear system

Proof: ⇐

Suppose for all test substitutions σ, c[z s ]σ is reducible. By property of test sets, we deduce that for all ground substitutions τ such that for all x ∈ var(c), xτ is ground and irreducible: there exists a ground substitution ρ such that for all x ∈ var(c), xσρ is ground and irreducible. Then, c[z s ]σρ is reducible. Thus, for all ground substitutions τ such that dom(τ) = var(c), c[z s ]τ is reducible.

⇒

Suppose that there exists a test substitution σ such that c[z s ]σ is irreducible. We have to show that we can build a ground substitution ρ such that ∀x ∈ var(c), xσρ is ground and irreducible, and c[z s ]σρ is irreducible, and Thus, c[z s ] is not quasi ground reducible. The proof uses the same arguments than for showing that test sets allow to test for ground reducibility. Let us detail the linear case:

From condition 2/ of test sets, there exists a ground substitution ρ such that σρ is ground and irreducible. Suppose that c[z s ]σρ is reducible. Then there exists a strict position u, a rule g → d and a substitution θ such that c[z s ]σρ/u = gθ. Note that the position u necessarily occurs in c[z s ] since σρ is irreducible. Since g is linear and for all x in c[z s ] |xσ| = sdepth(R), we can build a substitution α such that for all variable x occuring at a position

v of g, xα = c[z s ]σ/uv. Then, c[z s ]σ/u = gα.
Thus, c[z s ]σ is reducible, contradiction.

✷

Theorem 1 Let R be a left-linear rewriting system. Then, the set of contexts CC output by the computation described in Figure 3 is a cover-context set.

Proof:

We have to show that CC is a cover-context set w.r.t Definition 7 i/ Let c ∈ CC. Then there exists i such that c ∈ CC i . Let us show that there exists an observable context c obs such that c obs [c] is not quasi ground reducible. The proof is by induction on i: i = 0: in this case c ∈ CC 0 . We set c obs = z s where s is the sort of c. i > 0: there exists c i-1

∈ CC i-1 such that c i-1 [c] is not quasi ground reducible. If c i-1 ∈ C obs , then we set c obs = c i-1 . Otherwise, |c i-1 | = sdepth(R)
. By induction hypothesis, there exists an observable context c obs such that c obs

[c i-1 ] is not quasi ground reducible. Let us show that c obs [c i-1 [c]] is not quasi ground reducible.
obs [c i-1 ] is not quasi ground reducible, therefore, there exists a test substitution σ such that dom(σ) = var(c obs [c i-1 ]) and (c obs [c i-1 ])σ is irreducible (by Lemma 2). Let σ 1 be the restriction of σ to var(c obs ), then (c obs σ 1 )[c i-1 ] is still irreducible. c i-1 [c] is not quasi ground reducible, therefore, there exists a test substitution σ 2 such that dom(σ 2 ) = var(c i-1 ) ∪ var(c) and c i-1 [c]σ 2 is irreducible (by Lemma 2). Let us show that c obs [c i-1 [c]]σ 1 σ 2 is irreducible. We can then deduce, by property of test sets, a ground substitution τ such that c obs [c i-1 [c]]σ 1 σ 2 τ is ground and irreducible. Suppose that c obs [c i-1 [c]]σ 1 σ 2 is reducible, then there exists a rule g → d, a substitution θ and a po-

sition u such that c obs [c i-1 [c]]σ 1 σ 2 /u = gθ. The position u cannot occur in c i-1 , otherwise c i-1 [c]
σ 2 would be reducible. Then, necessarily, u occurs in c obs . Since g is linear, we can build a substitution α such that for each variable x appearing at a position w of g, xα = (c obs σ 1 )[c i-1 ]/uw. Then (c obs σ 1 )[c i-1 ]/u = gα, which contradicts the fact that (c obs σ 1 )[c i-1 ] is irreducible ii/ Suppose that there exists an observable ground irreducible context c o such that there does not exist c ∈ CC and a ground substitution τ such that cτ is a subcontext of c o . Let us first define the top of a term t as follows:

• top(t, d) = t, if |t| ≤ d • top( f (t 1 , . . . ,t n ), 0) = f (x 1 , . . . , x n ), where x i (i ∈ [1.
.n]) are fresh variables.

• top( f (t 1 , . . . ,t n ), d) = f (top(t 1 , d -1), . . . ,top(t n , d - 1
′ ∈ CC, τ ′ , c ′′ obs such that c ′ obs = c ′′ obs [c ′ ]τ ′ . In this case, c ′ ∈ CC since c ′ [c]
is not quasi ground reducible, contradiction.

✷

Example 6 Consider the specification in Figure 1. We have: sdepth(R) = 1. A test set for R is:

{0, s(x), Nil, push(x, y)}.
Applying the computation principle described in Figure 3, we get:

CC 0 = {z nat ,top(z stack )} L 0 = {pop(z stack ), push(i, z stack )}
In the next iteration, we add the context pop(z stack ) since top(pop(z stack )) is ground and irreducible.

CC 1 = {z nat ,top(z stack )} ∪ {pop(z stack )} L 1 = {push(i, z stack )} CC 2 = CC 1 is a cover-context set for R. Definition 9 Let f ∈ D. We say that f is strongly complete if f (t 1 , . . . ,t ) * → t and t ∈ T (C, X), for all t i (i ∈ [1..n]) ∈ (T (C, X) \ X). A rewriting system R is strongly complete if for all f ∈ D, f is strongly complete.
Note that: if f is strongly complete, then f is sufficiently complete. The converse may not be true. The following theorem states that we can compute a cover-context based on the algorithm given in Figure 3, for a non left-linear rewriting systems provided that it is strongly complete and that the relations between defined functions are left-linear.

Theorem 2 Let R be a rewriting system strongly complete, such that relations between defined functions are left-linear. We also assume that if a constructor cons : s 1 × s 2 . . . s n → s is such that if s is observable then s 1 , s 2 . . . s n are also observable. Then, the set of contexts CC output by the computation described in Figure 3 is a cover-context set.

Proof:

i/ Let c ∈ CC. Then there exists i such that c ∈ CC i . Let us show that there exists an observable context c obs such that c obs [c] is not quasi ground reducible. The proof is by induction on i: i = 0: in this case c ∈ CC 0 . We set c obs = z s where s is the sort of c. i > 0: there exists c i-1

∈ CC i-1 such that c i-1 [c] is not quasi ground reducible. If c i-1 ∈ C obs , then we set c obs = c i-1 . Otherwise, |c i-1 | = sdepth(R)
. By induction hypothesis, there exists an observable context c obs such that c obs [c i-1 ] is not quasi ground reducible. Thanks to the assumptions on constructors, we can choose c obs such that c obs (ε) u ≺ u z then c obs (u) ∈ D. In this case, g is linear since the relations between defined symbols are left-linear. Then, we can build a substitution α such that for each variable x appearing at a position w of g, xα = (c obs σ 1 )[c i-1 ]/uw. Then (c obs σ 1 )[c i-1 ]/uw = gα, which contradicts the fact that (c obs σ 1 )[c i-1 ] is irreducible.

∈ D or c obs (ε) ∈ X. If c obs (ε) ∈ X (empty context), then we have c obs [c i-1 [c]] not
ii/ The proof of the second property of cover-contexts is similar to the case where R is left-linear.

✷ Example 7

Consider an example of a non left-linear rewriting system given in Figure 4. The rewriting system is strongly complete and the relations between defined operators (top and pop) are left-linear. We have sdepth(R) = 2. A test set for R is:

{0, s(0), s(s(x)), Nil, push(0, Nil), push(s(x), Nil), push(0, push(x, y)), push(s(x), push(x, y))} Applying the computation principle described in Figure 3, we get: CC 0 = {z nat ,top(z stack ),top(pop(z stack ))} L 0 = {pop(pop(z stack )), push(0, pop(z stack ), push(s(x), pop(z stack ), push(0, push(x, z)), push(s(y), push(x, z))}

In the next iteration, we add the context pop(pop(z stack )) since top(pop(pop(z stack ))) is ground and irreducible.

CC 1 = {z nat ,top(z stack ),top(pop(z stack ))} ∪ {pop(pop(z stack ))} L 1 = {push(0, pop(z stack ), push(s(x), pop(z stack ), push(0, push(x, z)), push(s(y), push(x, z))} CC 2 = CC 1 is a cover-context set for R. We can refine CC 1 by considering only subcontexts of depth smaller than or equal to 1. This leads to the cover-context set {z nat ,top(z stack ), pop(z stack )}.

Computation of cover-context sets for non left-linear systems

The algorithm for computing a cover-context set for left-linear rewriting systems does not work for the non-linear case. For example, consider the following rewrite system R:

g(g(x)) → x f (g(x), x) → x f (x, g(x)) → x f (x, x) → x f (x, f (x, z)) → x f (g(x), f (x, z)) → x A test set for R is T S(R) = {a, g(a)}. Consider the contexts c 1 = f (x 1 , z), c 2 = f (x 2 , z), c 3 = f (x 3 , z). The context c 1 [c 2 ]
has an irreducible ground instance which is f (a, f (g(a), z)). The context c 2 [c 3 ] has also an irreducible ground instance which is f (a, f (g(a), z)). However, the context

c 1 [c 2 [c 3 ]] = f (x 1 , f (x 2 , f (x 3 , z)))
has not an irreducible ground instance. Therefore, the cover-contexts computation for left-linear systems (see Figure 3), does not hold for non left-linear systems, since it is based on the idea that: if there exists c i ∈ CC i such that c i [c] is a non quasi ground reducible context, then c can be embedded in an observable ground irreducible context. For non left-linear systems, we use a stronger condition; we show that if there exists c i ∈ CC i such that c i [c] has an infinite number of irreducible instances, then c can be embedded in an observable ground irreducible context. We present in this section a procedure for computing a cover-context set for non left-linear rewriting systems, but which can diverge in some cases. Let us first introduce some useful definitions.

for each non observable sort s, construct a cover-tree T s of depth depth(R). let LV be the set of leaves of all cover-trees T s .

L := S c∈LV expand(c) where expand(c) is c if c is observable, otherwise expand(c) is obtained from c by instantiating its variables (except the contextual variable) in all possible ways by terms, such that the new obtained contexts have all their variables at the same depth depth(R).

CC 0 := {c ∈ L | c is observable and not quasi ground reducible} ∪ {z s | s is observable} L 0 := {c ∈ L | c is not observable} repeat for each c ∈ L i do if there exists c i ∈ CC i such that c i [c] is observable and not quasi ground reducible then CC i+1 := CC i ∪ {c} L i+1 := L i \ {c} else if there exists c i ∈ CC i such that c i [c] is quasi infinitary or ground and irreducible then CC i+1 := CC i ∪ {c} L i+1 := L i \ {c} else for each c i ∈ CC i such that c i [c] is not quasi ground reducible
and not quasi infinitary do extend c i [c] by all possible ground substitutions ρ j such that c i [c]ρ j is either ground irreducible or quasi infinitary If c is a quasi infinitary context, then c has an infinite number of irreducible instances, thanks to the test set properties (transnormality).

L i+1 := (L i \ {c}) ∪ (∪ j c i [c]ρ j ) until L i+1 = L i and CC i+1 = CC i output CC = CC i
Example 8 Consider the specification in Figure 4. The context push(x, z s ) is quasi-infinitary since push(s(y), z) is irreducible for all y.

Theorem 3 Let R be a non left-linear rewriting system. Then, if the computation described in Figure 5 terminates, the set of contexts CC output is a cover-context set. -if c obs [c i-1 ]/uu 2 is not ground. Let x be a variable occuring in c obs [c i-1 ]/uu 2 . We have:

|xτ 2 | > |c obs [c i-1 ]τ 1 |.
Therefore: Therefore: c obs [c i-1 ]τ 1 /uu 1 = c obs [c i-1 ]τ 1 /uu 2 , contradiction -if c obs [c i-1 ]/uu 1 is ground and c obs [c i-1 ]/uu 2 is not ground. Let x be a variable occuring in c obs [c i-1 ]/uu 2 . We have

|c obs [c i-1 [c]]τ 1 τ 2 /uu 1 | = |c obs [c i-1 ]τ 1 /uu 1 | < |c obs [c i-1 ]τ 1 τ 2 /uu 2 | = |c obs [c i-1 ]τ 1 τ 2 /uu 1 |, contradiction.
|xτ 2 | > |c obs [c i-1 ]τ 1 | ≥ |c obs [c i-1 ]τ 1 /uu 1 |.
Therefore:

|c obs [c i-1 [c]]τ 1 τ 2 /uu 2 | > |c obs [c i-1 [c]]τ 1 τ 2 /
|c obs [c i-1 [c]]τ 1 τ 2 /uu 1 | > |c obs [c i-1 [c]]τ 1 τ 2 /uu 2 |, contradiction.
The second part of the proof is similar to that of Theorem 1. ✷

Conclusion

We have presented an algorithm for computing a cover-context set which is a finite description of the often infinite set of observable contexts. We have shown that this computation applies to left-linear rewriting systems as well as an interesting class of non left-linear rewriting system, with any number of observable sorts. In the general case of a non left-linear system, we have proposed a procedure for computing a covercontext set. Once a cover-context set is computed, it is possible to use any first order theorem prover to prove observational properties, provided we use the context induction rule given below:

∀c[z s ] ∈ CC, c[t 1 ] = c[t 2 ] t 1 = t 2
where t 1 ,t 2 are terms of non observable sort. s

We plan to extend the computation of cover-context sets for a more general class of conditional specifications, and to use more refined observations based on operators or terms.

Fig. 1 :

 1 Fig. 1: Stack specification

  )) otherwise. Let d be the depth of the position of the contextual variable of c o . Let us choose c o such that d is minimal. Let c obs = top(c o , d). If d ≤ sdepth(R) then c obs ∈ CC, contradiction. Otherwise, let c be a subcontext of c obs of depth sdepth(R), and let c ′ obs be an observable context such that c obs = c ′ obs [c]. Note that c ′ obs [c] is not quasi ground reducible. By hypothesis, c ∈ CC. Let d ′ be the depth of the contextual variable of c ′ obs . We have, d ′ < d, necessarily there exists c

Fig. 4 :

 4 Fig. 4: A non left-linear specificationLet u z be the position of z s in (c obs σ 1 )[c i-1 [z s ]], and u be a position in(c obs σ 1 )[c i-1 [z s ]] such that u ≺ u z . Necessarily, (c obs σ 1 )[c i-1 ](u) ∈ D, otherwise (c obs σ 1 )[c i-1 ] would be reducible since R is strongly complete. Now, let us show that c obs [c i-1 [c]]σ 1 σ 2 is irreducible. We canthen deduce, by property of test sets, a ground substitution τ such that c obs [c i-1 [c]]σ 1 σ 2 τ is ground and irreducible. Suppose that c obs [c i-1 [c]]σ 1 σ 2 is reducible, then there exists a rule g → d, a substitution θ and a position u such that c obs [c i-1 [c]]σ 1 σ 2 /u = gθ. The position u cannot occur in c i-1 , otherwise c i-1 [c]σ 2 would be reducible. Then, necessarily, u occurs in c obs . u ≺ u z , then (c obs σ 1 )[c i-1 ] would be reducible. Contradiction.

Fig. 5 :

 5 Fig. 5: Computation of cover-contexts for a non left-linear system Definition 10 (Quasi infinitary) A context c[z s ] is quasi infinitary iff there exists a test substitution σ such that dom(σ) = var(c), for all x ∈ dom(σ), xσ is not ground, and c[z s ]σ is irreducible.

Proof:

  We have to show that CC is a cover-context set w.r.t Definition 7. Let c ∈ CC. Then there exists i such that c ∈ CC i . Let us show that there exists an observable context c obs such that c obs [c] is not quasi ground reducible. The proof is by induction on i:-if c obs [c i-1 ]/uu 2 is ground, then c obs [c i-1 [c]]τ 1 τ 2 /uu 2 = c obs [c i-1 ]τ 1 /uu 2 .Besides:c obs [c i-1 [c]]τ 1 τ 2 /uu 2 = c obs [c i-1 [c]]τ 1 τ 2 /uu 1 . Therefore c obs [c i-1 ]τ 1 /uu 2 = c obs [c i-1 [c]]τ 1 τ 2 /uu 1 = c obs [c i-1 ]τ 1 /uu 1 , contradiction.

case 2 :

 2 u 1 occurs in c i-1 . u 2 occurs in c i-1 . case 2.1: u 2 ≺ u z and u 1 ≺ u z In this case c obs [c i-1 [c]]τ 1 τ 2 /uu 2 is not ground and c obs [c i-1 [c]]τ 1 τ 2 /uu 1 is ground, contradiction. case 2.2: u 2 ≺ u z and u 1 ≺ u z . Similar to case 1.2 case 2.3: u 2 ≺ u z and u 1 ≺ u z . -if c obs [c i-1 ]/uu 1 is ground and c obs [c i-1 ]/uu 2 is ground. In this case c obs [c i-1 [c]]τ 1 τ 2 /uu 1 = c obs [c i-1 ]τ 1 /uu 1 and c obs [c i-1 [c]]τ 1 τ 2 /uu 2 = c obs [c i-1 ]τ 1 /uu 2 .

  x 1 , . . . , x i-1 , x i+1 , . .. , x n are new variables not occuring in c[z s ].A path from a node n 1 to a node n p is a sequence of contexts (n 1 , n 2 , . . . , n p ) such that each n i is a successor of n i-1 , for 2 ≤ i ≤ p. The depth of T, denoted by depth(T ) is the length of the longest path of T .

	top(pop(z stack ))	pop(pop(z stack ))	push(x, pop(z stack ))
	top(z stack )	pop(z stack )	push(x, z stack )
		z stack

  quasi ground reducible. Otherwise, we have c obs (ε) ∈ D. Let us show then, that c obs [c i-1 [c]] is not quasi ground reducible.c obs [c i-1 ] is not quasi ground reducible, therefore, there exists a test substitution σ 1 such that dom(σ 1 ) = var(c obs ) and(c obs σ 1 )[c i-1 ] is irreducible. c i-1 [c] is not quasi ground reducible, therefore, there exists a test substitution σ 2 such that dom(σ 2 ) = var(c i-1 ) ∪ var(c) and c i-1 [c]σ 2 is irreducible. Consider all subcontexts f (t 1 , . . . ,t k-1 , c ′ [z s ],t k+1 , . . . ,t n ) of c obs [c i-1 ]σ 1 σ 2 ,where t j is a term for all j ∈ {1, . . . , k -1, k + 1, . . . , n}, and c ′ is a context. Since (c obs σ 1 )[c i-1 ] is irreducible and R is strongly complete, then t j ∈ T (C, X). Besides c obs (ε) ∈ D.

	specification: STACK
	sorts: nat, stack
	observable sorts: nat
	constructors:
	0: →nat
	s: nat→ nat
	Nil: → stack
	push: nat × stack → stack
	defined operators
	top: stack → nat
	pop: stack → stack
	axioms:
	push(x,push(x,Nil))=push(x,Nil)
	top(Nil)=0
	top(push(x,y))=x
	pop(Nil)=Nil
	pop(push(x,y))=y

  uu 1 |, contradiction.-if c obs [c i-1 ]/uu 1 is not ground and c obs [c i-1 ]/uu 2 is not ground. Let x be a variable in c obs [c i-1 ]/uu 1 such that|xτ 1 | = max x i ∈c obs [c i-1 ]/uu 1 |x i τ 2 |.Let y be a variable in c obs [c i-1 ]/uu 2 such that|yτ 2 | = max y i ∈c obs [c i-1 ]/uu 2 |y i τ 2 |. Suppose that |xτ 2 | > |yτ 2 | + |c obs [c i-1 ]τ 1 |. Therefore:

† A reduction ordering is a well-founded ordering that is closed under contexts and substitutions.

Acknowledgements

We would like to thank the referees for their valuable comments.

i = 0: in this case c ∈ CC 0 . We set c obs = z s where s is the sort of c. i > 0: there exists c i-1 ∈ CC i-1 such that c i-1 [c] is not quasi ground reducible. If c i-1 ∈ C obs , then we set

. By induction hypothesis, there exists an observable context c obs such that c obs [c i-1 ] is quasi infinitary or ground irreducible. Let us show that c obs

is not quasi ground reducible.

c obs [c i-1 ] is not quasi ground reducible, therefore, there exists a ground substitution τ 1 such that dom(τ 1 ) = var(c obs ) and

is quasi infinitary (the proof of the case where it is ground and irreducible is a subcase), therefore, there exists a ground substitution τ 2 such that dom(τ

reducible, then there exists a rule g → d, a substitution θ and a position u such that c obs [c i-1 [c]]τ 1 τ 2 /u = gθ. The position u cannot occur in c i-1 , otherwise c i-1 [c]τ 2 would be reducible. Then, necessarily, u occurs in c obs .

• If g is linear, we can build a substitution α such that for each variable x appearing at a position w of g, xα

• If g is not linear, suppose there exists two positions u 1 and u 2 corresponding to a variable x in g such that

Let u z be the postion of the contextual variable of c i-1 in c obs [c i-1 ].

case 1: u 1 occurs in c obs τ 1 . u 2 occurs in c i-1 .

case 1.1: u 2 ≺ u z and u 1 ≺ u z . In this case:

case 1.2: u 2 ≺ u z and u 1 ≺ u z . In this case:

case 1.3: u 1 ≺ u z and u 2 ≺ u z .


Josef Pieprzyk

Xian-Mo Zhang

On Cheating Immune Secret Sharing

Keywords: Secret Sharing, Cheating Prevention, Cheating Immune

The paper addresses the cheating prevention in secret sharing. We consider secret sharing with binary shares. The secret also is binary. This model allows us to use results and constructions from the well developed theory of cryptographically strong boolean functions. In particular, we prove that for given secret sharing, the average cheating probability over all cheating vectors and all original vectors, i.e., 1 n • 2 -n ∑ n c=1 ∑ α∈V n ρ c,α , denoted by ρ, satisfies ρ ≥ 1 2 , and the equality holds if and only if ρ c,α satisfies ρ c,α = 1 2 for every cheating vector δ c and every original vector α. In this case the secret sharing is said to be cheating immune. We further establish a relationship between cheating-immune secret sharing and cryptographic criteria of boolean functions. This enables us to construct cheating-immune secret sharing.

Introduction

Since its invention in 1978 by Blakley (Bla79) and Shamir (Sha79), secret sharing has evolved dramatically. Initially, it was designed to facilitate a distributed storage for a secret in an unreliable or insecure environment. Later, however, secret sharing has been incorporated into public key cryptography giving rise to the well-known concept of group or society oriented cryptography (see [START_REF] Desmedt | Society and group oriented cryptography: A new concept[END_REF]). Now secret sharing is one of the basic cryptographic tools with variety of very interesting schemes based on algebraic or geometric structures.

Tompa and Woll (TW88) observed that Shamir secret sharing can be subject to cheating by dishonest participants who, at the recovery stage, may submit invalid shares to the combiner. Clearly, the combiner reconstructs an invalid secret and passes it to currently active participants. The honest participants are left with the invalid secret while the cheaters are able to recover the valid secret from the invalid one. This observation is true for all linear secret sharing. The cheating attack can also be extended for geometrical secret sharing.

Cheating prevention can be considered in the context of conditionally and unconditionally secure secret sharing. We focus our attention on unconditionally secure secret sharing. In this setting, cheating can be thwarted by

• share verification by the combiner -all invalid shares are identified and discarded. The key recovery goes ahead only if there are enough valid shares to recover the valid secret (see (Car95; CSV93; RBO89)),

• discouraging cheaters from sending invalid shares to the combiner -this argument works if the cheater gains no advantage over honest participants. In other words, sending invalid share will result with recovery of an invalid secret which gives no clues to the cheater as to the value of the valid secret. This paper investigates this case of cheater prevention.

We intend to consider a class of secret sharing for which, a cheating participant is no better off than a participant who tries simply to guess a secret. Ideally, the probability of successful cheating should be equal to the probability of guessing the secret by a participant. To make our considerations explicit, we assume that secret and shares are binary. For this case we prove that there is a secret sharing, further in the work called cheating immune, that gives no advantage to a cheater making it, in a sense, immune against cheating. The cheating immunity was considered in (PZ01) and this paper continues this line of the study by investigating the connection between secret sharing and cryptographically strong boolean functions. The work is structured as follows. Section 2 introduces secret sharing in terms of its notions and notations. Section 3 gives necessary background for boolean functions. In Section 4, we describe a model which is further used to characterise cheating in secret sharing. The main results are given in Section 5. Section 6 explores the problem of constructing cheating-immune secret sharing. Section 7 concludes the work.

Background

Secret sharing allows a group of participants P = {P 1 , . . . , P n } to collectively hold a secret K ∈ K , where K is a set of elements from which the secret is drawn. Secret sharing is created by a trusted algorithm called a dealer who for a given secret, generates a collection of shares s i ∈ S, where S is a set of shares.

Note that s i is given to P i , i = 1, . . . , n. The collective ownership of the secret is defined by the access structure of secret sharing. The access structure Γ is a collection of subgroups of P that are authorised to recover the secret.

An authorised group of participants A ∈ Γ is able to reconstruct the secret by invoking a trusted algorithm called combiner. The combiner always returns the valid secret if the group A submits their valid shares. If the group, however, is too small, i.e. A / ∈ Γ, then the algorithm returns a value which is not the valid secret (with an overwhelming probability).

In this work, we describe a secret sharing by a set of distribution rules [START_REF] Stinson | Cryptography: Theory and practice[END_REF], where a distribution rule is a function f : P → S that represents possible distribution of shares to the participants. In other words, secret sharing is a set

F = [ K∈K F K
where F K is a distribution rule corresponding to the secret K. Equivalently, F can be presented in the form of distribution table T . The table has (n + 1) columns -the first one includes secrets and the other n ones list shares assigned to participants (P 1 , . . . , P n ), respectively. Each row of the distribution table specifies the secret for a collection of shares held by P . Note that F K can be seen as a part of the distribution table with rows whose first entry is K. This table is denoted by T K .

Most of practical secret sharing schemes are linear and therefore subject to an attack observed by Tompa and Woll [START_REF] Tompa | How to share a secret with cheaters[END_REF]. The attack permits a dishonest participant who at the pooling stage submits an invalid share, to recover the valid secret from an invalid one returned by the combiner.

Binary Sequences

We consider a mapping f from V n to GF(2) where V n is the vector space of n tuples of elements from GF(2). f is also called a function on V n . The truth table of a mapping f is a sequence defined by ( f (α 0 ), f (α 1 ), . . . , f (α 2 n -1 )), where α 0 = (0, . . . , 0, 0), α 1 = (0, . . . , 0, 1), . . ., α 2 n -1 = (1, . . . , 1, 1). Each α j is said to be the binary representation of integer j, j = 0, 1, . . . , 2 n -1. A function f is said to be balanced if its truth table contains an equal number of zeros and ones.

An affine function f on V n is a function that takes the form of f (x 1 , . . . ,

x n ) = a 1 x 1 ⊕ • • • ⊕ a n x n ⊕ c
, where ⊕ denotes the addition in GF(2), a j , c ∈ GF(2), j = 1, 2, . . . , n. The function f is called a linear function if c = 0. It is easy to verify that any nonzero affine function is balanced. Let , denote the scalar product of two vectors. There precisely exist 2 n linear functions on V n . We can denote all the 2 n linear functions by ϕ 0 , ϕ 1 , . . . , ϕ 2 n -1 , where ϕ j (x) = α j , x .

The Hamming weight of a vector α ∈ V n , denoted by HW (α), is the number of nonzero coordinates of α. The Hamming weight of a function f , denoted by HW ( f ), is the number of nonzero terms in the truth

table of f .
The nonlinearity of a function f on V n , denoted by N f , is the minimal Hamming distance between f and all affine functions on V n , i.e.,

N f = min i=1,2,...,2 n+1 HW ( f ⊕ ψ i )
where ψ 1 , ψ 2 , . . ., ψ 2 n+1 are all the affine functions on V n . High nonlinearity can be used to resist a linear attack. We know that N f ≤ 2 n-1 -2 1 2 n-1 (MS78). Let f be a function on V n . We say that f satisfies the propagation criterion with respect to α if f (x) ⊕ f (x ⊕ α) is a balanced function, where x = (x 1 , . . . , x n ) ∈ V n and α = (a 1 , . . . , a n ) ∈ V n . Furthermore f is said to satisfy the propagation criterion of degree k if it satisfies the propagation criterion with respect to every nonzero vector α whose Hamming weight is not larger than k. (PLL + 91). The propagation properties were employed in selecting the S-boxes used in the cipher, which contributed to the strength of the cipher against various attacks including differential (BS91) and linear (Mat94) attacks. Note that the strict avalanche criterion (SAC) (WT86) is the same as the propagation criterion of degree one.

The concept of correlation immune functions was introduced by Siegenthaler (Sie84). Xiao and Massey gave an equivalent definition (CCCS91; XM88). A function

f on V n is called a k-th order correlation immune function if ∑ x∈V n f (x)(-1) β,x = 0 for all β ∈ V n with 1 ≤ HW (β) ≤ k,
where f (x) and β, x are regarded as real-valued functions. Correlation immune functions are used in the design of runningkey generators in stream ciphers to resist a correlation attack. A balanced kth-order correlation immune function is also called a k-resilient function. Due to Lemma 3 of (ZZ97), we can give a k-resilient function an equivalent definition: a function f is said to be k-resilient if f satisfies the property: for every subset { j 1 , . . . , j k } of {1, . . . , n} and every (a 1 , . . . ,

a k ) ∈ V k , f (x 1 , . . . , x n )| x j 1 =a 1 ,...,x j k =a k is a balanced function on V n-k .
A special class of functions is called bent. There exist equivalent definitions of bent functions (Rot76). For example, a function f on V n is said to be bent if and only if f satisfies the propagation criterion with respect to every nonzero vector in V n . The sum of any bent function on V n and any affine function on V n is bent. Bent functions are not balanced and bent functions on V n exist only when n is even. Furthermore, it is well known that any bent function f on V n achieves the maximum nonlinearity, i.e.,

N f = 2 n-1 -2 1 2 n-1 .

Model of Cheating

Given (n, n) threshold secret sharing defined by its distribution table T . We define a function f : V n → {0, 1} and fix an integer c; 1 ≤ c ≤ n, which points to the position (column) of the cheater P c in T . The vector δ c = (0, . . . , 0, 1, 0, . . . , 0) ∈ V n represents the cheating vector introduced by the cheater. Note that the cheater P c can only change his share on the c-th position (other positions are not changed assuming that other participants are honest). Let ρ c,α be the probability of successful cheating by P c , where α is a row of T indicating the secret and shares currently in use. A precise expression of ρ c,α will be given in next two paragraphs. In the work (PZ01), it was shown that for an arbitrary α, there is a vector α ′ ∈ V n such that either ρ c,α + ρ c,α ′ = 1 or ρ c,α = 1. This implies that the maximum cheating probability is always larger than or equal to 1 2 . Naturally one would expect that (a) max{ρ c,α |α ∈ V n , 1 ≤ c ≤ n} is as small as possible, and (b) ρ = 1 n •2 -n ∑ n c=1 ∑ α∈V n ρ c,α is as small as possible (ideally, the both probabilities are equal to 1

2 ). In this paper we identify conditions for which (a) and (b) hold and as the result we introduce the concept of cheating-immune secret sharing. Furthermore we characterise cheating-immune secret sharing using cryptographic properties of boolean functions. Thus we are able to construct cheating-immune secret sharing that gives no advantage to a cheater over honest participants.

We introduce the following notations:

• α = (s 1 , . . . , s n ) is the sequence of shares held by P and the secret K = f (α),

• α * = (s 1 , . . . , s c-1 , 1 ⊕ s c , s c+1 , . . . , s n ) is the sequence of shares submitted to the combiner where P c modified her share. The sequence δ c = (0, . . . , 0, 1, 0, . . . , 0) contains all zero except the c-th position and represents modification done by the cheater, K * = f (α * ) is the invalid secret returned by combiner,

• Ω * α = {(x 1 , . . . , x c-1 , s c , x c+1 , . . . , x n )| f (x 1 , . . . , x c-1 , 1⊕s c , x c+1 , . . . , x n ) = K * } is the set of all shares
taken from rows of T containing α and K which are consistent with the invalid secret returned by the combiner. The set determines the view of the cheater after getting back K * from the combiner,

• Ω α = {(x 1 , . . . , x c-1 , s c , x c+1 , . . . , x n )| f (x 1 , . . . , x c-1 , s c , x c+1 , . . . , x n ) = K} is the set of rows which contain the current share of P c and the valid secret K.

The function f is called defining function. To prevent cheaters from finding the correct secret (and effectively discourage them from cheating), one would wish to obtain Ω * α as big as possible for any α, while Ω * α ∩ Ω α as small as possible. The nonzero vector δ c = (0, . . . , 0, 1, 0, . . . , 0), where only the c-th coordinate is nonzero, is called the cheating vector. α = (s 1 , . . . , s n ) is called the original vector. The value of ρ c,α = #(Ω * α ∩ Ω α )/#Ω * α , where #X denotes the the number of elements in the set X, expresses the probability of cheater success with respect to α = (s 1 , . . . , s n ). As the original vector α = (s 1 , . . . , s n ) is always in Ω * α ∩ Ω α , the probability of successful cheating is always nonzero or ρ c,α > 0. The following result can be found in (PZ01):

Theorem 1 Given secret sharing with its distribution table T and the defining function f on V n . Let c be any integer with 1 ≤ c ≤ n and α = (s 1 , . . . , s n ) be any vector in V n . Then there exists a vector α ′ ∈ V n such that ρ c,α + ρ c,α ′ = 1 otherwise ρ c,α = 1.

Theorem 1 implies that the maximum probability of successful cheating is always higher than or equal to 1 2 .

Given secret sharing with its distribution table T and the defining function f on V n . The value of

ρ c = 2 -n ∑ α∈V n ρ c,α
is the average cheating probability over all original vectors in V n for a fixed cheating vector. The value of

ρ = 1 n n ∑ c=1 ρ c = 1 n • 2 -n n ∑ c=1 ∑ α∈V n ρ c,α
is the average cheating probability over all cheating vectors (with Hamming weight one) and all original vectors in V n .

It should be noticed that the definition of ρ depends on a particular defining function f .

Theorem 2 Given secret sharing with its distribution table T and the defining function f on V n . Then for each fixed integer c with 1 ≤ c ≤ n, we have ρ c ≥ 1 2 where the equality holds if and only if ρ c,α = 1 2 for each α ∈ V n .

Proof 1 Write y = (x 1 , . . . , x c-1 ) and z = (x c+1 , . . . ,

x n ). Set R 1 = {(y, z)| f (y, 1, z) = 1, f (y, 0, z) = 1} R 2 = {(y, z)| f (y, 1, z) = 1, f (y, 0, z) = 0} R 3 = {(y, z)| f (y, 1, z) = 0, f (y, 0, z) = 1} R 4 = {(y, z)| f (y, 1, z) = 0, f (y, 0, z) = 0}
(1)

and #R i = r i , i = 1, 2, 3, 4. Obviously r 1 + r 2 + r 3 + r 4 = 2 n-1 . Let β 1 ∈ V c-1 , β 2 ∈ V n-c and α = (β 1 , 0, β 2 ) or α = (β 1 , 1, β 2 ).
Due to the definition of ρ c,α , it is easy to verify that

ρ c,α =                          r 1 r 1 +r 2 if α = (β 1 , 0, β 2 ), where (β 1 , β 2 ) ∈ R 1 r 2 r 1 +r 2 if α = (β 1 , 0, β 2 ), where (β 1 , β 2 ) ∈ R 2 r 3 r 3 +r 4 if α = (β 1 , 0, β 2 ), where (β 1 , β 2 ) ∈ R 3 r 4 r 3 +r 4 if α = (β 1 , 0, β 2 ), where (β 1 , β 2 ) ∈ R 4 r 1 r 1 +r 3 if α = (β 1 , 1, β 2 ), where (β 1 , β 2 ) ∈ R 1 r 3 r 1 +r 3 if α = (β 1 , 1, β 2 ), where (β 1 , β 2 ) ∈ R 3 r 2 r 2 +r 4 if α = (β 1 , 1, β 2 ), where (β 1 , β 2 ) ∈ R 2 r 4 r 2 +r 4 if α = (β 1 , 1, β 2 ), where (β 1 , β 2 ) ∈ R 4 (2)
There exist two cases to be considered: R j ∪ R i = / 0, where / 0 denotes the empty set, for each ( j, i) ∈ {(1, 2), (3, 4), (1, 3), (2, 4)}, and R j 0 ∪ R i 0 = / 0 for some ( j 0 , i 0 ) ∈ {(1, 2), (3, 4), (1, 3), (2, 4)}.

Case 1: R j ∪ R i = / 0 for each ( j, i) ∈ {(1, 2), (3, 4), (1, 3), (2, 4)}. In this case r j + r i = 0 for each ( j, i) ∈ {(1, 2), (3, 4), (1, 3), (2, 4)}. Therefore we can compute ρ c :

ρ c = 2 -n ∑ α∈V n ρ c,α = 2 -n ( r 2 1 r 1 + r 2 + r 2 2 r 1 + r 2 + r 2 3 r 3 + r 4 + r 2 4 r 3 + r 4 + r 2 1 r 1 + r 3 + r 2 3 r 1 + r 3 + r 2 2 r 2 + r 4 + r 2 4 r 2 + r 4 ) (3)
It is easy to see that (ab) 2 ≥ 0 or equivalently a 2 +b 2 a+b ≥ 1 2 (a + b) for any two real numbers with a, b ≥ 0 and a + b > 0 where the equality holds if and only if a = b. Using the same arguments on (3), we conclude that

ρ c ≥ 2 -n ( 1 2 (r 1 + r 2 ) + 1 2 (r 3 + r 4 ) + 1 2 (r 1 + r 3 ) + 1 2 (r 2 + r 4 )) = 2 -n (r 1 + r 2 + r 3 + r 4 ) = 1 2 (4)
where the equality holds if and only if r

1 = r 2 = r 3 = r 4 . From (2), r 1 = r 2 = r 3 = r 4 if and only if ρ c,α = 1 2 for each α ∈ V n . Therefore, in Case 1, ρ c ≥ 1 2
where the equality holds if and only if

ρ c,α = 1 2 for each α ∈ V n . Case 2: R j 0 ∪ R i 0 = / 0 for some ( j 0 , i 0 ) ∈ {(1, 2), (3, 4), (1, 3), (2, 4)
}. Without loss of generality we assume that R 1 ∪ R 2 = / 0. In this case r 1 = r 2 = 0 and thus r 3 + r 4 = 2 n-1 .

There exist two cases to be considered: R j ∪ R i = / 0 for each ( j, i) ∈ {(3, 4), (1, 3), (2, 4)}, and R j 1 ∪ R i 1 = / 0 for some ( j 1 , i 1 ) ∈ {(3, 4), (1, 3), (2, 4)}.

Case 2.1: R j ∪ R i = / 0 for each ( j, i) ∈ {(3, 4), (1, 3), (2, 4)}. In this case r j + r i = 0 for each ( j, i) ∈ {(3, 4), (1, 3), (2, 4)}.

We can compute ρ c :

ρ c = 2 -n ∑ α∈V n ρ c,α = 2 -n ( r 2 3 r 3 + r 4 + r 2 4 r 3 + r 4 + r 2 3 r 1 + r 3 + r 2 4 r 2 + r 4 ) Since r 1 = r 2 = 0, we have ρ c = 2 -n ∑ α∈V n ρ c,α = 2 -n ( r 2 3 +r 2 4 r 3 +r 4 + r 3 + r 4 ). Note that r 2 3 +r 4 2 r 3 +r 4 ≥ 1 2 (r 3 + r 4 ) and r 3 + r 4 = 2 n-1 . Thus we conclude that ρ c ≥ 2 -n ( 1 2 (r 3 + r 4 ) + r 3 + r 4 ) = 3 4 . Case 2.2: R j 1 ∪ R i 1 = / 0 for some ( j 1 , i 1 ) ∈ {(3, 4), (1, 3), (2, 4)}. Recall that r 3 + r 4 = 2 n-1 . Thus ( j 1 , i 1 ) = (3, 4). Without loss generality we assume that ( j 1 , i 1 ) = (1, 3). In other words, R 1 ∪ R 3 = / 0.
Thus r 3 = 0. Since r 1 = r 2 = r 3 = 0, we know that r 4 = 2 n-1 . We compute ρ c :

ρ c = 2 -n ∑ α∈V n ρ c,α = 2 -n ( r 2 4 r 3 + r 4 + r 2 4 r 2 + r 4 ) Since r 2 = r 3 = 0, we have ρ c = 2 -n (r 4 + r 4 ) = 1.
Summarising Cases 1 and 2, we have proved that ρ c ≥ 1 2 where the equality holds if and only if

ρ c,α = 1 2 for each α ∈ V n . ✷ f (x 1 , . . . , x n )| x c =1 is balanced. Similarly from the fact r 1 + r 3 = r 2 + r 4 , we conclude that f (x 1 , . . . , x n )| x c =0
is balanced. Since c is arbitrarily in {1, . . . , n}, we have proved that f is 1-resilient.

We now consider f (x) ⊕ f (x ⊕ δ c ) where δ c = (0, . . . , 0, 1, 0, . . . , 0) has been defined in Section 4. Let x = (y, x c , z) where y ∈ V c-1 , z ∈ V n-c and x c ∈ GF(2). ¿From (1),

f (x) ⊕ f (x ⊕ δ c ) = 0 if (y, z) ∈ R 1 or (y, z) ∈ R 4 1 if (y, z) ∈ R 2 or (y, z) ∈ R 3 (6) Since r 1 = r 2 = r 3 = r 4 , from (6), it is clear that f (x) ⊕ f (x ⊕ δ c
) is balanced. Note that c is an arbitrarily integer with 1 ≤ c ≤ n. Thus we have proved that f satisfies the SAC.

Conversely assume that f is 1-resilient and satisfies the SAC. Let c be an integer with 1 ≤ c ≤ n. Due to the 1-resilience, f (x 1 , . . . , x n )| x c =1 is balanced and thus r 1 + r 2 = r 3 + r 4 . Similarly f (x 1 , . . . , x n )| x c =0 is balanced and thus r 1 + r 3 = r 2 + r 4 .

On the other hand, since f satisfies the SAC, f (x) ⊕ f (x ⊕ δ c ) is balanced. From (6), we have r 1 + r 4 = r 2 + r 3 . Combing r 1 + r 2 = r 3 + r 4 , r 1 + r 3 = r 2 + r 4 and r 1 + r 4 = r 2 + r 3 , we conclude that r 1 = r 2 = r 3 = r 4 . From the proof of Theorem 2, we have proved that ρ c,α = 1 2 for each α ∈ V n . Since c is an arbitrarily integer with 1 ≤ c ≤ n, we have proved that the secret sharing is cheating immune. ✷

Since resilient functions are balanced, the defining function of any cheating immune secret sharing must be balanced.

Construction of Cheating-Immune Secret Sharing Scheme

Based on Theorem 4, to construct an cheating-immune secret sharing scheme, we need a 1-resilient function on V n satisfying the SAC.

The following result can be found from the proof of Theorem 17 of the reference (SM00), that is an article on boolean functions with cryptographic properties.

Lemma 1 Let h be a bent function on V n-2 (n is even). Set g(x 1 , . . . , x n-1 ) = (1 ⊕ x n-1 )h(x 1 , . . . ,

x n-2 ) ⊕ x n-1 (1 ⊕ h(x 1 ⊕ a 1 , . . . , x n-2 ⊕ a n-2 ))
where HW (a 1 , . . . ,

a n-2 ) = 1 2 n -1. Set f (x 1 , . . . , x n ) = (1 ⊕ x n )g(x 1 , . . . , x n-1 ) ⊕ x n g(x 1 ⊕ 1, . . . , x n-1 ⊕ 1) Then (i) f is 1-resilient, (ii) f satisfies the propagation criterion of degree 1 2 n -1, (iii) f has a nonlinearity 2 n-1 -2 1 2 n .
If we apply the function mentioned in Lemma 1 to Theorem 4, then we obtain an cheating-immune secret sharing with defining function whose nonlinearity is 2 n-1 -2 1 2 n . Therefore we have the following conclusion:

Theorem 5 Let n > 0 be an even integer. Then there exists a secret sharing with its distribution table T and the defining function f on V n such that (i) this secret sharing is cheating immune, (ii) the nonlinearity N f of f satisfies 2 n-1 -2 1 2 n . For each secret sharing constructed in (PZ01), there always exists some integer c and some vector α ∈ V n such that ρ c,α > 1 2 . Therefore each secret sharing in (PZ01) is not cheating immune.

Example 1 Let n = 4 in Lemma 1. Set h(x 1 , x 2 ) = x 1 x 2 . It is easy to see that h is a bent function on V 2 . Choose (a 1 , a 2 ) = (1, 0). Then HW (a 1 , a 2 ) = 1 = 1 2 n -1. Set g(x 1 , x 2 , x 3 ) = (1 ⊕ x 3 )h(x 1 , x 2 ) ⊕ x 3 (1 ⊕ h(1 ⊕ x 1 , x 2 )) = x 1 x 2 ⊕ x 2 x 3 ⊕ x 3
We further set

f (x 1 , x 2 , x 3 , x 4 ) = (1 ⊕ x 4 )g(x 1 , x 2 , x 3 ) ⊕ x 4 g(x 1 ⊕ 1, x 2 ⊕ 1, x 3 ⊕ 1) = x 1 x 2 ⊕ x 1 x 4 ⊕ x 2 x 3 ⊕ x 3 x 4 ⊕ x 3 ⊕ x 4
Due to Lemma 1, f is 1-resilient and satisfies the propagation criterion of degree 1 (SAC). Due to Theorem 4, this secret sharing is cheating immune. Let the group P include four participants and the defining function

f (x 1 , x 2 , x 3 , x 4 ) = x 1 x 2 ⊕ x 1 x 4 ⊕ x 2 x 3 ⊕ x 3 x 4 ⊕ x 3 ⊕ x 4
It is easy to find the truth table of f which is 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 1, 0, 1, 1, 1, 0

The secret sharing can be described as the following table :   f S 1 S 2 S 3 S 4 0 0 0 0 0 1 0 0 0 1 1 0 0 1 0 1 0 0 1 1 0 0 1 0 0 1 0 1 0 1 0 0 1 1 0 0 0 1 1 1 0 1 0 0 0 0 1 0 0 1 1 1 0 1 0 0 1 0 1 1 1 1 1 0 0 1 1 1 0 1 1 1 1 1 0 0 1 1 1 1

Using Theorem 4 or by a straightforward verification, we get that N f = 4 = 2 n-1 -2 1 2 n where n = 4. Assume that the dealer fixed the shares α = (1, 0, 1, 0) ∈ V 4 and the secret K = f (1, 0, 1, 0) = 1. Our cheater is P 3 . Thus δ 3 = (0, 0, 1, 0) and c = 3. The combiner obtains the sequence α * = (1, 0, 0, 0) with the third share changed by the cheater and returns the invalid secret K * = f (1, 0, 0, 0) = 0. On receiving K * , the cheater can identify the set

Ω * α = {(x 1 , x 2 , 1, x 4 )| f (x 1 , x 2 , 0, x 4 ) = 0}
which is Ω * α = {(0, 0, 1, 0), (0, 1, 1, 0), (1, 0, 1, 0), (1, 0, 1, 1)}. The set

Ω α = {(x 1 , x 2 , 1, x 4 )| f (x 1 , x 2 , 1, x 4 ) = 1}
becomes Ω α = {(0, 0, 1, 0), (0, 0, 1, 1), (1, 0, 1, 0), (1, 1, 1, 0)}. The intersection Ω * α ∩ Ω α = {(0, 0, 1, 0), (1, 0, 1, 0)} and the probability of successful cheating is ρ 3,α = #(Ω * α ∩ Ω α )/#Ω * α = 1 2 .

Conclusions

We have proved an interesting property of secret sharing. For given secret sharing, the average cheating probability over all cheating vectors and all original vectors, denoted by ρ, satisfies ρ ≥ 1 2 , and the equality holds if and only if the cheating probability ρ c,α satisfies ρ c,α = 1 2 for every cheating vector δ c and every original vector α. In this case the secret sharing is said to be cheating immune. We have found a relationship between cheating immune secret sharing and cryptographic criteria of boolean functions, and then we have successfully constructed cheating immune secret sharing using a highly nonlinear defining function. For simplicity, in this work we have considered cheating immune secret sharing where there is a single dishonest participant (or cheater). However this concept can be generalised for the case where there are many colluding cheaters. Future works include also the design of cheating immune secret sharing for a given access structure.

1365-8050 c 2004 Discrete Mathematics and Theoretical Computer Science (DMTCS), Nancy, France

Acknowledgements

The work was in part supported by Australian Research Council grant A00103078 and DP0345366. The authors thank the anonymous referees for helpful comments.

Theorem 3 Given secret sharing with its distribution table T and the defining function f on V n . Then ρ ≥ 1 2 where the equality holds if and only if ρ c,α = 1 2 for each integer c with 1 ≤ c ≤ n and each α ∈ V n .

Proof 2 By using Theorem 2, we have

Hence we have proved inequality in the theorem. Assume ρ = 1 2 . From ρ = 1 2 and ρ c ≥ 1 2 , c = 1, . . . , n, we know that ρ c = 1 2 , c = 1, . . . , n. By using Theorem 2, we know that ρ c,α = 1 2 for each integer c with 1 ≤ c ≤ n and each α ∈ V n . We have proved the necessity. The sufficiency is obvious. Hence we proved the theorem. ✷

Cheating-Immune Secret Sharing Scheme

Secret sharing resists cheating if either max{ρ c,α |α ∈ V n , 1 ≤ c ≤ n} is as small as possible, or ρ is as small as possible. As mentioned in Section 4, the maximum cheating probability is always larger than or equal to 1 2 . Due to Theorem 1, if ρ = 1 2 then the maximum cheating probability is equal to 1 2 . We now prove the converse. Assume that the maximum cheating probability is equal to 1 2 . We next prove that ρ c,α = 1 2 for each integer c with 1 ≤ c ≤ n and each α ∈ V n . Assume for contradiction that ρ c,α < 1 2 for some integer c with 1 ≤ c ≤ n and some α ∈ V n . According to Theorem 1, there exists another vector

2 . This contradicts the assumption that the maximum cheating probability is equal to 1 2 . The contradiction proves ρ c,α = 1 2 for each integer c with 1 ≤ c ≤ n and each α ∈ V n . In this case, clearly, ρ = 1 2 . Due to Theorems 2 and 3, we conclude Corollary 1 Given secret sharing with its distribution table T and the defining function f on V n . Then the following statements are equivalent:

(iii) ρ c,α = 1 2 for each integer c with 1 ≤ c ≤ n and each α ∈ V n . A secret sharing is said to be cheating immune if it satisfies (i) or (ii) or (iii) of Corollary 1.

Cheating immunity of secret sharing can be investigated in the context of well-known characteristics of the defining function f such as correlation immunity and SAC.

Theorem 4 Given secret sharing with its distribution table T and the defining function f on V n . Then the secret sharing is cheating immune if and only if f is 1-resilient and satisfies the SAC.

Proof 3 We keep using the notations as in the proof of Theorem 2. Assume that the secret sharing is cheating immune. Let c be an integer with 1 ≤ c ≤ n. Using Corollary 1, ρ c,α = 1 2 for each α ∈ V n . Therefore, from the proof of Theorem 2, we have r 1 = r 2 = r 3 = r 4 . From r 1 +r 2 = r 3 +r 4 , we conclude that