Jérémy Parriaux
email: jeremy.parriaux@esstin.uhp-nancy.fr

Philippe Guillot
email: philippe.guillot@univ-paris8.fr

Gilles Millérioux
email: gilles.millerioux@esstin.uhp-nancy.fr

Towards a Spectral Approach for the Design of Self-Synchronizing Stream Ciphers

Keywords: Self-synchronizing stream cipher, Boolean function, Walsh matrix, correlation matrix

This paper addresses the problem of characterizing the functions that can be used in the design of self-synchronizing stream ciphers. We propose a general framework based on a spectral characterization through correlation matrices or equivalently through Walsh matrices. Two modes of self-synchronization are discussed: the finite time one and the statistical one.

Introduction

Stream ciphers are cryptosystems specifically devoted to the transmission of data streams over public channels. At the transmitter side, the ciphertext is carried out by adding a plaintext symbol with a symbol of a pseudorandom stream called the key-stream. At the receiver side, the decryption consists in subtracting the ciphertext symbol with a symbol of, again, a pseudorandom stream. Proper decryption is achieved provided that the pseudorandom streams generated at the transmitter and receiver sides are the same. In other words, the pseudorandom generators have to be synchronized. There are two ways to ensure the synchronization. The first one is to use an external protocol in order to initialize the two generators with the same seed. The protocol must also be able to resynchronize the generators if the synchronization is lost. The resulting ciphers are known as synchronous stream ciphers. The second method relies on systems for which synchronization is due to a structural property. The corresponding ciphers are called self-synchronizing stream ciphers, SSSC for short. The absence of synchronization protocol makes them particularly appealing when high throughputs are required. As it turns out, very few works have paid attention to them. Let us mention [START_REF] Daemen | Cipher and Hash function design, strategies based on linear and differential cryptanalysis[END_REF][START_REF] Joux | Chosen-ciphertext attacks against mosquito. Fast Software Encryption[END_REF] for exceptions. This work aims at characterizing new functions which can be involved in self-synchronizing stream ciphers. The interest of enlarging the class of candidate functions lies in that they can potentially lead to systems of reduced size or with better cryptographic properties than the existing ones. The characterization is performed in the spectral domain and thereby allows to connect the results to the usual cryptographic criteria. The outline of this paper is the following: Section 2 is devoted to the problem statement. Section 3 recalls the usual material devoted to spectral analysis and Boolean functions. Section 4 deals with the spectral characterization of the selfsynchronizing property and is the core of the paper. Section 5 investigates the reachability of the states in terms of probability law. Finally, Section 6 is devoted to an illustrative example.

Problem Statement

Let us first introduce the notations. The two-element field is denoted by F 2 . The plaintext symbol to be ciphered at time t ∈ N is m t ∈ F 2 , the corresponding ciphertext is c t ∈ F 2 and the corresponding recovered plaintext is m t ∈ F 2 . In stream ciphers, the ciphertext c t is obtained from the plaintext m t by adding a random symbol z t ∈ F 2 . The original message m t is recovered by subtracting the symbol z t ∈ F 2 from the ciphertext c t . For binary streams the subtraction is the same operation than the addition. In the canonical representation of a selfsynchronizing stream cipher, the random symbols z t and z t are generated using the same keyed function g θ : F n 2 -→ F 2 whose arguments are a finite sequence of some past ciphertexts, namely c t-1 , . . . , c t-n . The parameter θ is the key of the system. The decryption is properly performed, that is m t = m t , whenever z t = z t . It is guaranteed if both the encryptor and the decryptor have same key and if the ciphertexts c t-1 , . . . , c t-n are properly transmitted. The equations of the canonical form of self-synchronizing stream ciphers are

z t = g θ (c t-1 , . . . , c t-n ) c t = m t + z t (encryptor) (1)
z t = g θ (c t-1 , . . . , c t-n ) m t = c t + z t (decryptor) (2)
Remark 1. As the synchronization, in general, operates on bit streams, it is relevant to consider binary input devices. Moreover, the generalization to device with input and output symbols of k bits is direct which allows for instance to apply the results to byte streams. The extension of the results to this case is discussed after the main results.

The canonical form admits an equivalent recursive form involving an internal state x ∈ F n 2 which is an n-dimensional Boolean vector. Its value at time t is x t = (c t-1 , . . . , c t-n ). Its i th coordinate is denoted by (x t ) i . The corresponding block diagram is depicted in Figure 1. The equations read The canonical recursive form (3)-( 4) is directly obtained from the canonical form (1)-( 2). The state updating transformation is a mere shift register fed with the previous ciphertexts. Thus, the initial state is eliminated in a shift-like way and all the complexity of the system lies in the function g θ . More interesting schemes are obtained when considering a keyed state updating transformation f θ : F 2 × F n 2 -→ F n 2 more complex than a shift. In this situation, the shift next-state function and the output function g θ are replaced by a function f θ and an output function h θ : F n 2 -→ F 2 . This setup is referred to as the generalized recursive form and its block diagram is depicted in Figure 2. The corresponding equations are   

   (x t+1 ) i = (x t ) i-1 if i > 0, c t if i = 0 z t = g θ (x t ) c t = m t + z t (encryptor) (3)    ( x t+1 ) i = ( x t ) i-1 if i > 0, c t if i = 0 z t = g θ ( x t ) m t = c t + z t (decryptor) (4)
g θ ⊕ ct mt zt n ct-n • • • ct-1 xt g θ ⊕ ct mt zt n ct-1 • • • ct-n xt
x t+1 = f θ (c t , x t ) z t = h θ (x t ) c t = m t + z t (encryptor) (5)    x t+1 = f θ (c t , x t ) z t = h θ ( x t ) m t = c t + z t (decryptor) (6)
In order to guarantee the self-synchronization property of the system, the function f θ cannot be chosen arbitrarily. It must have the property that, after a fixed number of iterations, denoted by t c , the key stream symbols z t and z t are equal for all t > t c . In the general case, this is achieved if and only if the current state of the decryptor is equal to the current state of the encryptor, x t = x t regardless of the initial states x 0 and x 0 . Clearly, given the system described by ( 5)-( 6), the self-synchronization can be studied by focusing exclusively on the function f θ . Besides, the fact that this recursive form is more general than a mere shift allows to relax the constraint that the synchronization is achieved within a finite amount of time. That leads to so-called statistical self-synchronizing stream ciphers. They will be detailed and motivated later on in this paper. This paper does not intend to study how the key θ is involved in the system. Therefore, for simplification purposes and hereafter, the subscript θ will be omitted, the parametrization with the key of the functions will be implicit. The introduction of the key is left for a further study. In the sequel, a function from the vector space F n 2 to F 2 will be referred to as a (n)-function. We will call a (n, m)-function a function from the vector space F n 2 to the vector space F m 2 . Indeed, a (n, m)-function f is nothing but a m-dimensional vector whose each coordinate is a (n)-function. The j th coordinate is denoted by f j and named the coordinate function. We recall a definition introduced by Klimov and Shamir in [START_REF] Klimov | A new class of invertible mappings[END_REF].

Definition 1 (T -function).

A (n, n)-function is called a T-function if the coordinate function f j depends only on the variables x i with i = 0, . . . , j. Some special T -functions of interest in our study are called strict T -functions, their definition is the following:

Definition 2 (Strict T -function).

A T -function such that the coordinate function f j depends only on the variable x i with i = 0, . . . , j -1 is called a strict T -function.

Note 1. What we call strict T-function is called parameter in [START_REF] Klimov | Cryptographic applications of t-functions[END_REF] however, we think that this name is misleading in our context and we prefer to use another name in order not to confuse the reader.

Having a look at the literature, it can be noticed that, so far, all the selfsynchronizing stream ciphers use the same principle in order to guarantee that the current state at time t does no longer depend on the initial state, that is to guarantee the self-synchronization. The state updating function is such that its coordinate functions depend on the bits of the internal state with strictly lower indexes than their own index. In other words, the state updating function is based on strict T -functions.

The main purpose of this paper is to pinpoint more general classes of functions which guarantee the self-synchronization property besides strict T -functions. Self-synchronization properties are addressed from a spectral point of view as motivated in the introduction.

Preliminaries

This section introduces a formal definition of self-synchronization and then recalls the strict necessary prerequisites on spectral analysis of Boolean functions from which our results will be derived.

Self-synchronization

Let us first formally define some self-synchronization related notions.

Definition 3 (Self-synchronizing sequence). A ciphertext sequence (c) is self-synchronizing for f if there exists an integer t c so that for all initial states x 0 and x 0 ∀t ≥ t c , x t = x t (7) Definition 4 (Finite-time self-synchronization). The system (5)-( 6) is finitetime self-synchronizing if the minimum value t c is upper bounded for all possible ciphertext sequences (c). The upper bound t c is called the self-synchronization delay of f . Remark 2. Finite-time self-synchronization means that there is an integer t c such that any sequence of length at least t c is a self-synchronizing sequence. The synchronization delay depends on the pair of initial states x 0 and x 0 . The delay t c is defined as the maximum delay over all initial state pairs. Definition 5 (Finite-time self-synchronizing function). A (n + 1, n)-function f is called finite-time self-synchronizing function if, when used as a nextstate function in the system (5)-( 6), the resulting system is finite-time selfsynchronizing.

Spectral Analysis

The rest of this section recalls the basics about Boolean spectral analysis. If f is a (n)-function, we denote by f its Fourier transform, which is by definition the real-valued mapping

F n 2 -→ R defined for any u ∈ F n 2 , by f (u) = x∈F n 2 f (x)(-1) x•u (8)
where

x • u = x 0 u 0 + • • • + x n-1 u n-1 .
The expression of the Walsh transform ( 8) also admits a matrix oriented representation f = Hf where H is the so called Hadamard matrix whose coefficients at row u and column v is

h u,v = (-1) u•v where u, v ∈ F n 2 .
The 2 n -dimensional vectors f and f are have their coordinate x equal to the corresponding function evaluated at x. Note 2. Matrices indexes may be without ambiguity either an integer or a binary vector being the binary expansion of this integer. This transform is invertible and the inverse is given by:

f = 2 n f (9)
When dealing with Boolean functions, we rather resort to the Walsh transform which gets nicer properties than the Fourier transform in most cases. The Walsh transform of a Boolean function f is the Fourier transform of its sign function

f χ where f χ (x) = (-1) f (x) = 1 -2f (x) for x ∈ F n 2 that is, f χ (u) = x∈F n 2 (-1) f (x)+x•u (10)
As shown in [START_REF] Carlet | Boolean Models and Methods in Mathematics, Computer Science, and Engineering, chapter Boolean Functions for Cryptography and Error-Correcting Codes[END_REF], the correspondence between the Fourier and Walsh transforms is given by

∀u ∈ F n 2 , f χ (u) = 2 n δ 0 (u) -2 f (u), (11)
where δ 0 (u) equals 1 if u is the n-dimensional zero vector and equals 0 elsewhere.

The Walsh matrix of any (n, m)-function is the 2 m × 2 n dimensional matrix [START_REF] Carlet | Boolean Models and Methods in Mathematics, Computer Science, and Engineering, chapter Vectorial Boolean Functions for Cryptography[END_REF]):

W f = w f u,v with u ∈ F m 2 and v ∈ F n 2 such that (see
w f u,v = x∈F n 2 (-1) u•f (x)+v•x (12)
The row u of the matrix W f is the Walsh transform of the linear combinations of the coordinates of f defined by x -→ u • f (x). The coefficients of the Walsh matrix of a function is called the spectrum of that function.

Correlation matrices have been defined in [START_REF] Daemen | Correlation matrices[END_REF], they are related to Walsh matrices by a mere normalization coefficient. If R f is the correlation matrix of f , then

R f = 2 -n W f (13)
with coefficients r f u,v . In the paper we usually use correlation matrices to derive the results but it could be done with Walsh matrices as well. The example is given in terms of Walsh matrices.

An interesting property relates the correlation matrices of composed functions.

Proposition 1 (see [START_REF] Carlet | Boolean Models and Methods in Mathematics, Computer Science, and Engineering, chapter Vectorial Boolean Functions for Cryptography[END_REF]).

If f is a (n, m)-function and g is a (p, n)-function then R f •g = R f R g (14)
After these necessary recalls, we are now in position of characterizing the selfsynchronization property from a spectral point of view.

Spectral Characterization of the Self-Synchronization Property

In this section, we focus on characterizing the self-synchronizing property of the system (5)- [START_REF] Carlet | Boolean Models and Methods in Mathematics, Computer Science, and Engineering, chapter Vectorial Boolean Functions for Cryptography[END_REF]. As motivated earlier, we can exclusively focus on the next-state function f . It is a (n + 1, n)-function depending both on the input stream and on the internal state. Let us denote by f 0 (respectively f 1 ) the (n, n)-function which is the restriction of f to the input bit c t = 0 (respectively to c t = 1). The function f can be expressed as

f (c t , x t ) = f 0 (x t ) if c t = 0 f 1 (x t ) if c t = 1 (15)
For our purpose, we must define the t th order iterated function of f . It is the (n + t + 1, n)-function denoted by φ t and defined by

φ t (c, x 0 ) = f ct • • • • • f c0 (x 0 ) for t > 0, c ∈ F t+1 2 , x 0 ∈ F n 2 (16)
We set φ 0 = f . For a prescribed ciphertext sequence (c) of length t + 1 and an initial state x 0 , the value φ t (c, x 0 ) is the internal state at time t + 1.

In this section, we characterize the self-synchronizing property in terms of correlation (or Walsh) coefficients. We first focus on self-synchronizing sequences and then apply their properties to address the finite-time and statistical selfsynchronization issues of the system (5)-(6).

Self-synchronizing sequences

Let us denote by φ c t (x) the (n, n)-function which is the restriction of φ t (c, x) to a fixed sequence (c) of length t + 1.

Proposition 2. The sequence (c) is self-synchronizing if and only if the correlation matrix of φ c t is a 2 n × 2 n correlation matrix of the form

R φ c t =      1 0 • • • 0 ±1 0 • • • 0 . . . . . . . . . ±1 0 • • • 0      (17)
Proof. By definition, if (c) is a self-synchronizing sequence, φ c t (x) does not depend on x thus, φ c t is a constant function. And yet, any linear combination of the coordinate functions of φ c t is also a constant function. It turns out that any row of (17) is the correlation transform of a constant function. The converse can be derived by using the inverse Fourier transform formula [START_REF] Parriaux | Synchronization of boolean dynamical systems: A spectral characterization[END_REF].

The matrix R φ c t can easily be determined from the knowledge of the correlation matrices of f 0 and f 1 .

Proposition 3. The expression of the correlation

matrix R φ c t is R φ c t = R f c t × • • • × R f c 0 (18)
Proof. The proof is a direct consequence of Proposition 1.

In the following, we use these results to derive some characteristics of the correlation matrices of the functions that have the self-synchronization property.

Finite-time Self-Synchronization

Let us first notice some important features of correlation matrices. In the sequel, we consider W as a square correlation matrix of dimension q × q.

R =      1 0 • • • 0 r 1,0 r 1,1 • • • r 1,q-1 . . . . . . . . . r q-1,0 r q-1,1 • • • r q-1,q-1      (19)
The matrix W can be rewritten

W = A + N with A =      1 0 • • • 0 r 1,0 0 • • • 0 . . . . . . . . . r q-1,0 0 • • • 0      N =      0 0 • • • 0 0 r 1,1 • • • r 1,q-1 . . . . . . . . . 0 r q-1,1 • • • r q-1,q-1     
A matrix is said to be of type A if the only non-zero coefficients are located on the first column. A matrix is said to be of type N if all the coefficients of the first row and first column are zero. It is straightforward to verify the following remark:

Remark 3.
the product of any two matrices of type A is a matrix of type A; the product of any matrix of type A with any matrix of type N is a zero matrix; the product of any matrix of type N with any matrix of type A is a matrix of the type A; the product of any two matrices of type N is a matrix of type N .

R f 0 = A f 0 + N f 0 and R f 1 = A f 1 + N f 1 . The product R = R f c t × • • • × R f c 0 is of type A if and only if the matrix N f c t × • • • × N f c 0 is null. Proof. R = R f c t × • • • × R f c 0 = (A f c t + N f c t ) × • • • × (A f c 0 + N f c 0 ) (20)
By expanding the expression and using Remark 3, R can be rewritten R = A+N with a type-A matrix A and a type-

N matrix N = N f c t × • • • × N f c 0 .
Because of its structure, A cannot cancel the non-zero coefficients of N . Therefore, R is a type-A matrix if and only if N is null.

The self-synchronization property in the spectral domain can have an algebraic interpretation. It is based on the concept of semigroup.

A semigroup is a set together with an associative internal law. For instance the set of the 2 n × 2 n correlation matrices together with the matrix multiplication is a semigroup. A nilpotent element e is an element such that there exists a large enough positive integer k for which e k is equal to an absorbing element denoted by 0. A semigroup is said to be generated by a family of elements E = {e 0 , . . . , e n } if any element of the semigroup can be expressed in terms of a product of finite length of elements of E. A nilpotent semigroup is a semigroup that has an absorbing element 0 and in which each element is nilpotent. The nilpotency class of a semigroup S is the smallest positive integer k such that ∀e ∈ S, e k = 0.

Proposition 5. The system (5)-( 6) is finite-time self-synchronizing if and only if the matrices N f 0 and N f 1 span a nilpotent semigroup.

Proof. According to Remark 2, a system is finite-time self-synchronizing if and only if there is a positive integer t c such that any sequence of length greater than t c is self-synchronizing. That is, in view of Proposition 2, for t > t c , any correlation matrix R φ c t is of type A. The expression of R φ c t given by ( 18) is, up to a constant factor, the product of t + 1 elements of the pair {R f 0 , R f 1 }.

According to Proposition 4 this product is of type A if and only if whatever is c ∈ F t+1 2 , the product N f c t × • • • × N f c 0 is null. This is the case if and only if the pair {N f 0 , N f 1 } spans a nilpotent semigroup of nilpotency class at most t + 1. Now, we aim at pinpointing different classes of self-synchronizing functions. To this end, let us recall an interesting theorem stated in [START_REF] Radjavi | Simultaneous Triangularization[END_REF] (Theorem 2.1.7).

Theorem 1 (Levitski's theorem). Any semigroup of nilpotent matrices is triangularizable.

For any square correlation matrix R of dimension 2 n , let us define its reduced matrix R * of dimension (2 n -1) × (2 n -1) which is the matrix R in which the first row and column have been removed.

R =    r 1,1 • • • r 1,q-1 . . . . . . r q-1,1 • • • r q-1,q-1   
The reduced Walsh matrix W * of a Walsh matrix W is defined in the same way.

Remark 4. Note that the reduced matrix of N is R * as well.

Next proposition makes a classification of the possible situations that allow the system ( 5)-( 6) to be finite-time self-synchronizing. It clearly gives a characterization of the functions that can be used in the design of finite-time SSSC.

Proposition 6. The system (5)-( 6) with the next-state function f (and the associated (n, n)-functions f 0 and f 1 ) is finite-time self-synchronizing if and only if the reduced correlation matrices R * f 0 and R * f 1 are nilpotent and fulfill one of the following cases: Case 1 Both matrices R * f 0 and R * f 1 are lower triangular. Case 2 Both matrices R * f 0 and R * f 1 are not lower triangular but can be simultaneously triangularized by a change of basis whose matrix is the reduced correlation matrix R * p of some (n, n)-function p. This matrix has to be invertible. In this situation, the following equalities hold:

R * p R * f 0 (R * p ) -1 = R * f 0 and R * p R * f 1 (R * p ) -1 = R * f 1 with R * f 0 and R * f 1 two
lower triangular matrices with zeros on the diagonal. Case 3 Both matrices R * f 0 and R * f 1 are not lower triangular. They can be however simultaneously triangularized like in Case 2. but unlike Case 2, R * p does not correspond to a correlation matrix.

Proof. Proposition 5 states that the system (5)-( 6) is finite-time self-synchronizing if and only if N 0 f and N 1 f span a nilpotent semigroup. In view of Remark 4, the same holds for the matrices R * f 0 and R * f 1 . Then, in view of Theorem 1, they can be simultaneously triangularized. Cases 1, 2 and 3 are exclusive and describe all the possible situations.

The following lemma is required in order to interpret the significance of Proposition 6.

Lemma 1. For any bijection p of

F n 2 the relation (R * p ) -1 = R * p -1 holds.
Proof. It can be seen from ( 14) that R p -1 = (R p ) -1 . Since p is an invertible transformation we know from [START_REF] Daemen | Correlation matrices[END_REF] that its correlation matrix is orthogonal. If we denote the transpose of R by R t then,

(R * p ) -1 = (R * p ) t = (R t p ) * = (R -1 p ) * = (R p -1 ) *
Case 1 corresponds to the case when f 0 and f 1 are strict T -functions. Indeed, the reduced correlation matrix is lower triangular with zeros on diagonal except on the first row if and only if the corresponding function is a strict T -function (see Proposition 11 in [9]). Therefore Case 1 refers to functions which have been already proposed through the open literature. Case 2 corresponds to the situation when f 0 and f 1 are not strict T -functions but functions of the form

f 0 = p • f 0 • p -1 and f 1 = p • f 1 • p -1
where f 0 and f 1 are strict T -functions and p a bijection over F n 2 . A consequence of Lemma 1 is that this case is nothing but Case 1 in which the functions f 0 and f 1 have been both right-composed with the same bijective function p and left composed with p -1 . Thus, this case is equivalent to Case 1 up to an invertible transformation of the internal state. Case 3 corresponds to self-synchronizing functions that are not based on strict T -functions. This case is the most interesting one insofar as it allows to identify new classes of self-synchronizing functions. An example of such a function is given in Section 6.

Remark 5. It is interesting to note that the synchronization delay t c precisely corresponds to the nilpotency class of the semigroup spanned by R * f 0 and R * f 1 . Moreover, since Cases 1 and 2 are based on strict T -functions, the maximum nilpotency class is bounded by n in these situations. In Case 3 the maximum nilpotency class is the dimension of the matrices which is 2 n -1. Therefore, if two reduced correlation matrices R * f 0 , R * f 1 span a nilpotent semigroup of nilpotency class greater than n, it necessary corresponds to Case 3.

The problem of determining if any two (n, n)-functions f 0 and f 1 can be used to design finite-time self-synchronizing systems as defined by ( 5)-( 6) amounts to checking whether or not their reduced correlation matrices R * f 0 and R * f 1 span a nilpotent semigroup. From Proposition 5, if this is the case they can be simultaneously triangularized. The book [START_REF] Radjavi | Simultaneous Triangularization[END_REF] provides interesting approaches to determine whether or not a set of matrices can be simultaneous triangularized. An algorithm that simultaneously triangularizes a set of matrices is given in the paper [START_REF] Dubi | An algorithmic approach to simultaneous triangularization[END_REF]. The algorithm can be applied to any set of matrices, it simply fails when no common triangularization basis exists.

Extension to multi-bit symbols We now explains how to extend these results to streams whose symbols are composed of more than one bit, say k bits for instance. In this situation, m t , c t , m t and z t belong to F k 2 . The next state function is now f :

F k 2 × F n 2 -→ F n 2 and the output function is h : F n 2 -→ F k 2 .
In order to extend the previous results it is necessary to do the same decomposition of f than in (15). This time, f can be viewed as a set of 2 k functions

f i : F n 2 -→ F n 2 for i ∈ F k 2 .
All the previous results can be extended. It suffices to consider the 2 k matrices R f i instead of only two matrices. Essentially, the following result holds Proposition 7. The system is finite-time self-synchronizing if and only if the set of reduced correlation matrices R * f i span a nilpotent semigroup.

Proof. The proof is the same as in Proposition 5 except that there are now 2 k matrices to consider instead of only 2.

The classification of proposed in Proposition 6 still holds.

Statistical Self-Synchronization

In this paragraph, in order to enlarge the class of potential candidate functions, we relax the finite-time self-synchronization constraint and extend Definition 4. Indeed, in practice, it is acceptable that the synchronization delay t c is not bounded, but may be a random variable with a probability law that decreases to zero as time goes to infinity. In other words, the probability of being synchronized reaches one while the length of the stream (c) increases. This concept is viable only if the probability of being synchronized is sufficiently close to one for some reasonable length. Such systems are called statistical SSSC. If (c) is a random sequence then, the synchronization delay t c is a random variable. In such a case, it is denoted by T c .

Definition 6 (Statistical self-synchronization). The system (5)-( 6) is statistically self-synchronizing if lim t→+∞ Pr(T c ≤ t) = 1. The random variable T c is called the random synchronization delay for the random sequence (c).

Remark 6. It is interesting to note that if the probability of synchronization is one for some constant delay, Definition 6 reduces to Definition 4. Therefore, finite-time self-synchronization is nothing but a special case of statistical selfsynchronization.

State Probability

Ensuring the self-synchronizing property is a first feature required for the design of SSSC. The security has to be further assessed. From this perspective, we think it is interesting to determine the probability that a given state can be reached after a fixed number of iterations. A cryptographic criterion is that at the decryptor side, all the states are reached with almost the same probability, ideally the same, for a random cryptogram stream symbols. Studying this criterion is the purpose of this section.

Let us first consider the following matter. We are given a (n, m)-function g and a random variable X ∈ F n 2 whose value is described by the probability law p :

F n 2 -→ R defined by p(x) = Pr[X = x].
We want to know the probability law q : F m 2 -→ R that describes the random variable Y ∈ F m 2 defined by Y = g(X). The function q is defined by q(y) = Pr[y = g(X)]. Without ambiguity, the notation p (respectively q) refers either to the function or to the 2 n (respectively 2 m ) column vector whose coordinate index x ∈ F n 2 (respectively y ∈ F m 2 ) has the value p(x) (respectively q(y)). The same holds for p and q which are the Fourier transforms of p and q. Proposition 8. Let R g be the correlation matrix of g. Applying the function g to a variable whose value is chosen according to the probability law described by p gives a vector whose value is described by the probability law q. They are related by the relation

q = R g p (21)
Proof. Let us first relate q and p.

q(y) = x∈F n 2 |g(x)=y p(x) = 2 -m x∈F n 2 p(x) u∈F m 2 (-1) u(g(x)+y) = 2 -m u∈F m 2 x∈F n 2 (-1) u•y p(x)(-1) u•g(x)
We now express the Fourier transform of q.

q(s) = y∈F m 2 q(y)(-1) s•y = 2 -m u∈F m 2 ,x∈F n 2 y∈F m 2 (-1) u•y+s•y    2 m if u = s 0 else p(x)(-1) u•g(x) = x∈F n 2 p(x)(-1) s•g(x) = 2 -n x∈F n 2 p(x) z∈F n 2 (-1) s•g(z) v∈F n 2 (-1) v•(x+z) = v∈F n 2 x∈F n 2 p(x)(-1) v•x p(v) 2 -n z∈F n 2 (-1) s•g(z)+v•z r g s,v =2 -n w g s,v
where w g s,v is as defined by [START_REF] Crama | Boolean Models and Methods in Mathematics[END_REF]. The result holds.

The following corollary can be stated

Corollary 1. q = H -1 R g Hp (22)
Proof. Equation (21) also reads Hq = R g Hp. The result holds.

If we restrict the vector p of Proposition 8 to the uniform probability vector the following corollary, which corresponds to Lemma 1 in [START_REF] Nyberg | Multidimensional walsh transform and a characterization of bent functions[END_REF], is direct.

Corollary 2. Let X follow the uniform distribution and g be a (n, n)-function.

The probability distribution, after applying the function g to X reads

∀x ∈ F n 2 , Pr[g(X) = x] = 2 -n s∈F n 2 (-1) s•x r g s,0 (23)
where r g s,0 is the coefficient of the correlation matrix of g of the s th row and of the first column.

Till now, we have always considered that the initial state x 0 is chosen according to the uniform distribution. We have also assumed that the symbols of the ciphertext stream (c) are uniformly distributed. Let us stress that even though this assumption makes sense in cryptography since the stream (c) should not be distinguishable from a true uniform random stream, it should be considered with caution. Indeed, the uniformity of (c) depends on the uniformity of (z) which in turn depends on the function f and h. We now focus on the evolution of the probability law modified by the next-state function f . Proposition 9. Let (C) be a uniform random sequence and assume a uniform random distribution of the initial state X 0 . Then, the probability that the iterated function φ C t returns the state x ∈ F n 2 is

P [φ C t (X 0 ) = x] = 1 2 n+t+1 s∈F n 2 (-1) s•x R f 0 + R f 1 t+1 s,0 (24)
Proof. Since (C) is a uniform random sequence of length t + 1, the probability of having this specific sequence in t + 1 iterations is 2 -t-1 .

P [φ C t (X 0 ) = x] = 1 2 t+1 c∈F t+1 2 P [f Ct • • • • • f C0 = x]
Then, in view of Proposition 1 and Corollary 2

P [φ C t (X 0 ) = x] = 1 2 t+1 c∈F t+1 2 1 2 n s∈F n 2 (-1) s•x R f C t × • • • × R f C 0 s,0 = 1 2 n+t+1 s∈F n 2 (-1) s•x R f 0 + R f 1 t+1 s,0
Proposition 10. Assuming a random sequence (C) of length t+1 and a random initial state X 0 , the system (5)-( 6) has an equal probability to be in each state if and only if the first column of the matrix R f 0 + R f 1 t+1 denoted by r 0 is given by

r 0 = 2 t+1 0 • • • 0 T (25)
Proof. Proving this result amounts to solving a linear algebra problem. Let ν be the 2 n -dimensional column vector whose coefficients at row x is the probability of being in the state x. In our case, we set the value of each coefficient to 2 -n . Considering Proposition 9, denoting by H the 2 n -dimensional Hadamard matrix defined by H = (h s,x ) = (-1) s•x for s, x ∈ F n 2 and by k the constant 2 -n-t-1 , the problem reads ν = kHr 0 where r 0 is the unknown. Since both k and H are invertible, the system can be solved and has a unique solution.

Remark 7. The fact that each state is reached with an equal probability for a random sequence of length t + 1 does not mean that each state is reached with an equal probability with a uniform random sequence of length t + 2.

Remark 8. Proposition 10 states that assuming a uniform distribution of the initial state X 0 and a uniform random sequence (C), the uniform distribution of the internal state at time t is achieved if and only if the first column vector of R f 0 + R f 1 t+1 is given by the relation (25). Under this condition, a uniform distribution is achieved at any time if and only if f is balanced.

Since the first column of R f 0 + R f 1 is the same as the first column of R f , if f is balanced, the condition r f 0 s,0 = -r f 1 s,0 if s = 0 holds.

Example

As an illustration of the finite-time SSSC described by Case 3 in Section 4.2, let us show that the set of functions described by Case 3 is not empty. In this example we rather use Walsh matrices than correlation matrices, it allows to have matrices with integer coefficients. We recall that the correspondence between these two kind of matrices is given by (13). We consider n = 3. The next-state function f is based on two almost-bent functions f 0 and f 1 as defined by (15):

   f 0 0 (x) = 1 + x 0 + x 1 + x 0 x 2 f 0 1 (x) = 1 + x 0 x 1 + x 2 + x 0 x 2 f 0 2 (x) = x 1 x 2    f 1 0 (x) = x 0 x 1 + x 2 f 1 1 (x) = 1 + x 0 + x 0 x 1 + x 1 x 2 f 1 2 (x) = 1 + x 0 + x 0 x 1 + x 0 x 2
Then, the reduced Walsh matrices can be worked out by using ( 12) According to Theorem 1, the matrices W * f 0 and W * f 1 span a nilpotent semigroup. Indeed, they can be simultaneously triangularized and the algorithm of the paper [START_REF] Dubi | An algorithmic approach to simultaneous triangularization[END_REF] allows to find out one possible change of basis. The matrix

W * f 0 =           0
W * p =          
1 -1 -2 -2 4 0 0 1 -1 4 0 0 0 0 0 0 0 -4 -2 2 0 0 2 1 -3

1 -1 -1 -1 -1 1 -3 1 -1 1 1 1 -1 -1 -3 -1 1 0 2 1 1 3 1 1          
triangularizes both W * f 0 and W * f 1 . It can be checked that the class of nilpotency of this semigroup is larger than n and because of Remark 5 there are no bijection from F 3 2 that allows to triangularize the semigroup. Therefore this system corresponds to Case 3.

The algebraic normal form of f is    f 0 (c, x) = 1 + x 0 + x 1 + x 0 x 2 + c + x 0 c + x 1 c + x 0 x 1 c + x 2 c + x 0 x 2 c f 1 (c, x) = 1 + x 0 x 1 + x 2 + x 0 x 2 + x 0 c + x 2 c + x 0 x 2 c + x 1 x 2 c f 2 (c, x) = x 1 x 2 + c + x 0 c + x 0 x 1 c + x 0 x 2 c + x 1 x 2 c This function is balanced, in view of Remark 8 each state is reached with the same probability.

Conclusion

Two kinds of self-synchronization have been defined. Finite-time self-synchronization has been characterized from the spectral analysis point of view. It has been shown that it is possible to achieve finite-time self-synchronization using functions which are not strict T -functions. Three cases have been pinpointed. The known strict T -function case, the case when strict T -functions have been right and left composed with a permutation and its inverse and the case which is not based on strict T -functions. The latter case is interesting due to its novelty, an algebraic characterization in terms of nilpotent semigroups has been performed. The example encourages to study the problem from this point of view since it shows that Case 3 contains functions that are worth to be considered. We then have discussed statistical self-synchronization as a generalization of finite-time self-synchronization. These characterizations will provide constructive material in order to find out classes of keyed families of functions for cryptographic purposes. The way how to incorporate performance constraints regarding the security deserves a deeper insight in the perspective of designing fully specified self-synchronizing stream ciphers.

Fig. 1 :

 1 Fig. 1: Canonical recursive form of self-synchronizing stream ciphers

Fig. 2 :

 2 Fig. 2: Generalized recursive form of self-synchronizing stream ciphers

Proposition 4 .

 4 Consider a Boolean sequence (c) of length t + 1 and the correlation matrices of the two (n, n)-functions f 0 and f 1 :


Mathieu Giorgino

Martin Strecker

Ralph Matthes

Marc Pantel

Verification of the Schorr-Waite algorithm -From trees to graphs

Keywords: Verification of imperative programs, Pointer algorithms, Program refinement

This article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement -functional to imperative and tree to graph -finally merged to obtain the result. Our imperative specifications use monadic constructs and syntax sugar, making them close to common imperative languages. This work has been realized within the Isabelle/HOL proof assistant.

Introduction

The Schorr-Waite algorithm [START_REF] Schorr | An efficient machine independent procedure for garbage collection in various list structures[END_REF] is an in-place graph marking algorithm that traverses a graph without building up a stack of nodes visited during traversal. Instead, it codes the backtracking structure within the graph itself while descending into the graph, and restores the original shape on the way back to the root. Originally conceived to be a particularly space-efficient algorithm to be used in garbage collectors, it has meanwhile become a benchmark for studying pointer algorithms.

A correctness argument for the Schorr-Waite (SW) algorithm is non-trivial, and a large number of correctness proofs, both on paper and machine-assisted, has accumulated over the years. All these approaches have in common that they start from a low-level graph representation, as elements of a heap which are related by pointers (see Section 7 for a discussion).

In this paper, we advocate a development that starts from high-level structures (Section 2), in particular inductively defined trees, and exploits as far as possible the corresponding principles of computation (mostly structural recursion) and reasoning (mostly structural induction). We then proceed by refinement, along two dimensions: on the one hand, by mapping the inductively defined structures to a low-level heap representation (Sections 3 and 4), on the other hand, by adding pointers to the trees, to obtain genuine graphs (Sections 5). These two developments are joined in Section 6.

We argue that this method has several advantages over methods that manipulate lower-level structures:

-Termination of the algorithms becomes easier to prove, as the size of the underlying trees and similar measures can be used in the termination argument. -Transformation and also preservation of structure is easier to express and to prove than when working on a raw mesh of pointers. In particular, we can state succinctly that the SW algorithm restores the original structure after having traversed and marked it. -Using structural reasoning such as induction allows a higher degree of proof automation: the prover can apply rewriting which is more deterministic than the kind of predicate-logic reasoning that arises in a relational representation of pointer structures.

Technically, the main ingredients of our development are, on the higher level, spanning trees with additional pointers parting from the leaf nodes to represent graphs with an out-degree of 2 (by a standard encoding of lists by binary trees we can in fact encode arbitrary finite graphs). During the execution of the algorithm, the state space is partitioned into disjoint areas that may only be linked by pointers which satisfy specific invariants. On the lower level, we use statetransformer and state-reader monads for representing imperative programs. The two levels are related by a refinement relation that is preserved during execution of the algorithms. In this article, the refinement is carried out manually, but in the long run, we hope to largely automate this step.

Even though, taken separately, most of these ingredients are not new (see Section 7 for a discussion of related work), this paper highlights the fact that relatively complex graph algorithms can be dealt with elegantly when perceiving them as refinements of tree algorithms.

The entire development has been carried out in the Isabelle theorem prover [START_REF] Nipkow | HOL. A Proof Assistant for Higher-Order Logic[END_REF], which offers a high degree of automation -most proofs are just a few lines long. The formalization itself does not exploit any specificities of Isabelle, but we use Isabelle's syntax definition facilities for devising a readable notation for imperative programs. A longer version of this paper with details of the proofs is available at [START_REF] Giorgino | Verification of the Schorr-Waite algorithm -From trees to graphs[END_REF].

Schorr-Waite on Pure Trees

A few words on notation before starting the development itself: Isabelle/HOL's syntax is a combination of mathematical notation and the ML language. Type variables are written ′ a, ′ b, . . . , total functions from α to β are denoted by α ⇒ β and type constructors are post-fix by default (like ′ a list). -→/=⇒ are both implication on term-level/meta-level where the meta-level is the domain of proofs. [[a 0 ; ... ;a n ]] =⇒ b abbreviates a 0 =⇒ (. . . =⇒ (a n =⇒ a). . . ). Construction and concatenation operators on lists are represented by x # xs and xs @ ys. Sometimes we will judiciously choose the right level of nesting for pattern matching in definitions, in order to take advantage of case splitting to improve automation in proofs.

The high-level version of the algorithm operates on inductively defined trees, whose definition is standard:

datatype ( ′ a, ′ l ) tree = Leaf ′ l | Node ′ a (( ′ a, ′ l ) tree) (( ′ a, ′ l ) tree)
The SW algorithm requires a tag in each node, consisting of its mark, here represented by a boolean value (True for marked, False for unmarked) and a "direction" (left or right), telling the algorithm how to backtrack. We store this information as follows:

datatype dir = L | R datatype ′ a tag = Tag bool dir ′ a
With these preliminaries, we can describe the SW algorithm. It uses two "pointers" t and p (which, for the time being, are trees): t points to the root of the tree to be traversed, and p to the previously visited node. There are three main operations:

-As long as the t node is unmarked, push moves t down the left subtree, turns its left pointer upwards and makes p point to the former t node. The latter node is then marked and its direction component set to "left". -Eventually, the left subtree will have been marked, i. e. t's mark is True, or t is a Leaf. If p's direction component says "left", the swing operation makes t point to p's right subtree, the roles of p's left and right subtree pointers are reversed, and the direction component is set to "right". -Finally, if, after the recursive descent, the right subtree is marked and p's direction component says "right", the pop operation will make the two pointers move up one level, reestablishing the original shape of t. Our algorithm uses two auxiliary functions sw-term (termination condition) and sw-body, the body of the algorithm with three main branches as in the informal characterisation above. The function sw-body should not be called if t is marked and p is a Leaf, so it returns an insignificant result in this case.

fun sw-term :: (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) ⇒ bool where sw-term (p, t) = (case p of Leaf -⇒ (case

t of Leaf -⇒ True | (Node (Tag m d v ) tlf tr ) ⇒ m) | - ⇒ False)
fun sw-body :: (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) ⇒ (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) where sw-body (p, t) = (case t of (Node (Tag False d v ) tlf tr ) ⇒ ((Node (Tag

True L v ) p tr ), tlf ) | -⇒ (case p of Leaf -⇒ (p, t) | (Node (Tag m L v ) pl pr ) ⇒ ((Node (Tag m R v ) t pl ), pr ) | (Node (Tag m R v ) pl pr ) ⇒ (pr , (Node (Tag m R v ) pl t))))
The SW algorithm on trees, sw-tr, is now easy to define, using the p and t pointers like a zipper data-structure [START_REF] Huet | Functional pearl: The zipper[END_REF]. We note in passing that sw-tr is tail recursive. If coding it in a functional programming language, your favorite compiler will most likely convert it to a while loop that traverses the tree without building up a stack.

function sw-tr :: (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) ⇒ (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) where sw-tr args = (if (sw-term args) then args else sw-tr (sw-body args))

We still have to prove the termination of the algorithm. We note that either the number of unmarked nodes decreases (during push), or it remains unchanged and the number of nodes with "left" direction decreases (during swing), or these two numbers remain unchanged and the p tree becomes smaller (during pop). This double lexicographic order is expressed in Isabelle as follows (with the predefined function size, and unmarked-count and left-count with obvious definitions): Please note that the algorithm works on type ( ′ a tag, ′ l ) tree with an arbitrary type for the data in the leaf nodes, which will later be instantiated by types for references.

Let's take a look at some invariants of the algorithm. The first thing to note is that the t tree should be consistently marked: Either, it is completely unmarked, or it is completely marked. This is a requirement for the initial tree: a marked root with unmarked nodes hidden below would cause the algorithm to return prematurely, without having explored the whole tree. We sharpen this requirement, by postulating that in a t tree, the direction is "right" iff the node is marked. This is not a strict necessity, but facilitates stating our correctness theorem. We thus arrive at the following two properties t-marked True and t-marked False for t trees that are defined in one go:

primrec t-marked :: bool ⇒ ( ′ a tag, ′ l ) tree ⇒ bool where t-marked m (Leaf rf ) = True | t-marked m (Node n l r ) = (case n of (Tag m ′ d v ) ⇒ (((d = R) = m) ∧ m ′ = m ∧ t-marked m l ∧ t-marked m r ))
We can similarly state a property of a p tree. We note that such a tree is composed of an upwards branch that is again a p-shaped tree, and a downwards branch that, depending on the direction, is either a previously marked t tree or an as yet unexplored (and therefore completely unmarked) t tree:

primrec p-marked :: ( ′ a tag, ′ l ) tree ⇒ bool where p-marked (Leaf rf ) = True | p-marked (Node n l r ) = (case n of (Tag m d v ) ⇒ (case d of L ⇒ (m ∧ p-marked l ∧ t-marked False r ) | R ⇒ (m ∧ t-marked True l ∧ p-marked r )))
We note in passing that these two properties are invariants of sw-body. What should the correctness criterion for sw-tr be? We would like to state that sw-tr behaves like a traditional recursive tree traversal (implicitly using a stack!) that sets the mark to True. Unfortunately, SW not only modifies the mark, but also the direction, so the two components have to be taken into account:

fun mark-all :: bool ⇒ dir ⇒ ( ′ a tag, ′ l ) tree ⇒ ( ′ a tag, ′ l ) tree where mark-all m d (Leaf rf ) = Leaf rf | mark-all m d (Node (Tag m ′ d ′ v ) l r ) = (Node (Tag m d v ) (mark-all m d l ) (mark-all m d r ))
By using the function mark-all we also capture the fact that the shape of the tree is unaltered after traversal. Of course, if a tree is consistently marked, it is not modified by marking with True and direction "right":

lemma t-marked-R-mark-all : t-marked True t -→ mark-all True R t = t
A key element of the correctness proof is that at each moment of the SW algorithm, given the p and t trees, we can reconstruct the shape of the original tree (if not its marks) by climbing up the p tree and putting back in place its subtrees:

fun reconstruct :: (( ′ a tag, ′ l ) tree * ( ′ a tag, ′ l ) tree) ⇒ ( ′ a tag, ′ l ) tree where reconstruct (Leaf rf , t) = t | reconstruct ((Node n l r ), t) = (case n of (Tag m d v ) ⇒ (case d of L ⇒ reconstruct (l , (Node (Tag m d v ) t r )) | R ⇒ reconstruct (r , (Node (Tag m d v ) l t))))
For this reason, if two trees t and t ′ have the same shape (i. e. are the same after marking), they are also of the same shape after reconstruction with the same p.

Application of sw-body does not change the shape of the original tree that p and t are reconstructed to:

lemma sw-body-mark-all-reconstruct: [[ p-marked p; t-marked m ′ t; ¬ sw-term (p, t) ]] =⇒ mark-all m d (reconstruct (sw-body (p, t))) = mark-all m d (reconstruct (p, t))
Obviously, if t is t-marked and we are in the final state of the recursion (sw-term is satisfied), then t is marked as true and p is empty. Together with the invariant of sw-body just identified, an induction on the form of the recursion of sw-tr gives us:

lemma sw-tr-mark-all-reconstruct: let (p, t) = args in (∀ m. t-marked m t -→ p-marked p -→ (let (p ′ , t ′ ) = (sw-tr args) in mark-all True R (reconstruct (p, t)) = t ′ ∧ (∃ rf . p ′ = Leaf rf )))
For a run of sw-tr starting with an empty p, we obtain the desired theorem (which, of course, is only interesting for the non-trivial case m=False):

theorem sw-tr-correct: t-marked m t =⇒ sw-tr (Leaf rf , t) = (p ′ , t ′ ) =⇒ t ′ = mark-all True R t ∧ (∃ rf . p ′ = Leaf rf )
To show the brevity of the development, the full version of the paper [START_REF] Giorgino | Verification of the Schorr-Waite algorithm -From trees to graphs[END_REF] reproduces the entire Isabelle script up to this point, which is barely 5 pages long.

Imperative Language and its Memory Model

This section presents a way to manipulate low-level programs. We use a heaptransformer monad providing means to reason about monadic/imperative code along with a nice syntax, and that should allow similar executable code to be generated.

The theory Imperative HOL [START_REF] Bulwahn | Imperative Functional Programming with Isabelle/HOL[END_REF] discussed in Section 7 already implements such a monad, however our development started independently of it and we have then used it to improve our version, without code generation for the moment.

The State Transformer Monad

In this section we define the state-reader and state-transformer monads and a syntax seamlessly mixing them. We encapsulate them in the SR -respectively ST -datatypes, as functions from a state to a return value -respectively a pair of return value and state.

We can escape from these datatypes with the runSR -respectively runST and evalST -functions which are intended to be used only in logical parts (theorems and proofs) and that should not be extractible.

datatype ( ′ a, ′ s) SR = SR ′ s ⇒ ′ a datatype ( ′ a, ′ s) ST = ST ′ s ⇒ ′ a × ′ s primrec runSR :: ( ′ a, ′ s) SR ⇒ ′ s ⇒ ′ a where runSR (SR m) = m primrec runST :: ( ′ a, ′ s) ST ⇒ ′ s ⇒ ′ a × ′ s where runST (ST m) = m abbreviation evalST where evalST fm s == fst (runST fm s)
The return (also called unit) and bind functions for manipulating the monads are then defined classically with the infix notations SR and ST for bind s. We add also the function SRtoST translating state-reader monads to statetransformer monads and the function thenST (with infix notation ⊲ ST ) abbreviating binding without value transfer.

consts returnSR :: ′ a ⇒ ( ′ a, ′ s) SR returnST :: ′ a ⇒ ( ′ a, ′ s) ST bindSR :: ( ′ a, ′ s) SR ⇒ ( ′ a ⇒ ( ′ b, ′ s) SR) ⇒ ( ′ b, ′ s) SR (infixr SR ) bindST :: ( ′ a, ′ s) ST ⇒ ( ′ a ⇒ ( ′ b, ′ s) ST ) ⇒ ( ′ b, ′ s) ST (infixr ST ) SRtoST :: ( ′ a, ′ s) SR ⇒ ( ′ a, ′ s) ST
We define also syntax translations to use the Haskell-like do-notation. The principal difference between the Haskell do-notation and this one is the use of state-readers for which order does not matter. With some syntax transformations, we can simply compose several state readers into one as well as give them as arguments to state writers, almost as it is done in imperative languages (for which state is the heap). In an adapted contexti. e. in doSR{. . . } or doST {. . . } -we can so use state readers in place of expressions by simply putting them in . . . , the current state being automatically provided to them, only thanks to the syntax transformation which propagates the same state to all . . . . We also add syntax for let (letST

x = a SR ; b ST ) and if (if (a SR ) {b ST } else {c ST }). For example with f ′ a ⇒ ( ′ b, ′ s) ST , a ( ′ a, ′ s) SR , g ((), ′ s) ST and h ′ b ⇒ ′ d
, all these expressions are equivalent:

-doST { x ← f a ; g; returnST (h x )} -doST { va ← SRtoST a; x ← f va; g; returnST (h x )} -ST λs. runST (f (runSR a s)) s (λx . g ⊲ returnST (h x ))
We finally define the whileST combinator ([v = v0 ] while (c) {a}), inspired from the while combinator definition of the Isabelle/HOL library, the only difference with it being the encapsulation in monads:

whileST b c v = (doST {if ( b v ){v ′ ← c v ; whileST b c v ′ }else{returnST v }}) while b c v = (if b v then while b c (c v ) else v )

The Heap Transformer Monad

We define a heap we will use as the state in the state-reader/transformer monads. We represent it by an extensible record containing a field for the values.

As the Schorr-Waite algorithm doesn't need allocation of new references, our heap simply is a total function from references to values. (We use a record here because of developments already under way and needing further components.)

record ( ′ n, ′ v ) heap = heap :: ′ n ⇒ ′ v
We assume that we have a data type of references, which can either be Null or point to a defined location:

datatype ′ n ref = Ref ′ n | Null
To read and write the heap, we define the corresponding primitives read and write. To access directly to the fields of structures in the heap, we also add the get (a•b), rget (r → b) and rupdate (r → b := v ) operators, taking an access-and-update function (b) as argument.

In this section, we provide a low-level representation of trees as structures connected by pointers that are manipulated by an imperative program. This is the typical representation in programming languages like C, and it is also used in most correctness proofs of SW.

Data Structures

These structures are either empty (corresponding to a leaf with a null pointer, as we will see later) or nodes with references to the left and right subtree:

datatype ( ′ a, ′ r ) struct = EmptyS | Struct ′ a ( ′ r ref ) ( ′ r ref )
We define then access-and-update functions $v (value) $l (left) and $r (right) for the ( ′ a, ′ r ) struct datatype, and access-and-update functions $mark, $dir and $val for the ′ a tag datatype.

Traditionally, in language semantics, the memory is divided into a heap and a stack, where the latter contains the variables. In our particular case, we choose a greatly simplified representation, because we just have to accommodate the variables pointing to the trees p and t. Our heap will be a type abbreviation for heaps whose values are structures:

types ( ′ r , ′ a) str-heap = ( ′ r , ( ′ a, ′ r ) struct) heap

An Imperative Algorithm

We now have an idea of the low-level memory representation of trees and can start devising an imperative program that manipulates them (as we will see, with a similar outcome as the high-level program of Section 2). The program is a while loop, written in monadic style, that has as one main ingredient a termination condition:

constdefs sw-impl-term :: ( ′ r ref × ′ r ref ) ⇒ (bool , ( ′ r , ′ v tag) str-heap) SR sw-impl-term vs == doSR { (case vs of (ref-p, ref-t) ⇒ (case ref-p of Null ⇒ (case ref-t of Null ⇒ True | t ⇒ (( read t •$v )•$mark ) ) | -⇒ False))}
The second main ingredient of the while loop is its body:

constdefs sw-impl-body :: ( ′ r ref × ′ r ref ) ⇒ ( ′ r ref × ′ r ref , ( ′ r , ′ v tag) str-heap) ST sw-impl-body vs == (case vs of (p, t) ⇒ doST { if (case t of Null ⇒ True | -⇒ ( read t •$v )•$mark ) { (if ( p → ($v oo $dir ) = L) { ( * * swing * * ) letST rt = p → $r ; p → $r := p → $l ; p → $l := t; p → ($v oo $dir ) := R; returnST (p, rt) } else { ( * * pop * * ) letST rp = p → $r ; p → $r := t; returnST (rp, p) }) } else { ( * * push * * ) letST rt = t → $l ; t → $l := p; t → ($v oo $mark ) := True; t → ($v oo $dir ) := L; returnST (t, rt) } })
The termination condition and loop body are combined in the following imperative program:

constdefs sw-impl-tr :: ( ′ r ref × ′ r ref ) ⇒ ( ′ r ref × ′ r ref , ( ′ r , ′ v tag) str-heap) ST
where sw-impl-tr pt == (doST {[vs = pt] while (¬ sw-impl-term vs ) {sw-impl-body vs}})

Correctness

Before we can describe the implementation of inductively defined trees in low-level memory, let us note that we need to have a means of expressing which node of a tree is mapped to which memory location. For this, we need trees adorned with address information:

datatype ( ′ r , ′ v ) addr = Addr ′ r ′ v
For later use, we also introduce some projections (cf. definition of tag in Section 2) : We can now turn to characterizing the implementation relation of trees in memory, which we define gradually, starting with a relation which expresses that a (non-empty) node n with subtrees l and r is represented in state s. Remember that node n contains its address in memory. It is not possible that the structure at this address is empty. We therefore find a structure with a field corresponding to the value of n (just remove the address, which is not represented in the structure) and left and right pointers to the l and r subtrees:

primrec val-proj-of-tag :: ( ′ r , ′ v ) addr tag ⇒ ′ v tag where val-proj-of-tag (Tag m d av ) = (case av of (Addr ref v ) ⇒ (Tag m d v ))
constdefs struct-alloc-in-state ::

( ′ t ⇒ ′ r ref ) ⇒ ( ′ r , ′ v ) addr tag ⇒ ′ t ⇒ ′ t ⇒ ( ′ r , ′ v tag) str-heap ⇒ bool struct-alloc-in-state ac n l r s == (case (heap s (addr-of-tag n)) of EmptyS ⇒ False | Struct ns ref-l ref-r ⇒ ns = val-proj-of-tag n ∧ ref-l = ac l ∧ ref-r = ac r )
Please ignore the projection parameter ac for the moment. We will instantiate it with different functions, depending on whether we are working on trees (this section) or on graphs (in Section 6).

Given the representation of a node in memory, we can define the representation of a tree t in a state s: Just traverse the tree recursively and check that each node is correctly represented (tree-alloc-in-state ac t s). Finally, a configuration (the p and t trees) is correctly represented (config-alloc-in-state (p, t)) if each of the trees is, and the p variable contains a reference to the p tree, and similarly for t.

Let us now present the first intended instantiation of the ac parameter appearing in the above definitions: It is a function that returns the address of a non-empty node, and always Null for a leaf:

primrec addr-of :: (( ′ r , ′ v ) addr tag, ′ b) tree ⇒ ′ r ref where addr-of (Leaf rf ) = Null | addr-of (Node n l r ) = Ref (addr-of-tag n)
We can now state our first result: for a couple of p and t trees correctly allocated in a state s, the low-level and high-level algorithms have the same termination behaviour:

lemma sw-impl-term-sw-term: config-alloc-in-state addr-of pt (ref-pt, s) =⇒ runSR (sw-impl-term ref-pt) s = sw-term pt
Before discussing the correctness proof, let us remark that the references occurring in the trees have to be unique. Otherwise, the representation of a tree in memory might not be a tree any more, but might contain loops or joint subtrees. Given the list reach of references occurring in a tree, we will in the following require the p and t trees to have disjoint ("distinct") reference lists.

The correctness argument of the imperative algorithm is now given in the form of a simulation theorem: A computation with sw-tr carried out on trees p and t and producing trees p ′ and t ′ can be simulated by a computation with sw-impl-tr starting in a state implementing p and t, and ending in a state implementing p ′ and t ′ . We will not go into details here (please refer to the long version of the paper [START_REF] Giorgino | Verification of the Schorr-Waite algorithm -From trees to graphs[END_REF]), since the correctness argument for trees is just a light-weight version of the argument for graphs in Section 5.

Schorr-Waite on Trees with Pointers

The Schorr-Waite algorithm has originally been conceived for genuine graphs, and not for trees. We will now add "pointers" to our trees to obtain a representation of a graph as a spanning tree with additional pointers. This is readily done, by instantiating the type variables of the leaves to the type of references. Thus, a leaf can now represent a null pointer (Leaf Null ), or a reference to r, of the form Leaf (Ref r ).

For example, the graph of Figure 4 could be represented by the following tree, with references of type nat:

Node (Tag False L (Addr 1 ())) (Node (Tag False L (Addr 2 ())) (Leaf Null ) (Leaf Null )) (Node (Tag False L (Addr 3 ())) (Leaf (Ref 2 )) (Leaf Null ))
A given graph might be represented by different spanning trees with additional pointers, but the choice is not indifferent: it is important that the graph is represented by a spanning tree that has an appropriate form, so that the low-level algorithm of Section 4 starts backtracking at the right moment. To characterize this form and to get an intuition for the simulation proof presented in Section 6, let's take a look at a "good" (Figure 2) and a "bad" spanning tree (Figure 3). In Figure 2, the decisive step occurs when p points to node 3. Since the highlevel algorithm proceeds structurally, it does not follow the additional pointer. Its t tree will therefore be a leaf, and the algorithm will start backtracking at this moment. The low-level representation does not distinguish between pointers to subtrees and additional pointers in leaf nodes, so that the t pointer will follow the link to node 4, just to discover that this node is already marked. For this reason, also the low-level algorithm will start backtracking. The situation is different in Figure 3, when p reaches node 2. The high-level algorithm finishes its recursive descent at this point and starts backtracking, leaving node 4 unmarked. However, the low-level version proceeds to node 4 with its t pointer, marks it and starts exploring its subtrees. At this point, the high-level and low-level versions of the algorithm start diverging irrecoverably.

What then, more generally, is a "good" spanning tree? It is one where all additional pointers reference nodes that have already been visited before, in a pre-order traversal of the tree. This way, we can be sure that by following such an additional pointer, the low-level algorithm discovers a marked node and returns. We formalize this property by a predicate that traverses a tree recursively and checks that additional pointers only point to a set of allowed external references extrefs. When descending into the left subtree, we add the root to this set, and when descending into the right subtree, the root and the nodes of the left subtree.

primrec t-marked-ext :: (( ′ r , ′ v ) addr tag, ′ r ref ) tree ⇒ ′ r set ⇒ bool where t-marked-ext (Leaf rf ) extrefs = (case rf of Null ⇒ True | Ref r ⇒ r ∈ extrefs) | t-marked-ext (Node n l r ) extrefs = (t-marked-ext l (insert (addr-of-tag n) extrefs) ∧ t-marked-ext r ((insert (addr-of-tag n) extrefs) ∪ set (reach l )))
There is a similar property p-marked-ext, less inspiring, for p trees, which we do not give here. It uses in particular the function reach-visited giving the list of addresses of nodes that should have been visited. Let us insist on one point, because it is essential for the method advocated in this paper: Intuitively, we partition the state space into disjoint areas of addresses with their spanning trees, as depicted in Figure 5. The properties of these areas are described by the predicates t-marked-ext and p-marked-ext. Pointers may reach from one area into another area (the extrefs of the predicates). For the proof, it will be necessary to identify characteristic properties of these external references.

One of these is that all external references of a t tree only point to nodes marked as true. To prepare the ground, the following function gives us all the references of nodes that have a given mark, using the projection nmark for retrieving the mark from a tag: We can now show some invariants of function sw-body that will be instrumental for the correctness proof of Section 6. For example, if all external references of t only point to marked nodes of p, then this will also be the case after execution of sw-body: To conclude this section, let us remark that the refinement of trees by instantiation of the leaf node type described here allows us to state some more invariants, but of course, the correctness properties of the original algorithm of Section 2 remain valid.

Implementation for Trees with Pointers

More surprisingly, we will now see that the low-level traversal algorithm of Section 4 also works for all graphs -without the slightest modification of the algorithm! The main justification has already been given in the previous section: There is essentially only one situation when the "pure tree" version and the "tree with pointers" version of the algorithm differ:

-In the high-level "pure tree" version, after a sequence of push operations, the t tree will become a leaf. This will be the case exactly when in the low-level version of the algorithm, the corresponding t pointer will become Null. -In the high-level "tree with pointers" version, after some while, the t tree will also become a leaf, but in the low-level version, the t pointer might have moved on to a non-Null node. If the underlying spanning tree is well-formed (in the sense of t-marked-ext), the t will point to a marked node, so that the algorithm initiates backtracking in both cases.

We achieve this by taking into account the information contained in leaf nodes. Instead of the function addr-of of Section 4, we now parametrize our development with the function addr-or-ptr that also returns the references contained in leaf nodes: We can now prove an extension of the lemma sw-impl-term-sw-term of Section 4 establishing the correspondence of the high-level and low-level termination conditions described above.

The proof for the simulation lemma now proceeds essentially along the same lines as before. Now, the proof proceeds along the lines of the proof discussed in Section 4, yielding finally a preservation theorem for configurations: If we start our computation with an empty p tree, some of the preconditions of this lemma vanish, as seen by a simple expansion of definitions. A tidier version of our result is then:

theorem impl-correct-tidied : [[ t-

Related Work

A considerable amount of work has accumulated on the Schorr-Waite algorithm in particular and on the verification of pointer algorithms in general. For reasons of space, we have to defer a detailed discussion to the full version [START_REF] Giorgino | Verification of the Schorr-Waite algorithm -From trees to graphs[END_REF], which also contains some references we cannot accommodate here. Schorr-Waite: Since its publication [START_REF] Schorr | An efficient machine independent procedure for garbage collection in various list structures[END_REF], the algorithm has given rise to numerous publications which, in the early days, were usually paper proofs which often followed a transformational approach to derive an executable program. There are recently some fully automated methods that, however, are incomplete or cover only very specific correctness properties. Of more interest to us are proofs using interactive theorem provers, sparked by Bornat's proof using his Jape prover [START_REF] Bornat | Proving pointer programs in Hoare logic[END_REF]. This work has later been shortened considerably in Isabelle [START_REF] Mehta | Proving pointer programs in higher-order logic[END_REF], using a "split heap" representation. Similar in spirit are proofs using the Caduceus platform [START_REF] Hubert | A case study of C source code verification: the Schorr-Waite algorithm[END_REF] and the KeY system [START_REF] Bubel | The Schorr-Waite-Algorithm[END_REF]. A proof with the B method [START_REF] Abrial | Event based sequential program development: Application to constructing a pointer program[END_REF] follows the refinement tradition of program development.

Verification of imperative programs with proof assistants: There are two ways to obtain verified executable code: verify written code by abstracting it or generate it from abstract specification.

Haskabelle [START_REF] Rittweiler | Haskabelle -converting Haskell source files to Isabelle/HOL theories[END_REF] allows to import Haskell code into Isabelle, which can then be used as specification, implementation or intermediate refinement like in [START_REF] Klein | Experience report: sel4formally verifying a high-performance microkernel[END_REF]. Why/Krakatoa [START_REF] Filliâtre | The Why/Krakatoa/Caduceus platform for deductive program verification[END_REF] is a general framework to generate proof obligations from annotated imperative programs like Java or C into proof assistants like Coq, PVS or Isabelle.

As to the second way, the Isabelle extractor generates SML, Caml, Haskell code from executable specifications. The theory Imperative HOL [START_REF] Bulwahn | Imperative Functional Programming with Isabelle/HOL[END_REF] takes advantage of this and already implements a state-transformer monad with syntax transformations, and code extraction/generation.

We used a simple memory model as a total function from natural numbers to values which was sufficient in our case, but managing allocation could become hard. [START_REF] Schirmer | State spaces -the locale way[END_REF] compares several memory models and then presents a synthesis enjoying their respective advantages, which could be interesting for our work. Our state space partitioning bears similarities with methods advocated in Separation logic [START_REF] Peter | Local reasoning about programs that alter data structures[END_REF] -details of this connection still have to be explored.

Conclusions

We have presented a correctness proof of the Schorr-Waite algorithm, starting from a high-level algorithm operating on inductively defined trees, to which we add pointers to obtain genuine graphs. The low-level algorithm, written in monadic style, has been proved correct using a refinement relation with the aid of a simulation argument.

The Isabelle proof script is about 1000 lines long and thus compares favorably with previous mechanized proofs of Schorr-Waite, in particular in view of the fact that the termination of the algorithm and structure preservation of the graph after marking have been addressed. It is written in a plain style without particular acrobatics. It favours readability over compactness and can presumably be adapted to similar proof assistants without great effort.

The aim of the present paper is to advocate a development style starting from high level, inductively defined structures and proceeding by refinement. There might be other approaches of verifying low-level heap manipulating algorithms (iterating, for example, over the number of objects stored in the heap and thus not exploiting structural properties). However, we hope to develop patterns that make refinement proofs easier and to partly automate them, thus further decreasing the proof effort.

We think that some essential concepts of our approach (representation of a graph by spanning trees with additional pointers, refinement to imperative programs in monadic style, partitioning of the heap space into subgraphs) can be adapted to other traditional graph algorithms: Often, the underlying structure of interest is indeed tree-shaped, whereas pointers are just used for optimization. In this spirit, we have verified a BDD construction algorithm [START_REF] Giorgino | Verification of BDD algorithms by refinement of trees[END_REF] and we are planning to apply similar techniques in the context of Model Driven Engineering. Of course, we do not claim that our approach is universally applicable for graphs without deeper structure.

Fig. 1 .

 1 Fig. 1. Operations of the Schorr-Waite algorithm.

  primrec addr-of-tag :: ( ′ r , ′ v ) addr tag ⇒ ′ r where addr-of-tag (Tag m d av ) = (case av of (Addr ref v ) ⇒ ref ) primrec val-of-tag :: ( ′ r , ′ v ) addr tag ⇒ ′ v where val-of-tag (Tag m d av ) = (case av of (Addr ref v ) ⇒ v )

Fig. 2 .

 2 Fig.2. Low-level graph with a "good" spanning tree

Fig. 3 .

 3 Fig. 3. The same graph with a bad spanning tree

1 2 3 Fig. 4 .Fig. 5 .

 1345 Fig. 4. A tree with additional pointers (drawn as dashed lines)

  primrec marked-as-in :: bool ⇒ (( ′ r , ′ v ) addr tag, ′ l ) tree ⇒ ′ r set where marked-as-in m (Leaf rf ) = {} | marked-as-in m (Node n l r ) = (if (nmark n) = m then {addr-of-tag n} else {}) ∪ marked-as-in m l ∪ marked-as-in m r

  primrec addr-or-ptr ::(( ′ r , ′ v ) addr tag, ′ r ref ) tree ⇒ ′ r ref where addr-or-ptr (Leaf rf ) = rf | addr-or-ptr (Node n l r ) = Ref (addr-of-tag n)

The present paper is primarily a case study, so there are still some rough edges: the representation of our imperative programs has to be refined, with the aim of allowing their compilation to standard programming languages like C or Java.


Eugen Barbu
email: eugen.barbu@univ-rouen.fr

Pierre Héroux

Sébastien Adam

Eric Trupin

Clustering of Document Images using Graph Summaries

published or not. The documents may come

L'archive ouverte

Introduction

A document image analysis (DIA) system transforms a document image into a description of the set of objects that constitutes the information on the document and which are in a format that can be further processed and interpreted by a computer [START_REF] Antonacopoulos | Introduction to Document Image Analysis[END_REF]. Documents can be classified in mostly graphical or mostly textual documents [START_REF] Nagy | Twenty years of document analysis in PAMI[END_REF]. The mostly textual documents also known as structured documents respect a certain layout and powerful relations exist between components. Examples of such documents are technical papers, simple text, newspapers, program, listing, forms,… Mostly graphical documents do not have strong layout restrictions but usually relations exist between different document parts. Examples of this type of documents are maps, electronic schemas, architectural plans... For these two categories of documents, graph based representations can be used to describe the image content (e.g. region adjacency graph [START_REF] Pavlidis | Algorithms or Graphics and Image Processing[END_REF] for graphical and Voronoi-based neighborhood graph [START_REF] Bagdanov | Fine-grained Document Genre Classification Using First Order Random Graphs[END_REF] for textual document images).

In this paper we present an approach similar to the "bag of words" method used in Information Retrieval (IR) field. We describe a document using a bag of symbols found automatically using graph mining [START_REF] Washio | State of the art of graph-based data mining[END_REF] techniques. In other words, we consider the frequent subgraphs of a graph-based document representation as "symbols" and we investigate whether the description of a document as a bag of "symbols" can be profitably used in a classification task.

The approach has the ability to process document images without knowledge of, or models for, document content. In the literature one can find papers dealing with representations of textual documents using frequent items [START_REF] Fung | Hierarchical Document Clustering Using Frequent Itemsets[END_REF] and description of XML documents using frequent trees [START_REF] Termier | Mining XML Data with Frequent Trees[END_REF] but we do not know of any similar approaches in the DIA field.

The motivation for our study is the fact that unsupervised classification can represent the starting point for semi-supervised classification or indexation and retrieval from document collections. Also, the existing clustering solutions for document images are usually domain dependent and can not be used in an "incoming document flux" (fax, business mail,…) setting, where supervised techniques are not at hand.

The outline of this paper is as follows. In section 2 we present a graph representation and how we create this representation from a document image. Section 3 presents the graph-mining method used, in section 4 we describe how we create clusters based on dissimilarities between bags of symbols. Section 5 presents some experimental results. We conclude the paper and outline perspectives in section 6.

Document Graph Based Representations

Eight levels of representation in document images are proposed in [START_REF] Blostein | Document Representations[END_REF]. These levels are ordered in accordance with their aggregation relations. Data array level, primitive, lexical, primitive region, functional region, page, document, and corpus level are the representation levels proposed.

Without loosing generality, in the following paragraphs we focus our attention on a graph-based representation build from the primitive level. The primitive level contains objects such as connected components (sets of adjacent pixels with the same color) and the relations between them.

Let I be an image and C(I) the connected components from I, if

) (I C c∈ , c is described as ) , ( P id c=
, where id is a unique identifier and P the set of pixels the component contains. Based on this set P, we can compute the center for the connected component bounding box and also we can associate a feature vector to it. Based on that,

n R v v y x id c ∈ =
), , , , ( . Subsequently using a clustering procedure on the feature vectors we can label the connected component and reach the description The exact methodology employed to construct the graph representation is subsequently presented. From a binary document image we extract connected components (black and white). The connected components will be the graph nodes. For each connected component we extract features. In the actual implementation the extracted characteristics are rotation and translation invariant features based on Zernike moments [START_REF] Khotazad | Invariant Image recognition by Zernike Moments[END_REF]. The invariants represent the magnitudes of a set of orthogonal complex moments of a normalized image.

The following step is to associate each connected component a label.

Labeling Connected Components

The two main categories of clustering methods are partitional and hierarchical.

Partitional methods can deal with large sets of objects ("small" in this context means less than 300) but needs the expected number of clusters in input. Hierarchical methods can overcome the problem of number of clusters by using a stopping criterion [START_REF] Gordon | Classification 2ndEdition[END_REF] but are not applicable on large sets due to their time and memory consumption.

In our case the number of connected components that are to be labeled can be larger than the limit of applicability for hierarchical clustering methods. In the same time we cannot use a partitional method because we do not know the expected number of clusters. Based on the hypothesis that a "small" sample can be informative for the geometry of data, we obtain in a first step an estimation for the number of clusters in data. This estimation is made using an ascendant clustering algorithm with a stopping criterion. The number of clusters found in the sample is used as input for a partitional algorithm applied on all data.

We tested this "number of cluster estimation" approach using a hierarchical ascendant clustering algorithm [START_REF] Gordon | Classification 2ndEdition[END_REF] that uses Euclidean distance to compute the dissimilarity matrix, complete-linkage to compute between-clusters distances, and Calinsky-Harabasz index [START_REF] Milligan | An Examination of Procedures for Determining the Number of Clusters in a Data Set[END_REF] as a stopping criterion. The datasets ( Considering S the sample extracted at random from a test set, in Table 2 we present predicted cluster numbers obtained for different sample sizes. After repeating the sampling procedure for 10 times if the test set is for example |S|=50, we obtain a set of estimations for the number of clusters. We can see that by using a majority voting decision rule we can find the good number of clusters in most of the cases and even when the sample size is very small (50 or 100) compared to the data set size. We employed our sampling approach combined with the k-medoids clustering algorithm [START_REF] Kaufmann | Clustering by means of medoids[END_REF] on the connected components data set from images in our corpus (see section 5). The k-medoids clustering algorithm is a more robust version of the well known k-means algorithm. The images from our corpus contain 6730 connected components. The proposed number of clusters using ten samples of size 600 is [START_REF] Ballard | Computer Vision[END_REF][START_REF] Seno | A Pattern Finding Toolkit[END_REF]17,[START_REF] Ballard | Computer Vision[END_REF][START_REF] Ballard | Computer Vision[END_REF]19,[START_REF] Termier | Mining XML Data with Frequent Trees[END_REF]17,[START_REF] Dumais | Improving the retrieval information from external resources[END_REF][START_REF] Ballard | Computer Vision[END_REF] and by considering the majority we use 16 clusters as input to the partitional clustering algorithm.

After labeling the connected components (nodes in the graph) subsequently we describe the way we add edges to the graph. The edges can be labeled or not (if unlabeled the significance is Boolean: we have or have not a relation between two connected components) and can be relations of spatial proximity, based on "forces" [START_REF] Tabbone | Matching of graphical symbols in line-drawing images using angular signature information[END_REF], orientation or another criterion. In our actual implementation the distance between centers of connected components is used (see Fig. 1). If the distance between two connected components centers is smaller than a threshold, then an edge will link the two components (nodes).

Graph Mining

The main objective of graph mining is to provide new principles and efficient algorithms to mine topological substructures embedded in graph data" [START_REF] Washio | State of the art of graph-based data mining[END_REF].

Mining frequent patterns in a set of transaction graphs is the problem of finding in this set of graphs those subgraphs that occur more times in the transactions than a threshold (minimum support). Because the number of patterns can be exponential this problem complexity can also be exponential. An approach to solve this problem is to start with finding all frequent patterns with one element, then all patterns with two elements, etc in a level-by-level setting. In order to reduce the complexity different constraints are used: the minimum support, the subgraphs are connected, and not overlapped. An important concept is that of maximal subgraph. A graph is said to be maximal if it does not have a frequent super-graph. In our document image analysis context we are interested in finding maximal frequent subgraphs because we want to find symbols but to ignore their parts.

A system that is used to find frequent patterns in graphs is FSG (Frequent Subgraph Discovery) that "finds patterns corresponding to connected undirected subgraphs in an undirected graph database" [START_REF] Seno | A Pattern Finding Toolkit[END_REF]. The input for the FSG program is a list of graphs and a minimum support threshold. Each graph represents a transaction. We present subsequently how we construct the transaction list starting from a set of document images. Using the procedure presented in section 2 we create for each document an undirected labeled graph. Every connected component of this graph represents a transaction. Using FSG we extract the frequent subgraphs and we construct a bag of frequent subgraphs occurring in each document.

Fig. 2. Frequent subgraph and its occurences in an image

In the following paragraphs we consider that the frequency condition is sufficient for a group of connected components to form a symbol and we will conventionally make an equivalence between the frequent subgraphs found and symbols. As we can see in the example (Fig. 2) the proposed symbols are far from being perfect due to the image noise, connected components clustering procedure imperfections, … however we can notice the correlation between this artificial symbol and the domain symbols.

Documents Description

A document can be seen as a bag of symbols ) ,..., , , . We can use this representation as it is but we can also apply a weightening schema on it in order to distinguish between symbols with different discriminative power.

A collection of documents is represented by a symbol-by-document matrix A, where each entry represents the occurrences of a symbol in a document image, A= ) ( ik a , where ik a is the weight of symbol i in document k. Let ik f be the number of occurrences of symbol i in document k, N the number of documents in the collection, and i n the total number of times symbol i occurs in the whole collection.

In this setting conform with [START_REF] Dumais | Improving the retrieval information from external resources[END_REF] one of the most effective weighting scheme is entropy-weighting. The weight for symbol i in document k is given by :

) )

= + + = N j ij i ij ik ik ni f n f N f a log( ) log( 1 1 ( * ) 1 log( 1 ∑
Now, considering two documents A, B with the associated weights ) ,..., , ( ), ,..., , (

Experimental Results

A comparison between results obtained using the proposed document representation and three other representations is made in the following paragraphs. On a corpus of graphical document images we have extracted different sets of features. Each document image is described with one of the following types of features : Zernike moments for the whole image (a vector with 16 components) abbreviated as ZM in Table 3, pixel densities (the feature vector considered is composed of the 85 (1+4+16+64) gray levels of a 4-level-resolution pyramid [START_REF] Ballard | Computer Vision[END_REF] , see Fig 3 .),(QT), weighted connected components label list , and symbol label list . Our corpus contains 30 images from the class of a French telephony operator (FT) maps, 25 electronic schemas, and 5 architectural plans.

Fig. 4. Corpus images

This images are scanned images that contains real and artificial noise. We can see that the connected component list approach obtains good results compared with the simple approaches (Zernike moments and densities). In the same time the symbols list approach representation is more compact than the connected components list and obtains better results.

Conclusions

The research undertaken represents a novel approach for clustering document images. The approach uses data mining tools for knowledge extraction. It automatically finds frequent symbols. These frequent patterns are part of the document model and can be put in relation with the domain knowledge. The exposed method can be applied to other graph representations of a document. In the near future, we will apply this approach to layout structures of textual document images.

Another follow up activity is to quantify the way noise can affect the connected components labeling, and the manner in which the inexact number of clusters can affect the graph mining procedure. Based on this error propagation study we can ameliorate our method.

Other possible improvements can be obtained if we would employ a graph-based technique that can deal with error tolerant graph matching.

.

  l is a nominal label . The graph G(I) representing the image is Vertices V(I) correspond to connected components and are labeled with component labels. An edge between vertex u and vertex w exists iff t is a threshold that depends on the image I global characteristics (size, number of connected components,…).

Fig. 1 .

 1 Fig. 1. Image and its associated graph

  measure based on the cosine correlation.

Fig. 3 .

 3 Fig. 3. Four level resolution pyramid

Table 1 )

 1 are synthetically generated and contain well separated (not necessarly convex) clusters.

Table 1 .

 1 Data sets description

	T	|T|	no. of clusters
	T1	24830	5
	T2	32882	15
	T3	37346	24

Table 2 .

 2 Proposed number of clusters

	T \ |S|	50	100	300		500	600	700
	T1	[6, 8, 7, 6, 5, 6, 6, 6, 5, 5]	[5, 7, 9, 7, 5, 5, 7, 5, 5, 7]	[7, 5, 7, 8, 7, 5, 5, 5, 7, 7]	[8, 7, 5, 5, 5, 5, 5, 5, 5, 5]	[5, 5, 5, 5, 5, 7, 7, 7, 7, 5]	[5, 5, 7, 5, 7, 5, 5, 7, 5, 5]
		6	5	7		5	5	5
	T2	[9, 15, 15, 14, 13, 15,	[15, 15, 13, 15, 15, 15,	[15, 15, 15, 15, 15, 15,	[15, 15, 15, 15, 15, 15,	[15, 15, 15, 15, 15, 15,	[15, 15, 15, 15, 15, 15,
		13, 13, 14,	15, 15, 15,	15, 15, 15,	15, 15, 15,	15, 15, 15,	15, 15, 14,
		15]	15]	14]		15]	15]	15]
		15	15	15		15	15	15
	T3	[11, 7, 9, 18, 7, 7, 6, 4,	[6, 14, 23, 21, 7, 17,	[22, 24, 23, 19, 23, 24,	[21, 25, 25, 24, 22, 24,	[20, 25, 21, 24, 19, 23,	[23, 20, 21, 20, 25, 24,
		14, 8]	23, 16, 12,	24,	21,	23, 24, 24,	24, 25, 24,	24, 21, 25,
			11]	21,24,] 24]	24]	22]	24]
		7	23	24		24	24	24

Table 3 .

 3 Results on our corpus

		ZM		Densities	Connected		Symbols
						Components list	list
	F-measure	0.58		0.69		0.89			0.90
		1	29	30	0	26	4	0	26	4	0
	Confusion	0	25	25	0	2	1	22	0	3	22
	matrix	0	5	0	5	0	5	0	0	5	0

Table 4 .

 4 How to read the confusion matrix

	Cluster 1	Cluster 2
	1	29	FT maps
	0	25	Electronic
			schemas
	0	5	Architectural
			drawings