Sophie Bernard
email: sophie.bernard@inria.fr

Formalization of the Lindemann-Weierstrass Theorem

Keywords: Coq, Formal proofs, Multivariate polynomials, Polynomial conjugates, Transcendance

This article details a formalization in Coq of the Lindemann-Weierstrass theorem which gives a transcendence criterion for complex numbers: this theorem establishes a link between the linear independence of a set of algebraic numbers and the algebraic independence of the exponentials of these numbers. As we follow Baker's proof, we discuss the difficulties of its formalization and explain how we resolved them in Coq. Most of these difficulties revolve around multivariate polynomials and their relationship with the conjugates of a univariate polynomial. Their study ultimately leads to alternative forms of the fundamental theorem of symmetric polynomials. This formalization uses mainly the Mathcomp library for the part relying on algebra, and the Coquelicot library and the Coq standard library of real numbers for the calculus part.

Introduction

Natural, integer, rational, real, complex . . . We are so used to this classification of numbers that we tend to forget it is not the only one. After all, integers are only the solutions of simple additive equations in IN, and rationals are the solutions of the simple multiplicative ones in Z Z. The next move would normally be to mix them both in Q. We then obtain the algebraic numbers: the set of all the roots of polynomials whose coefficients lie in Q.

The Lindemann-Weierstrass theorem gives a criterion to recognize transcendental numbers, that is non-algebraic numbers. More precisely, it explains that a set of exponentials of algebraic numbers which respect certain conditions can never verify some polynomial equation. The usual statement gives a result which links linear independence of these algebraic numbers and the algebraic independences of their exponentials, both over Q. This kind of criterion was pretty new at the time: only in 1844 has Liouville [START_REF] Liouville | Sur des classes très-étendues de quantités dont la valeur n'est ni algébrique, ni même réductible à des irrationnelles algébriques[END_REF] shown that there exist transcendental numbers, by explicitly exhibiting one. In the next few years, Hermite [START_REF] Hermite | Sur la fonction exponentielle[END_REF] used a special function to show that e is also transcendental. This same function led to the transcendance of π by Lindemann, and its generalization, an earlier version of the theorem we formalized [START_REF] Lindemann | Über die zahl π[END_REF]. The work of Weierstrass eventually resulted in the Lindemann-Weierstrass theorem in its usual form [START_REF] Weierstrass | Zu Lindemann's Abhandlung: " Über die Ludolph'sche Zahl[END_REF].

Later on, Gelfond and Schneider worked independently of some generalizations, which gave results on linear forms of complex logarithms, opening the door for many applications: diophantine equations, elliptic curves, cryptography, . . . In this paper, we formalized, in Coq, one of the many proofs that exist. To our knowledge, it is the first formalization of this theorem in any formal proof assistant. We were given different choices for the proof, the main ones were the following:

-Hermite, Lindemann and Weierstrass: it has the advantage of explaining exactly why a certain function is introduced. -Baker: it uses the same steps as the previous one, except that it goes straight for the result. -Lang: a less elementary proof relying on field extensions and Galois theory [START_REF] Lang | Algebra revised third edition[END_REF].

Lang's proof could be interesting to formally prove but the goal here was to continue the previous work on multivariate polynomials [START_REF] Bernard | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials[END_REF] and give a small interface for the study of polynomial roots. That's why Baker's proof was chosen. It can be found in Baker's book [START_REF] Baker | Transcendental number theory[END_REF].

In this paper, we will dedicate Sect. 2 to the first part of the proof: it will serve as an overview of the useful libraries and the proof, as well as introducing the theorem statement. Then, in Sect. 3, we will follow the different parts of Baker's proof. For each part, we will explain the ideas of the mathematical proof, its difficulties and how we resolved them by formalizing several notions such as the conjugates roots of a polynomial or a special kind of symmetric polynomials. Finally, we compare our solution to related work, and present what could be the next step (Sect. 4).

All the files of this formalization can be found on [START_REF]Formalization of the Lindemann-Weierstrass theorem in Coq[END_REF], they are relying on Coq 8.5 [START_REF]Coq development team: The Coq proof assistant[END_REF], coquelicot 2.1.2, and development versions of mathcomp 1.6.1, multinomials, and finmap [START_REF] Cohen | Finmap library[END_REF].

Context

In this section, we will formally define the already introduced terms, motivate our choice of libraries in order to be able to give the Coq statement of the Lindemann-Weierstrass theorem.

Mathematical Context

Firstly, we say a finite set of numbers A = {a 1 , . . . , a n } is linearly independent over Q when a rational linear combination of A is null only if the coefficients are all zero.

∀(q 1 , . . . , q n ) ∈ Q n , q 1 a 1 + • • • + q n a n = 0 =⇒ ∀i ∈ {1, . . . , n}, q i = 0 . (1)
The same way a polynomial over a commutative ring IK is the linear combination of coefficients in IK and exponents of the indeterminate, a multivariate polynomial over a commutative ring IK is a linear combination of coefficients in IK and monomials which are products of indeterminates. Usually, there are no more than 3 indeterminates, they are written X, Y and Z, otherwise we call them X k where k ranges from 1 to n if n indeterminates are needed.

A number is said to be algebraic if it is one of the roots of a polynomial over Q. It is transcendental if it never is a root of a polynomial over Q. A finite set of numbers are algebraically independent over Q if no multivariate polynomial over Q has exactly this set as his roots.

With these definitions, we can finally explicitly state the theorem.

Theorem 1 (Lindemann-Weierstrass). For any non-zero natural number n and any algebraic numbers a 1 , . . . , a n , if the set {a 1 , . . . , a n } is linearly independent over Q, then {e a1 , . . . , e an } is algebraically independent over Q.

Stating the Lindemann-Weierstrass Theorem in Coq

In order to formally prove Theorem 1, the previous definitions need to be transfered in Coq, like the complex numbers. The library MathComp, originally developed to prove the four-color [START_REF] Gonthier | Formal proof-the four-color theorem[END_REF] and Feit-Thompson theorems [START_REF] Gonthier | A machine-checked proof of the odd order theorem[END_REF], provides a nice frame to define algebraic structures. In fact, to define complex numbers in module Cstruct, we use the Coq standard library of real numbers, and a MathComp file to define complexes as pairs over a real-closed field.

CoInductive complex (R : Type) : Type := Complex { Re : R; Im : R }. Definition complexR := (complex R).

Thanks to the real-closed field structure of the real numbers and the Math-Comp tools, the type complexR automatically inherits a closed field structure, equipped with a norm and a complete order on this norm. There exists a morphism QtoC from rat to complexR. This allows the use of the predicate algebraicOver QtoC x which states that there exists a polynomial over rat such that when its coefficients are embedded into complexR by QtoC, x is one of its roots.

Notation QtoC := (ratr : rat → complexR). Notation "x 'is_algebraic'" := (algebraicOver QtoC x).

We can then define the complex exponential from the embedding RtoC, and the Coq standard library functions, cos, sin and exp. In MathComp, as soon as a type has a monoid structure, an interface (bigop) is provided for the repeated use of the monoid operation. This usually translates in the possibility to easily write sums or products. For example, we call exp-linear combination of the tuples β and α the linear combination of the exponentials of α's with the β's as coefficients. For instance, the exp-linear combination of (2, 3) and (4, 5) is 2e 4 + 3e 5 .

Definition Cexp_span (n : nat) (a : complexR^n) (alpha : complexR^n) := \sum_(i : 'I_n) a i * Cexp (alpha i).

Mathematical tuples are used a lot in the proof of the Lindemann-Weierstrass theorem. In MathComp, they can either be viewed as a sequence of fixed size (tuple) or as a function with finite domain (finfun), which are actually constructed above tuple. For instance, with functions, the type of a mathematical n-tuple of complexes is complexR^n. In the context of multivariate polynomials, a monomial is also a tuple of natural numbers: to each ordinal i it associates the exponents of X i .

Finally, concerning polynomials, whether univariate or multivariate, the predicate \is a polyOver P (resp. mpolyOver) states that all the coefficients of the polynomial respect a certain predicate P. In each case, we also have a way to evaluate them: p.[x] for univariate polynomials and p.@[t] for multivariate polynomials.

To prove the Lindemann-Weierstrass theorem, we have to recognize the rational numbers amongst the complex. In the case of algebraic numbers, there exists a boolean function that returns true if a number is rational, and false in the other case [START_REF] Cohen | Formalized algebraic numbers: construction and first-order theory[END_REF]. In our context, we already added an axiom (from the Coq standard library: Epsilon, only on equality) which makes it possible to transform the equality between two reals into a boolean function. This boolean equality with the fact that complexR verifies a modified version of the archimedean property implies that testing whether a complex is an integer or not is now a boolean function.

Definition archimedean_axiom (R : numDomainType) : Prop := forall x : R, exists ub : nat, '|x| < ub%:R.

This means we have two boolean predicates Cnat and Cint that recognize if a complex number is a natural number or an integer. This also means that any numDomainType (approximately, an integral domain with a norm, a partial order and a boolean equality) which verifies this archimedean property can be automatically equipped with these two predicates, like int, rat, or algC (algebraic complex numbers).

Instead of adding yet another axiom to obtain a boolean predicate for the rationals, we preferred changing small parts of the proof to equivalent ones that don't rely on rational numbers. Moreover, as the MathComp library is designed around reflections between properties and booleans, this really improves both the feasibility and the ease of use for the proof.

The last missing piece concerns the linear and algebraic independence of a set of numbers. Their formalization follows almost exactly the mathematical definitions except that the set over which the independence is considered (Q until now, P in the following definition) is represented as a predicate.

Definition lin_indep_over (P : pred_class) {n : nat} (x : complexR^n) := forall (lambda : complexR^n), lambda \in ffun_on

P → lambda != 0 → \sum_(i < n) (lambda i * x i) != 0.
Definition alg_indep_over (P : pred_class) {n : nat} (x : complexR^n) := forall (p : {mpoly complexR[n]}), p \is a mpolyOver _ P → p != 0 → p.@[x] != 0.

We can now state Theorem 1 in Coq, using the predicate Cint, as the linear (or algebraic) independence over Q is the same as over Z Z.

Theorem Lindemann (n : nat) (a : complexR^n) :

(n > 0)%N → (forall i : 'I_n, alpha i is_algebraic) → lin_indep_over Cint alpha → alg_indep_over Cint (finfun (Cexp \o alpha)).

Proof Context

The proof has a small part involving real analysis on functions with complex values, and more precisely, derivatives and integrals of such functions. For this part, we use the Coquelicot library [START_REF] Boldo | Coquelicot: A user-friendly library of real analysis for Coq[END_REF] which gives us a way to get an upper bound for an integral (RInt).

RInt (fun x => norm ((T i)^+ p).[x *: alpha j]) 0 1 <= M ^+ p.
This means that our development is based on multiple libraries which were not meant to be used together. In Fig. 1, we show how the different libraries interact with each other. As the context for this proof is almost exactly the same as for the direct proof of e and π, you can refer to [START_REF] Bernard | Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials[END_REF] for more details. Baker's proof doesn't actually prove Theorem 1 but rather a reformulation which we call Theorem 2. This reformulation provides the advantage of eliminating the study of linear and algebraic independence.

Multivariate Polynomials Mathematical Components

Coq

Theorem 2 (Baker's reformulation). For any non-zero natural number l, any distinct algebraic numbers α 1 , . . . , α l and any non-zero algebraic numbers β 1 , . . . , β l , we have:

β 1 e α1 + . . . + β l e α l = 0 . (2)
Its proof has 3 main steps. The first one focuses on the β's and strengthens their hypothesis, using the first lemma (Lemma 3). The second one deals with the α's and adds some conditions on them, showed in Lemma 4. The final part actually deals with the last lemma and proves it. We will present the ideas of these different steps in the following subsections.

In Fig. 2, the dashed arrows are the trivial implications that are not proved in this paper, as we focus on the proof of the Lindemann-Weierstrass theorem.

Baker's Reformulation

In this subsection, we prove that the Lindemann-Weierstrass theorem is at least as strong as Baker's reformulation (previously called Theorem 2).

As the notations in Sect. 2 cover our needs, we can immediately give the Coq translation of Theorem 2, and notice the change on l: to avoid any problem later on, we explicitly state that the tuple is not empty, as its size is l.+1. It should be noted that the conditions that the α's must be distinct is seen as the injectivity of the function alpha from 'I l.+1 to complexR.

Theorem LindemannBaker : forall (l : nat) (alpha : complexR^l.+1) (a : complexR^l.+1), injective alpha → (forall i : 'I_l.+1, alpha i is_algebraic) → (forall i : 'I_l.+1, a i != 0) → (forall i : 'I_l.+1, a i is_algebraic) → (Cexp_span a alpha != 0).

In order to prove this reformulation is at least as strong as Theorem 1, we need to recall some definitions around multivariate polynomials. The support of a multivariate polynomial p is the set of all the monomials which have a nonzero coefficients, and is written msupp p in Coq. Finally, it is worth noticing that when one evaluates a monomial on a set of exponential of numbers, one obtains the exponential of a linear combination of these numbers.

As shown below, the proof of the implication of the Lindemann-Weierstrass theorem by Baker's reformulation is pretty straightforward.

Proof. Let us call t the tuple of the support of p, alpha (resp. beta) the tuple of the evaluation of the monomials of t on the exponentials of a (resp. the coefficients of the monomials of t in p). We can then recognize an exp-linear combination: we prove the following equality and rewrite it. By applying Theorem 2, we are left with all its hypothesis to prove. All of them are almost instantaneous except the injectivity of alpha. To prove this last bit, it suffices to unfold alpha so that we obtain an equality between two linear combinations of the a, which can we reduced to a single linear combination.

\sum_(k < n) (((t i) k)%:R -((t j) k)%:R) * a k != 0
By linear independence, and unicity of the support of a polynomial, the proof is finished.

Simplifying the β's

The goal of the first part of Baker's proof is to show that we can assume, without loss of generality, that the β's are integers. Thus, this subsection gives some insights about the set of roots of a polynomial, the minimal polynomial, a total order on the complex and the formalization of the maximum of a tuple. With all these facts, we prove that Lemma 3 below implies Theorem 2. Lemma 3. For any non-zero natural number l, any distinct algebraic numbers α 1 , . . . , α l and any non-zero integers β 1 , . . . , β l , we have:

β 1 e α1 + . . . + β l e α l = 0 . (3)
The main difference between the mathematical statement and the Coq one is that we replace the condition on l to be non-zero by the explicit value l.+1.

Lemma wlog1 :

(forall (l : nat) (alpha : complexR^l.+1) (a : complexR^l.+1), injective alpha → (forall i : 'I_l.+1, alpha i is_algebraic) → (forall i : 'I_l.+1, a i != 0) → (forall i : 'I_l.+1, a i \is a Cint) → (Cexp_span a alpha != 0)).

To explain the proof, we need some definitions about symmetric polynomials and minimal polynomials. A multivariate polynomial is said to be symmetric if it is left unchanged by any permutation of its variables. For instance, the following polynomial is symmetric, but its first half isn't.

X 3 Y 2 Z + X 2 Y Z 3 + XY 3 Z 2 + X 3 Y Z 2 + X 2 Y 3 Z + XY 2 Z 3 . (4)
The fundamental theorem of symmetric polynomials states that any symmetric polynomial in a ring IK can be obtained from a particular set of symmetric polynomials using only addition, multiplication, and multiplication by coefficients in the ring IK. As we shall develop more on this topic later, let us just remark that as a consequence of this theorem, we have that for any symmetric polynomial whose coefficients are in IK, its evaluation on the set of roots of a polynomial is in IK.

To more easily track the set of roots of a polynomial, we gave ourselves a small definition, which expresses that a set f is the set of roots of a polynomial. To be more general, we consider an archimedean closed field T with a norm and partial order, a predicate S and say that the polynomial whose roots are exactly f has all its coefficients in S when multiplied by a number c.

(f \is a set_roots S c) = ((c *: \prod_(x <-enum_fset f) ('X -x%:P)) \is a polyOver S).

In our case, the predicate will be Cint and the field complexR. Once more, as we can't recognize the rational numbers among the complex, we workaround this problem by specifying a multiple (c) of the expected least common multiple of the denominator of all the coefficients. The negative point of having one more parameter is once again largely compensated by the gain in ease of proof from a boolean predicate.

The minimal polynomial of an algebraic complex number x is the polynomial of smallest degree which has x as a root, whose coefficients are in Q and whose leading coefficient is 1 (we also say monic). We defined two related notions for the minimal polynomial: the one whose coefficients are in Z Z, and the one already embedded in the complex.

The first one, polyMinZ, is the irreducible, separable polynomial whose coefficients are in int, whose zcontents (the greatest common divisor of all its coefficients with the same sign as the leading coefficient) is 1, and which divides exactly all the polynomials which have x as a root. It corresponds to the minimal polynomial multiplied by the least common multiple of the denominators of all its coefficients, and if needed, by -1 so that the leading coefficient is positive.

{p : {poly int} | [∧ (zcontents p = 1), irreducible_poly p, separable_poly (map_poly ZtoC p) & forall q : {poly int}, root (map_poly ZtoC q) x = (p %| q)]}.

To prove the existence of such a polynomial, we used the fact that any number of type algC has a minimal polynomial over rat. As shown in Fig. 3, from an algebraic complex number x, we obtain a polynomial p which has x as a root. We can then proceed by recurrence on the degree of p to prove the existence of the minimal polynomial of x: if it is below or equal to 2, we already have a candidate for the minimal polynomial. From this point, we extract a root xC in algC of the polynomial p embedded in algC, and call its minimal polynomial q. If x is a root of q, we found a candidate for its minimal polynomial. If not, then q divides p, and we obtain a new polynomial with coefficients in rat with a smaller size and which has x as a root. By recurrence, we obtain a candidate. Once we have a candidate, we have to transform it to be in int instead of rat, by multiplying it by the least common multiple of the denominators of all its coefficients.

x p xC q q or p/q minPolyZ algebraic closed field min. poly. Proof (Lemma 3 =⇒ Theorem 2). We proceed by contrapositive, so we assume we have some l, α's and β's that respect Theorem 2's assumptions but contradict its conclusion: the linear combination of the β's and the exponentials of α's is considered equal to 0. Every β is algebraic: for each k which ranges from 1 to l, we call B k the set of roots of the minimal polynomial of β k . Then, we multiply all the expressions obtained by letting the β k 's to run independently through the B k 's in the left-hand side of (2).

β 1 ∈B1 • • • β l ∈B l (β 1 e α1 + . . . + β l e α l ) = 0 . (5)
Finally, ( 5) is symmetric with respect to each B k so that the new coefficients of the linear combination are rationals. It then suffices to multiply by the least common multiple of the denominators to ensure the new β's are integers.

In this proof, we can notice three main problems. In usual mathematical practice, we don't even bother checking if there is at least one new β and α to contradict Lemma 3. Secondly, we recognize an expression as symmetric and then directly state that the result is what we expected. Actually, we are supposed to begin by showing it is a symmetric polynomial evaluated on some numbers, then continue by applying the fundamental theorem of symmetric polynomials and end by verifying we obtain a Q-exp-lin combination. Finally, even the application of the theorem is misleading: we have to apply it for each B k .

The first point can be resolved by following the highest α according to the lexical ordering on complex numbers following the real part and then the imaginary part: In order to follow the highest of the α's, we define the maximum of a tuple. This is the repeated use of the maxc operation on the tuple, which evokes the bigop module. The structure (complexR, maxc) is not equipped with a monoid structure and we cannot use directly the big operations provided by the MathComp library.

In the case of a non-empty tuple f, we invoke the sequence case whose default value is the first value of the tuple (f ord0), and whose sequence is the sequence value of the tuple (codom f).

Definition bmaxf n (f : complexR^n.+1) := bigmaxc (f ord0) (codom f).

The third point can be resolved by changing a little bit the proof. Instead of letting each β k to run only within B k , they can now run through the whole B = l k=1 B k , seen as a multiset. Expression ( 5) is then changed into:

β 1 ∈B • • • β l ∈B (β 1 e α1 + . . . + β l e α l ) = 0 . ( 6
)
It presents two immediate benefits. First, ( 6) is now completely symmetric in the β's, which means we now only have to use the fundamental theorem of symmetric polynomials once. Secondly, it makes the expression clearer, and thus, more convincing. Finally, we can notice that the products in ( 6) can be replaced by a single product sign over the l-tuples of elements of B.

For the second point, we can identify explicitly the left-hand side of (2) with a multivariate polynomial whose coefficients are also multivariate polynomials evaluated on the right points: the first set of indeterminates represents the β's, the second set is used to hide the exponentials and verify that, in the end, we still obtain a linear combination of rationals and exponentials. For instance, ( 6) is changed into the following, where L.+1 is the cardinal of B.

((\prod_(f : 'I_L.+1 ^l.+1) \sum_(i : 'I_l.+1) 'X_i *: 'X_(f i))

.@[finfun ((@mpolyC l.+1 complexR_ringType) \o beta)]) .@[finfun (Cexp \o alpha)] = 0.

We can also notice that Lemma 3 is a direct consequence of the Lindemann-Weierstrass theorem.

Simplifying the α's

The second and third steps in Baker's proof both revolve around the same new lemma which strengthens the conditions on the α's. But, we need some last definitions to be able to write it.

First of all, a partition of a set S is a set of sets such that none of its elements is the null set, all of its elements are disjoint, and the union of all its elements is exactly S. For instance, {{1, 3, 6}, {2}, {4, 5}} is a partition of {1, 2, 3, 4, 5, 6}. In MathComp, the notion already existed and is based on the null set (set0), the union of all its parts (cover P) and trivIset which is a predicate that treats the disjoint condition by studying the cardinal of the parts of P. Secondly, two complex numbers are called conjugates if they are roots of a same minimal polynomial. In particular, in order to find a minimal polynomial, we need at least one of those numbers to be algebraic. In this case, an algebraic number x and a complex number y are conjugates if y is a root of the minimal polynomial of x.

Lemma conjOfP (x y : complexR) (x_alg : x is_algebraic) : reflect (y \is a conjOf x_alg) (root (polyMin x_alg) y).

We also say a set of conjugates is complete if it is exactly the set of all the roots of a minimal polynomial. For instance, {

√ 2} is a complete set of conjugates. Formalizing this property with a boolean predicate leads to a strange definition which once again uses an additional parameter c with the same role. In particular, given a complex c and a set f of complex numbers, our definition checks if P := c *: \prod (x <-enum fset f) ('X -x%:P) is non-zero, non-constant and only has integer coefficients, and from the proofs of these three statements, it constructs the minimal polynomial of a root of P. Then, it suffices to check if these two polynomials are equal up to an integer multiplication. In particular, any complex in a complete set of conjugates is algebraic.

Lemma setZconj_algebraic (c x : complexR) (f : {fset complexR}) :

x \in f → f \is a setZconj c → x is_algebraic.

Lemma 4. For any non-zero natural number l, any distinct algebraic numbers α 1 , . . . , α l and any non-zero integers β 1 , . . . , β l , such that the α's can be grouped into a partition P , if for each part in P , the α's form a complete set of conjugates, and on each part in P , the β's are constant, then:

β 1 e α1 + . . . + β l e α l = 0 . (7)
With the previously introduced notation, we obtain the following lemma in Coq. To continue the proof of the Lindemann-Weierstrass theorem, we need to prove that Lemma 4 implies Lemma 3. Its proof follows the same steps as the proof in Sect. 3.2 so we won't give too much details. The main differences and sources of difficulties between the two proofs can be found in Fig. 4. They come from the fact that we need to be far more specific in each argument. For instance, in Sect. 3.2, we introduced the fundamental theorem of symmetric polynomials. Here, we need a more precise version that states that any symmetric polynomial in a ring IK can be obtained as a IK-linear combination of a particular set of symmetric polynomials: the monomial symmetric polynomials. Each one is exactly the smallest symmetric polynomial of a monomial X k1 1 X k2 2 . . . X kn n , that is the sum of all the monomials X k1 σ(1) X k2 σ(2) . . . X kn σ(n) that can be obtained from all the permutations σ of the indeterminates. In Coq, we called them mmsym x or 'm x if x is a monomial.

Proving the Final Lemma

The final part of the proof uses even more precise arguments around multivariate polynomials and symmetry.

Proof. To actually prove Lemma 4, which corresponds to the third part of Baker's proof, we proceed by contradiction. We then need to introduce many notations and a big enough prime number p. This p only depends on the values of the α's and β's, and must be an upper bound (UB) of a certain polynomial T on [0; 1]. Once it is defined, we construct other polynomials and values I, J and K, as shown in Fig. 5 and study them in two ways. First, with algebra, we can show they have some properties of divisibility which lead to a lower bound for K. Then, as I can be recognized as an integral of a function of T , we can find an upper bound, and consequently, an upper bound for K, too. Finally, we combine both inequations involving K:

(p -1)! n ≤ K < (p -1)! n . (8)
This is a logical contradiction which completes the proof. This proof follows the same steps as the common lemma of the transcendence of e and π up until the results on J. In the last few different steps which are only in the algebra part, Baker proposes to impose being algebraic integers on the α's and then speaks of divisibility of algebraic integers by natural numbers. Because of the path chosen in the common lemma proof, we can finish the proof without ever explicitly using algebraic integers.

The proofs of divisibility on K relies heavily on repeated uses of the fundamental theorem of symmetric polynomials. In fact, K is the evaluation of a multivariate polynomial K m on the α's. For each part of the partition P , K m is symmetric on the subset of indeterminates of the part but not fully symmetric. This means that the theorem can not be applied directly on the full set of indeterminates, but repeatedly on each subset of indeterminates corresponding to a part of the partition, that is on a subset of indeterminates which make K m symmetric and corresponds to a complete set of conjugates. All the indeterminates must be considered once and only once, hence the need for a partition on complete set of conjugates.

We formalized a predicate symmetric for indicating if a multivariate polynomial is symmetric on a given subset of its indeterminates in the same way as a fully symmetric polynomial: it must be equal to itself on any permutation of this subset of indeterminates. This was done with an already existing predicate perm on on permutations that states that outside the subset, the permutation maps a value to itself.

Thanks to this predicate and extensions of other notations such as the smallest symmetric polynomial containing a monomial, we were able to obtain a new formalized corollary of the fundamental theorem of symmetric polynomials.

Lemma 5. Given a natural number m, a m-tuple l of unique complex numbers, a m-variate polynomial p whose coefficients are rationals, and P a partition of {1, . . . , m}, if p is symmetric on each part of P for each part of P , the corresponding l's form a complete set of conjugates, then P (l 1 , . . . , l m ) is rational.

This can be generalized in Coq to a closed field T (instead of C) and a boolean predicate kS (instead of rational) compatible with ring operations.

partition P [set: 'I_m.+1] → injective l → {in P, forall Q : {set 'I_m.+1}, [fset l i | i in Q]%fset \is a set_roots kS c} → p \is a mpolyOver m.+1 kS → {in P, forall Q, p \is (@symmetric_for _ _ Q)} → c ^+ (msize p).-1 * p.@[l] \in kS.

Conclusion

Related Work

Concerning transcendance formalizations, this work is a follow-up of the proof of transcendence of e by Bingham [START_REF] Bingham | Formalizing a proof that e is transcendental[END_REF] in HOL Light, and of the proofs of transcendance of e and π in Coq.

The work on multivariate polynomials is primarily based on a development made by Strub, and continued by Hivert who also formalized monomial symmetric polynomials but relied upon the definitions of partitions of an integer. We prefered to have a self-sufficient definition which introduces the notion of the smallest symmetric polynomial containing a monomial. Nevertheless, we added a lemma to ensure the compatibility of both definitions.

To our knowlegdge, this is the first formalization of multivariate polynomials that are symmetric on a subset of their indeterminates. This is not really surprising as the main current use of multivariate polynomials consists in studying the Bernstein polynomials [START_REF] Muñoz | Formalization of a representation of Bernstein polynomials and applications to global optimization[END_REF] in order to approximate polynomial inequalities. Moreover, it would be easier to separate the indeterminates in two sets (symmetric or not) of indeterminates, rather than staying with a fixed number of indeterminates.

Future Work

In the future, the multivariate polynomial library will evolve to pick the indeterminates differently, allowing the change of the number of indeterminates to be far easier. This will probably change the statement of the corollary of the fundamental theorem of symmetric polynomials, and make its proof way easier.

It could be interesting to try to formalize the same theorem using Galois theory as it is already formalized in Mathcomp, to compare the proofs. In the same spirit, proving the existence of an embedding from the algebraic complex numbers (type algC) to the complex numbers (type complexR) could offer a different view on the proof, with different definitions or different proofs. Nevertheless, the construction of the complex numbers would still be necessary for the analysis part.

The next step could probably be to prove Baker's theorem on the linear form of complex logarithms, as it is the basis for several developments derived from transcendence.

Definition

  Cexp (z : complexR) : complexR := RtoC (exp(Re_R z)) * (RtoC (cos (Im_R z)) + 'i * RtoC (sin (Im_R z))).

Fig. 1 .

 1 Fig. 1. Link between the different libraries

Fig. 2 .

 2 Fig. 2. Implications between the different theorems and lemmas

  P.@[finfun (Cexp \o a)] = Cexp_span beta alpha.

Fig. 3 .

 3 Fig. 3. Existence of a minimal polynomial

  Definition letc x y := ('Re x < 'Re y) || (('Re x == 'Re y) && ('Im x <= 'Im y)).

  Definition partition (T : finType) (P : {set {set T}}) (D : {set T}) := [&& cover P == D, trivIset P & set0 \notin P].

  Lemma wlog2 : forall (l : nat) (c : complexR) (alpha : complexR^l.+1) (part : {set {set 'I_l.+1}}) (a : complexR^l.+1), c != 0 → c \is a Cint → injective alpha → partition part [set: 'I_l.+1] → {in part, forall P : {set 'I_l.+1}, [fset (alpha i) | i in P]%fset \is a setZroots c} → (forall i : 'I_l.+1, a i != 0) → (forall i : 'I_l.+1, a i \is a Cint) → {in part, forall P : {set 'I_l.+1}, constant [seq a i | i in P]} → Cexp_span a alpha != 0.

2 Fig. 4 .

 24 Fig. 4. Comparison of the proofs of Sect.3.3 (left) and Sect.3.2 (right)

Fig. 5 .

 5 Fig. 5. Proof structure of Lemma 4


Andreas Fuchs
email: andreas.fuchs@sit.fraunhofer.de

Sigrid Gürgens
email: sigrid.guergens@sit.fraunhofer.de

Carsten Rudolph
email: carsten.rudolph@sit.fraunhofer.de

A Formal Notion of Trust -Enabling Reasoning about Security Properties

Historically, various different notions of trust can be found, each addressing particular aspects of ICT systems, e.g. trust in electronic commerce systems based on reputation and recommendation, or trust in public key infrastructures. While these notions support the understanding of trust establishment and degrees of trustworthiness in their respective application domains, they are insufficient for the more general notion of trust needed when reasoning about security in ICT systems. In this paper we present a formal definition of trust to be able to exactly express trust requirements from the view of different entities involved in the system and to support formal reasoning such that security requirements, security and trust mechanisms and underlying trust assumptions can be formally linked and made explicit. Integrated in our Security Modeling Framework this formal definition of trust can support security engineering processes and formal validation and verification by enabling reasoning about security properties w.r.t. trust.

Introduction

The meaning of the term trust in the context of information and communication technology (ICT) systems differs from the concept of trust between people. In particular trust as seen in the notion of trusted computing (e.g. as defined by the Trusted Computing Group TCG) refers to particular properties of a technical system. This notion of trust stands in contrast to some more intuitive notions of trust expressing that someone behaves in a particular well-behaved way. Trust in a technical system always has to be seen as trust in a property of the system. A more meta-level generic trust as it is possible for people ("I trust you") is not useful for computers or technical entities as parts of communication networks. A variety of existing notions of trust in the context of ICT systems addresses particular aspects, e.g. trust in electronic commerce systems based on reputation and recommendation, or trust in public key infrastructures (see Section 3 for a survey). While these notions are useful to understand trust establishment and degrees of trustworthiness in these application domains, they cannot be used for a more general notion of trust needed to reason about trust in ICT systems. In addition to the restricted applicability there is also a lack of formal semantics for the properties expressed by these different notions of trust. However, when used in a security engineering process, formal semantics are essential for traceability of trust and security requirements through the different steps of the process. This traceability is necessary to show relations between high-level requirements and underlying security mechanisms (e.g. particular cryptographic algorithms) and trust assumptions (e.g. trust in hardware security or trust in a particular behaviour of people using the system).

The goal of the formal notion of trust presented in this paper is to be able to exactly express trust requirements for ICT systems from the view of the different entities involved in the system, and to support formal reasoning such that finally security requirements, security and trust mechanisms and underlying trust assumptions can be formally linked and made explicit. Such a formal notion of trust can support security engineering processes as well as formal validation and verification. Previously established notions for security properties with formal semantics can provide traceability in a security engineering process as well and are used for validation and verification. However, trust adds another layer of information. While security properties may or may not be global properties of the system, trust always expresses the view of a particular entity or agent of the system. Trust depends on the individual perception of the agents. Therefore, different agents can have trust in contradictory properties. Furthermore, it must also be possible to express that one agent trusts that another agent has trust in a particular property (e.g. for expressing trust in certification authorities).

The notion of trust presented here extends the existing security modelling framework SeMF [START_REF] Gürgens | On a formal framework for security properties[END_REF]. This framework uses formal languages and is independent of specific representations of the system. The example used throughout the paper discusses trust of an agent in that a specific authenticity property holds in a system. This example is used to explain our new notion of trust and to show how reasoning can lead to refined trust properties that express underlying trust assumptions and assumptions on security mechanisms that are not further refined within the model.

The following two sections first provide some terminology and then briefly discuss its relation to existing notions of trust. In Section 4 we introduce an example that will be used throughout the rest of the paper and that imposes some interesting questions related to trust. Section 5 then gives a brief summary of our Security Modeling Framework SeMF. Based on this, we present our formal notion of trust in Section 6 and use it to formally prove some security properties of our example in Section 7. Finally we present our conclusions in Section 8.

Terminology

The meaning of the word trust has been subject to many (more or less philosophical) discussions, many different interpretations with subtle differences exist. Achieving a common understanding of the term trust is further complicated by mixing it with the related notions of trustworthiness or reputation. The formal notion of trust introduced in this paper is supposed to be useful mainly for reasoning about trust in the context of technical systems in the area of ICT. The work was motivated by concepts such as trusted computing using the so-called Trusted Platform Module (TPM) [2]. Therefore, we do not intend to contribute to the philosophical discussions on trust or the relation between trust and reputation.

Within our formal framework we will use the following terminologies:

The term trust refers to a relation from one agent in the system to another agent with respect to a property, or from an agent directly to a property in the system. Thus, agents can have three slightly different types of trust:

1. Agents can trust that some (global) property holds in a system. 2. Agents can trust that another agent behaves in a certain way, i.e. that a property concerning the behaviour of this other agent is satisfied. 3. Agents can trust that another agent has a particular trust.

Being a relation, this notion of trust cannot be used to express different degrees of trust. Agents can either trust or not trust. In a refinement process the notion of trust can be broken down into more detailed trust assumptions. These are expressed using the same formal notion of trust. However, as input for a subsequent security evaluation or risk assessment it is necessary to express to which degree this trust can be substantiated, i.e. what is the trustworthiness. Thus, we clearly distinguish between trust and trustworthiness. This motivates the following notion of trustworthiness.

The term trustworthiness expresses the degree to which a particular trust assumption can be made. Trustworthiness can be expressed as a probability or can simply have fixed values (e.g. high, medium, low). Depending on the particular representation of trustworthiness, agents within the system can reason about the trustworthiness of other agents, or reasoning mechanisms can be used for risk analysis and risk assessment.

Related work

A huge part of the approaches that use a notion of trust is concerned with reputation systems. In this area, trust is understood in the sense of trustworthiness as explained in Section 2 and e.g. defined by the research project Trust4All [START_REF] Muskens | Trust4All Trust Framework and Mechanisms[END_REF]: "Trust is the degree to which a trustor has a justifiable belief that the trustee will provide the expected function or service." Jøsang et al. [START_REF] Jøsang | A survey of trust and reputation systems for online service provision[END_REF] present two different notions of trust that capture main aspects in the context of reputation systems:

-Reliability Trust: "Trust is the subjective probability by which an individual, A, expects that another individual, B, performs a given action on which its welfare depends."

This definition captures both the concept of dependence on the trusted party and the non-binary nature of trust in the context of reputation systems. -Decision Trust: "Trust is the extent to which one party is willing to depend on something or somebody in a given situation with a feeling of relative security, even though negative consequences are possible. (inspired by [START_REF] Mcknight | The Meanings of Trust[END_REF])" Hence the concept of Decision Trust is useful in the context of risk assessment.

This or similar characterizations of "trust" can be found in many of the approaches in this area. A very good overview of approaches regarding trust in reputation systems along with a clarification and classification of the main concepts is given by Jøsang et al. [START_REF] Jøsang | A survey of trust and reputation systems for online service provision[END_REF]. They explain these concepts further by means of temporary reputation based systems such as eBay. Another survey that focusses particularly on trust management systems is given by Grandison and Sloman [START_REF] Grandison | A survey of trust in internet applications[END_REF].

A second branch of research focusses on formal models that capture certain aspects of trust. In [START_REF] Carbone | A formal model for trust in dynamic networks[END_REF] Carbone et al. introduce a formal model of trust that focusses on the formation, evolution and propagation of trust. Trust in their model is viewed as a function that assigns values to pairs of principles. The model can be used to formulate trust policies, however these seem to be restricted to access control. Further, their approach is not aimed at reasoning about security properties holding or not holding in a system. Delombe [START_REF] Demolombe | Reasoning about trust: A formal logical framework[END_REF] provides a formal definition for trust that distinguishes between different properties an agent may have trust in. Axioms related to these properties are defined, and the resulting axiomatic structure can then be used to reason about conditional trust between agents with respect to ratings regarding aspects such as cooperativity and credibility.

Another branch of research that takes a similar axiomatic approach are the so-called authentication logics. These logics use a specific notion of trust and aim at reasoning about security properties of a system. In particular, these logics are useful for the security verification of cryptographic protocols. The first such logic was the BAN Logic [START_REF] Burrows | A Logic of Authentication[END_REF] by Burrows et al. Here the concept of jurisdiction models trust of agents in statements of specific other agents about for example the trustworthiness of a key. The BAN logic inspired a large number of similar logics (see for example [START_REF] Syverson | On unifying some cryptographic protocol logics[END_REF][START_REF] Abadi | A Semantics for a Logic of Authentication[END_REF][START_REF] Gong | Reasoning about Belief in Cryptographic Protocols[END_REF][START_REF] Gürgens | SG Logic -A formal analysis technique for authentication protocols[END_REF]). Each of these logics constitutes an axiomatic system, i.e. formulates axioms and inference rules that capture the nature of security mechanisms and proves that certain security properties are provided given that certain assumptions on the system hold.

Although these approaches seem to be closely related to the one introduced in this paper, there is a fundamental difference: Our formalization of trust and the thereby enabled reasoning about security properties does not use axioms but is based on a formal semantics that uses only formal language theory. Further, our notion of trust applies to any security property and is independent of any security mechanism that might be employed to achieve a security property, while the security properties handled by authentication logics are directly derived from specific aspects of security mechanisms.

As already explained in Section 1, we do not address trust in the context of reputation systems. Our notion of trust is motivated by the work in the area of trusted computing [2] where trust refers to particular properties of a technical system. Our work aims at providing means to support formal reasoning such that security requirements, security and trust mechanisms, and underlying trust assumptions can be formally linked and made explicit. However, reputation systems can be seen as complementary to our approach. Results achieved by our reasoning can be used as input for a subsequent security evaluation or risk assessment where it is necessary to express to which degree trust can be substantiated. On the other hand, reputation systems can be used for substantiating trust assumptions being input for our reasoning.

An Example

In this section we introduce a very simple use case that includes a security requirement involving specific trust requirements. Similar situations typically arise in many scenarios from different domains, such as car-to-car, distributed sensor networks or email. This use case serves both as a motivation for our concept of trust and as an example of how to use this concept in order to prove that specific security mechanisms together with certain trust assumptions result in the satisfaction of specific security properties.

However, we discuss the security properties and resulting trust requirements only informally in this section in order to give an understanding of the practical implication of our notion of trust. In the subsequent sections we will provide a brief introduction to our formal Security Modeling Framework (SeMF), will introduce the formal definition of trust, some resulting theorems, and will revisit the example formally.

In order to explain our approach we will use the scenario illustrated in Figure 1.

Sensor send data sense data

Display

show data receive data

U ser

Fig. 1. Example System

Our example system consists of two active nodes and an end user. Sensor is a node deployed somewhere in the system that performs measurements (e.g. measures the temperature outside a house) and sends the resulting data over the network. Display is the second node of the system. It receives data from the network and displays them to the end user User (e.g. the owner of the house).

An obvious requirement of the above use case is that the user, when being shown some data, wants this data to be indeed measured by the Sensor. This requirement is usually denoted by data origin authenticity and can be informally stated as follows: P0 It must be authentic for the end user that the data he/she is shown on the display is the data that was measured by the Sensor.

There exist several schemes that can be used to secure a communication channel and provide data origin authenticity for a message during transfer over the network, such as digital signature schemes or message authentication codes (MACs). However, whatever mechanism is used, the user, a human being, cannot validate a digital signature or MAC, this has to be done by the Display node. Therefore it is the Display node that can be assured of the authenticity and not the user. Further what can actually be provided when applying these mechanisms to our use case is that each time the Display node receives some data and verifies the signature or MAC, it can be sure that the signature or MAC was generated by the Sensor. Yet, this assurance does not extend to the action of measuring the data, the Sensor can very well sign data different to the one that it has measured. Also, it is the action of showing the data that is relevant for the user, not the action in which the Display node receives and verifies it (the Display might show data different to the one received).

In order to capture this situation and simplify the example, we abstract the Sensor actions of signing and sending the data to a sending action, the Display actions of receiving and verifying the data to a receiving action, but keep the measuring and displaying actions, respectively, separate. The property provided by a digital signature or MAC can then be expressed as follows:

P1 It is authentic for the Display node that the data received is the data that was sent by the Sensor.

. Discrepancy between required and provided property

The discrepancy between property P0 we want the system to provide and property P1 that is actually provided by a digital signature or MAC is illustrated in Figure 2. For achieving P0 we need the system to provide more properties: In order for the Display to "extend" the authenticity of the send action by the Sensor node to the actual measuring action, the Display must trust the Sensor that it only sends data it has measured. Further, the user must trust the Display to show only what it has received and verified. Hence we need a concept of trust that allows to relate agents to the system properties they trust in and that enables formal reasoning about these properties.

An agent trusts in a property to hold in a system if in its conception of the system this property is fulfilled.

In the next section we give a brief introduction of those parts of the Security Modelling Framework SeMF that are the basis for the notion of trust presented in this paper. We then explain the concept of a property being fulfilled in an agent's conception of a system, the basis for our definition of trust.

The Security Modeling Framework SeMF

The behaviour B of a discrete system S can be formally described by the set of its possible sequences of actions (traces). Therefore B ⊆ Σ * holds, here Σ (called the alphabet) is the set of all actions of the system, Σ * is the set of all finite sequences (called words) of elements of Σ, including the empty sequence denoted by ε, and subsets of Σ * are called formal languages. Words can be composed: if u and v are words, then uv is also a word. For a word x ∈ Σ * , we denote the set of actions of x by alph(x). For more details on the theory of formal languages we refer the reader to [START_REF] Eilenberg | Automata, Languages and Machines[END_REF].

We further extend the system specification by two components: agents' initial knowledges about the global system behaviour and agents' local views. The initial knowledge W P ⊆ Σ * of agent P about the system consists of all traces P initially considers possible, i.e. all traces that do not violate any of P 's assumptions about the system. Every trace that is not explicitly forbidden can happen in the system. An agent P may assume for example that a message that was received must have been sent before. Thus the agent's W P will contain only those sequences of actions in which a message is first sent and then received. Further we can assume B ⊆ W P , as reasoning within SeMF primarily targets the validation and verification of security properties in terms of positive formulations, i.e. assurances the agents of the system may have. Other approaches that deal with malfunction, misassumptions and attacker models could not rely on this assumption.

In a running system P can learn from actions that have occurred. Satisfaction of security properties obviously also depends on what agents are able to learn. After a sequence of actions ω ∈ B has happened, every agent P can use its local view λ P of ω to determine the sequences of actions it considers to have possibly happened. Examples of an agent's local view are that an agent can see only its own actions, or that an agent P can see that an action send(sender, message) occurred but cannot see the message, in which case λ P (send(sender, message)) = send(sender).

For a sequence of actions ω ∈ B and agent P ∈ P (P denoting the set of all agents), λ -1 P (λ P (ω)) ⊆ Σ * is the set of all sequences that look exactly the same from P 's local view after ω has happened. Depending on its knowledge about the system S, underlying security mechanisms and system assumptions, P does not consider all sequences in λ -1 P (λ P (ω)) possible. Thus it can use its initial knowledge to reduce this set: λ -1 P (λ P (ω)) ∩ W P describes all sequences of actions P considers to have possibly happened when ω has happened.

Security properties can now be defined in terms of the agents' initial knowledges and local views. In [START_REF] Gürgens | On a formal framework for security properties[END_REF] we have introduced a variety of definitions of security properties (e.g. authenticity, proof of authenticity, confidentiality). Our concept of trust introduced in the next section applies to all of them, however, we will use our notion of authenticity as a demonstrating example.

We call a particular action a authentic for an agent P if in all sequences that P considers to have possibly happened after a sequence of actions ω has happened, some time in the past a must have happened. By extending this definition to a set of actions Γ being authentic for P if one of the actions in Γ is authentic for P we gain the flexibility that P does not necessarily need to know all parameters of the authentic action. For example, a message may consist of one part protected by a digital signature and another irrelevant part without protection. Then, the recipient can know that the signer has authentically sent a message containing the signature, but the rest of the message is not authentic. Therefore, in this case, Γ comprises all messages containing the relevant signature and arbitrary other message parts.

Definition 1 A set of actions Γ ⊆ Σ is authentic for P ∈ P after a sequence of actions ω ∈ B with respect to W P if alph(x)∩Γ = ∅ for all x ∈ λ -1 P (λ P (ω))∩W P .

We define the following instantiation of this property that states that whenever an action b has happened in a sequence of actions ω, it must be authentic for agent P that action a has happened as well. Note that in most cases, action b is in P 's local view.

Definition 2 For a system S with behaviour B ⊆ Σ * , agent P ⊆ P, and actions a, b ∈ Σ, auth(a, b, P ) holds in B if for all ω ∈ B, whenever b ∈ alph(ω), the action a is authentic for P .

The precedence of actions is a weaker property: Definition 3 For a system S with behaviour B ⊆ Σ * and actions a, b ∈ Σ, precede(a, b) holds in S if for all ω ∈ B with b ∈ alph(ω) it follows that a ∈ alph(ω).

A Formal Definition of Trust

In the previous section we have presented several factors that are important regarding security properties holding or not holding in a system. Accordingly we include these in the formal definition of a system as follows:

Definition 4 (System) A system S = (Σ, P, B, W, V) consists of a set P of agents acting in the system, a language B ⊆ Σ * over an alphabet of actions Σ describing the system behaviour in terms of sequences of actions, a set V = {λ X : Σ * → (Σ X ) * |X ∈ P} of agents' local views, and a set W = {W X ⊆ Σ * |X ∈ P} of agents' initial knowledges.

Here (Σ X ) * denotes the image of the homomorphism λ X which has to be individually specified for each system. Which part of an action an agent can see depends on the specific system to specify and can contain any part of it, as indicated in the previous section.

An agent P 's conception and understanding of a system S, denoted by S P , may defer from the actual system. P may not know all about the system's behaviour, thus from P 's point of view the system's behaviour consists of P 's initial knowledge W P . Further, P may not have all information with respect to the other agents' initial knowledges and local views, so P 's conception of agents' initial knowledges (W X P ) and local views (λ X P ) may defer from the actual initial knowledges and local views of the system S. This motivates the following definition.

Definition 5 (Trusted System) Agent P 's conception of system S is defined by S P = (Σ, P, W P , W P , V P ). Σ and P are the alphabet and set of agents, respectively, of both S and S P , whereas P 's initial knowledge (conception) W P ⊆ Σ * of system behaviour B constitutes the behaviour of S P . It further contains a set V P = {λ X P : Σ * → (Σ X P ) * |X ∈ P} of agent P 's conception of agents' local views of S, and a set W P = {W X P ⊆ Σ * |X ∈ P} of agent P 's conception of agents' initial knowledges in S. We say that P trusts in system S P (since it represents P 's knowledge about system S).

The definition of an agent's trusted system gives rise now to the definition of an agent's trust in a property holding in a system: Definition 6 (Trusted Property) Let prop be any property that refers to a system as defined in Definition 4. An agent P ∈ P trusts in prop to hold in a system S, denoted by trust(P, prop), iff prop is fulfilled in S P . This notion of trust follows naturally from the different aspects that constitute the model of a system. If a property holds in the system as P perceives it (i.e. in S P ), then from P 's point of view the property holds, i.e. P trusts in the property to hold in S. Further our notion of trust allows to specify precisely what it is an agent trusts in. An agent may have trust in one property but not in another. Of course, trust itself is a property of a system as well. Therefore the trust concept allows to model arbitrarily long trust chains such that e.g. the trust of an agent in another agent's trust in a property can be expressed.

Implications between Properties

In this section we present and prove specific implications of security and trust properties of SeMF that will then be used to reason about properties provided by the example system when introducing certain security mechanisms.

We use the following Assumption 1 to model that agents do not falsely exclude behaviour that can actually happen in the system. The correctness of this assumption must be verified during the formalization of a real system as a SeMF system model, violations identify flaws of the real system's design. Assumption 1 further models the fact that an agent P cannot assign an agent Q more knowledge about a system's behaviour than P itself knows about it. Note that the more an agent knows the smaller its initial knowledge.

Assumption 1 In general the behaviour of a system is included in all agents' initial knowledge (see Section 5). Hence B ⊆ W P , W P ⊆ W Q P , etc.

It is easy to show that Assumption 1 implies the following Lemma:

Lemma 1 Let S be a system as defined in Definition 4 with behaviour B, P ∈ P an agent, λ P this agent's local view, and W P ⊇ B this agent's initial knowledge. Then for all ω ∈ B holds ω ∈ λ -1 P (λ P (ω)) ∩ W P .

The next Theorem explains that authenticity is a stronger property than precede. This is due to the fact that precede is defined on the system behaviour B, while auth is defined taking into account an agent's local view and initial knowledge of a system which can result in a bigger set of sequences of actions. Theorem 1 a system S as defined in Definition 4, actions a, b ∈ Σ, and agent P ∈ P, auth(a, b, P ) holding in S implies that precede(a, b) holds in S.

Proof. Let S be a system as defined in Definition 4 with behaviour B, a, b ∈ Σ, P ∈ P, and let auth(a, b, P ) hold in S. Let us assume that precede(a, b) does not hold in S. Then there is ω ∈ B with b ∈ alph(ω) and a ∈ alph(ω). b ∈ alph(ω) and auth(a, b, P ) holding in S imply that a ∈ alph(x) for all x ∈ λ -1 P (λ P (ω)) ∩ W P . Since by Lemma 1 ω is one of the elements of λ -1 P (λ P (ω)) ∩ W P , it immediately follows that a ∈ alph(ω), a contradiction to the assumption. Hence precede(a, b) holds in S.

Corollary 1 For a system S, actions a, b ∈ Σ and agents P, Q ∈ P, trust(P, auth(a, b, Q)) holding in S implies that trust(P, precede(a, b)) holds in S.

Proof. The assertion follows immediately from Theorem 1. Since auth(a, b, P ) implies precede(a, b) in all systems, this implication holds in particular in the system S P .

The next Theorem shows that the authenticity of an action for an agent can be extended to a preceding action if the agent trusts in the precedence. Theorem 2 a system S as defined in Definition 4, actions a, b, c ∈ Σ and an agent P ∈ P, auth(b, c, P ) and trust(P, precede(a, b)) holding in S implies that auth(a, c, P ) holds in S.

Proof. Let S be a system as defined in Definition 4, a, b, c ∈ Σ, P ∈ P, and let auth(b, c, P ) hold in S. Then for all ω ∈ B, if c ∈ alph(ω) then b ∈ alph(x) for all x ∈ λ -1 P (λ P (ω)) ∩ W P . Further, trust(P, precede(a, b)) holding in S means that for all y ∈ W P , if b ∈ alph(y) then a ∈ alph(y). As λ -1 P (λ P (ω))∩W P ⊆ W P , a ∈ alph(x) in particular for all x ∈ λ -1 P (λ P (ω))∩W P . Hence auth(a, c, P ) holds in S.

Corollary 2 For a system S, actions a, b, c ∈ Σ, and agents P, Q ∈ P, trust(Q, auth(b, c, P ))∧trust(Q, trust(P, precede(a, b))) holding in S implies that trust(Q, auth(a, c, P )) holds in S.

Proof. Analogously to the proof of Corollary 1, we use the fact that Theorem 2 applies to all systems, hence in particular to S Q . Lemma 2 a system S as defined in Definition 4 and actions a, b, c ∈ Σ, precede(a, b) and precede(b, c) implies that precede(a, c) holds in S.

Proof. Let S be a system as defined in Definition 4, a, b, c ∈ Σ. precede(b, c) holding in S means that for all ω ∈ B, if c ∈ alph(ω) then b ∈ alph(ω). Further, precede(a, b) holding in S means that for all ω ∈ B, if b ∈ alph(ω) then a ∈ alph(ω). This concludes that if c ∈ alph(ω) then a ∈ alph(ω) for all ω ∈ B.

Theorem 3 For a system S and an agent P ∈ P, trust(P, precede(a, b) ∧ precede(b, c)) holding in S implies that trust(P, precede(a, c)) holds in S.

Proof. Analogously to the proof of Corollary 1, we apply Lemma 2 to the system S P .

In the next section we will apply the notion of trust and the above theorems to the example introduced in Section 4, and, by doing so, identify trust assumptions that need to hold in order for the system to provide certain security properties.

The Example Formally

We now specify our example system formally. It has three agents, so P = {Sensor, Display, U ser}. The set Σ of actions consists of Sensor-sense(data), Sensor-send (data), Display-rec(data), Display-show (data) and we assume that the parameter data can have different values, e.g. warm and cold. This is a very abstract formalization of the system's actions chosen simply to facilitate understanding. Our formalism works equally well with other notational conventions, e.g. (actionname, par 1 , . . . , par k ). Our formal model of the system needs to satisfy Assumption 1, in particular W U ser must be a subset of W U ser Display . As for our abstract system we simply assume equality. Further, agents' initial knowledges and local views must comply with the mechanisms and resulting properties discussed below. However, for our purposes we do not need to specify concrete initial knowledges of agents, and regarding the agents' local views it is sufficient to specify that the user's local view keeps the action Display-show (data) and maps all other actions onto the empty word, that is, the user can only see the data that is displayed to him/her. As to the other agents we simply assume them to be able to see only their own actions.

Figure 3 illustrates the requirement we have for the example system.

Note that we do not discuss here the quality of the data sensed by the Sensor, i.e. the question of how near it represents reality (although our framework allows to model this as well).

As explained in Section 4, a digital signature scheme (Sig) or message authentication code (MAC) can only establish a relation between signing/sending and receiving/verifying the data. Hence the property P1 informally stated in Section 4 can be formalized as follows:

auth(Sensor-send(data), Display-rec(data), Display)

As stated before, in order for the Display node to extend the authenticity of the sending action to the actual measuring action of the Sensor, the Display must trust the Sensor that it works correctly and only sends data that it has measured. As explained in Section 1, this type of trust in the correct functioning of a device can e.g. be achieved by trusted computing functionality. This involves a Trusted Platform Module (TPM) to be integrated in the Sensor that measures and signs the configuration of the Sensor, using a signature key certified by a trusted authority. The details of the very complex behaviour of a TPM are not the topic of this paper, thus we refer the reader to [START_REF] Mitchell | Trusted Computing[END_REF]. Using trusted computing functionality, the resulting property can be formally stated as follows: trust(Display, precede(Sensor-sense(data), Sensor-send(data)))

The resulting security properties are illustrated in Figure 4. However, as already explained, the stakeholder that requires the information to be authentic is the user rather than the Display. Thus the user has to trust in the correct functioning of the Display node. This means on the one hand that the user has to trust in that the Display node establishes its own trust into the correct functioning of the Sensor and verifies the Sensor's signature when receiving the message. This can be formalized as follows:

trust U ser, trust(Display, precede(Sensor-sense(data), Sensor-send(data))) ∧auth(Sensor-send(data), Display-rec(data), Display)

On the other hand, the user's trust in the correct functioning of the Display includes trust in the Display only showing data it has received. This can be captured with the following formalization: trust(U ser, precede(Display-rec(data), Display-show(data)))

We do not discuss here possible mechanisms that can ensure that properties 3 and 4 hold. However, in a concrete security engineering process all properties that are assumed to hold must be substantiated and evaluated e.g. by risk analysis techniques. The above two properties are illustrated in Figure 5. The resulting security property is illustrated in Figure 7.

This proves that the User can be assured that the data displayed is the same that was measured by the Sensor before. Our proof is based on two important aspects: the properties we assume the system to provide, substantiated by security mechanisms we assume the system to use, and the relations between these properties that we have proven to hold. This proof constitutes only one way to achieve this result, there are other ways that use different relations between properties which will be introduced in forthcoming papers.

Conclusions and Future Work

In this paper we have presented a formal definition of trust which reflects a simple understanding of the concept: An agent trusts in a specific property to hold in a system if it holds in its conception of the system. By integrating this formal trust concept into the SeMF Security Modeling Framework we have proven some relations between trust and specific authenticity properties. Using these we have exemplarily proven that an agent's wide-spanning authenticity property that can not be provided by current security mechanisms can be refined towards security properties that are provided by applicable security mechanisms. The refinement introduces other agents and makes use of trust relations between them. This process can be continued by substantiating certain trust assumptions through introducing further security mechanisms. Our approach has several advantages: It allows to formally prove certain security properties to hold in a system, and it extracts those trust assumptions that need to be substantiated by means beyond our formal framework (such as legal contracts). It further supports traceability: It allows to precisely identify the security properties that may be violated if a specific security mechanism is removed from the system (e.g. if the generation of a digital signature is removed because it turns out to be too slow) or if a trust assumption regarding an agent's behaviour is violated. The notion of trust is irrespective of underlying trust and security mechanisms. This makes it useful for risk analysis and management with respect to the comparison of different implementations.

We are still at the beginning of our work. Transitivity of trust for example can not be assumed to hold in general, sufficient conditions have to be found. More theorems relating trust in e.g. confidentiality, authenticity, and non-repudiation will allow to capture a wider variety of security mechanisms substantiating trust. A further interesting topic is to find conditions under which abstractions preserve certain trust properties. The aim of our work is to enable a security engineering process that takes as input a high level security property and provides as result a set of conditions to implement this property and the identification of the assumptions that need to hold.

Fig. 2

 2 Fig. 2. Discrepancy between required and provided property

Fig. 3 .

 3 Fig. 3. Security Requirement

Fig. 4 .

 4 Fig. 4. Security Properties regarding the Display

Sensor

Fig. 5 .

 5 Fig. 5. Security Properties regarding the user

⋆ Part of this work was accomplished within the project EVITA 224275 funded by the European Commission.

Finally, as explained at the beginning of this section, the User's local view keeps the action Display-show , i.e. the data being shown on the Display is visible to the user. This results in the following property: auth(Display-show(data), Display-show(data), U ser)

(5)

Reasoning with Trust

In the previous section we have discussed various mechanisms and introduced the security properties provided by mechanisms. In this section we will use the Theorems introduced in Section 6 to prove that these properties result in property P0 required to hold for our example system. Starting from Property (3) that describes the user's trust into the trusted computing and MAC mechanisms, we can apply Corollary 2 and derive the following property: trust(U ser, auth(Sensor-sense(data), Display-rec(data), Display)) [START_REF] Grandison | A survey of trust in internet applications[END_REF] Applying Corollary 1 we can conclude: trust(U ser, precede(Sensor-sense(data), Display-rec(data)))

Sensor send data sense data

Display

show data receive data U ser Fig. 6. Intermediate Proof Step This intermediate step [START_REF] Carbone | A formal model for trust in dynamic networks[END_REF] together with Property 4 is illustrated in Figure 6. Theorem 3 allows to combine these to: trust(U ser, precede(Sensor-sense(data), Display-show(data)))

Finally the application of Theorem 2 to Properties (5) and (8) implies auth(Sensor-sense(data), Display-show(data), U ser)