Claudio Gutiérrez-Soto

Gilles Hubert

Probabilistic Reuse of Past Search Results

In this paper, a new Monte Carlo algorithm to improve precision of information retrieval by using past search results is presented. Experiments were carried out to compare the proposed algorithm with traditional retrieval on a simulated dataset. In this dataset, documents, queries, and judgments of users were simulated. Exponential and Zipf distributions were used to build document collections. Uniform distribution was applied to build the queries. Zeta distribution was utilized to simulate the Bradford's law representing the judgments of users. Empirical results show a better performance of our algorithm compared with traditional retrieval.

Introduction

A wide range of approximations in information retrieval (IR) are devoted to improving the list of documents retrieved to answer particular queries. Among these approaches, we can find solutions that involve efficient assignments of systems to respond to certain types of queries, by applying data mining techniques [START_REF] Bigot | Fusing different information retrieval systems according to query-topics: a study based on correlation in information retrieval systems and trec topics[END_REF]. Nonetheless, some tasks of data mining can imply not only long periods of time, but also a high cost in money [START_REF] Gray | Present and future directions in data warehousing[END_REF]. In addition, solutions that involve an exhaustive analysis of all possible alternatives to find the best answer to a query (i.e., the best precision for each type of query) can be found in IR context. Prior solutions correspond to approaches based on learning techniques (e.g., neural networks, genetic algorithms, and machines support vectors). However, these approaches should imply a high cost in learning time as well as diverse convergence times when the datasets used are heterogeneous [START_REF] Nopiah | Time complexity analysis of the genetic algorithm clustering method[END_REF]. Additionally, characteristics, such as the scopes where these types of algorithms are applied and the performance achieved in different environments, are complex to address [START_REF] Kearns | The Computational Complexity of Machine Learning[END_REF].

In the IR literature, two types of approaches used in the context of past queries are easily identifiable. The first approaches are based on TREC collections. Most of these approaches use simulation to build similar queries with the aim to provide a suitable framework of evaluation. The second type of approaches rooted in the use of historical queries on the Web, most of which are supported on repetitive queries. As a result, having ad-hoc collections which allow to evaluate the use of past queries in an appropriate way, is a hard task. Therefore, one way to provide an ad-hoc environment for approximations based on past queries is simulation.

Our main contribution is a Monte Carlo algorithm, which uses relevant documents from the most similar past query to answer a new query. The algorithm splits the list of retrieved documents from the most similar past query in subsets of documents. Our algorithm is simple to implement and effective. Moreover, it does not require learning time. Documents, query collections, and relevance judgments of users were simulated to built a dataset for evaluating the performance of our algorithm. A wide range of experiments have been carried out. We have applied the Student's paired t-test to support the experimental results. Empirical results show better results of our algorithm (in particular the precision P@10) than traditional retrieval.

The paper is organized as follows. In section 2, related works on past searches, randomized algorithms, and simulation in IR context are presented. In section 3, we present our approach to simulate an IR collection, in the context of past search results. Section 4 details our approach using past search results, with mathematical definitions. In section 5, empirical results are described. Finally, conclusions are presented in section 6.

Related Work

Two categories of approaches employed in the context of past queries are easily identifiable. The first category is based on TREC collections. In a recent work [START_REF] Cetintas | Using past queries for resource selection in distributed information retrieval[END_REF], a distributed approach is presented in the context of past queries. Similar queries are simulated from a traditional set of queries. Moreover, the judgments of users are omitted. In [START_REF] Shen | Exploiting query history for document ranking in interactive information retrieval[END_REF], two strategies aiming at improving precision were implemented. The first strategy corresponds to the combination of results from previous queries, meanwhile the second implies the combination of query models. An extended work is exposed in [START_REF] Shen | Context-sensitive information retrieval using implicit feedback[END_REF]. The authors address models based on implicit feedback information to increase precision. Implicit feedback information is given by queries and clickthrough history in an active session. It is important to emphasize that TREC collections used here have been modified to evaluate approximations based on past queries.

The second category of approaches focuses on log files in the context of the Web. In [START_REF] Fonseca | Using association rules to discover search engines related queries[END_REF], an automatic method to produce suggestions based on previously submitted queries is presented. To achieve this goal, an algorithm of association rules was applied on log files. The 95 most popular queries were considered. Nonetheless, the percentage of these 95 queries over 2.3 millions of records is unknown. Hence, it is infeasible to estimate the impact of this approximation. Moreover, [START_REF] Baeza-Yates | Query recommendation using query logs in search engines[END_REF] claims that there is no easy way to calculate the real effect of approximations founded on association rules. It is mainly due to the complexity to determine the successive queries that belong to the same session (i.e., for the same user). In [START_REF] Teevan | Information re-retrieval: repeat queries in yahoo's logs[END_REF], an approximation based on repeated queries is exposed. The aim is the identification of identical queries executed in the same trace. In [START_REF] Garcia | Search Engine Optimisation Using Past Queries[END_REF], two contributions, which take advantages from repeated queries, are presented. The first contribution is aligned on efficiency in execution time and the second is focused on repetitive document access by the search engines. Simulation to evaluate information retrieval systems (IRSs) is presented as a novel branch of research [START_REF] Clough | Evaluating the performance of information retrieval systems using test collections[END_REF]. Simulation in IR is an automatic method, where documents, query collections, and judgments of users can be built without user intervention [START_REF] Huurnink | Validating query simulators: An experiment using commercial searches and purchases[END_REF].

In addition, the IR literature is crammed with contributions based on probabilistic algorithms. The major part of probabilistic algorithms in IR can be categorized in two classes, learning techniques and optimization. Typically, approximations rooted in learning techniques involve the use of Bayesian Networks and their variants. The PrTFIDF algorithm, which is a probabilistic version of TFIDF algorithm is presented in [START_REF] Joachims | A probabilistic analysis of the rocchio algorithm with tfidf for text categorization[END_REF]. PrTFIDF provides a new vision of vector space model, where the theorem of total probability, the Bayes' theorem, and a descriptor for every document are used. Final results show a better performance than TFIDF. In [START_REF] Chan | Probabilistic modeling for information retrieval with unsupervised training data[END_REF], the classification of documents in an unsupervised manner is carried out. It uses Poisson distribution according to the query or topic.

Several optimization techniques involve the use of Genetic Algorithms (GA). Inspired by the formula proposed by Salton [START_REF] Salton | Readings in information retrieval[END_REF] (where the term weights for documents and queries are the product between the term frequency multiplied by an inverse collection frequency factor), a new fitness function is presented in [START_REF] Radwan | Using genetic algorithm to improve information retrieval systems[END_REF]. Both, vectors of documents and queries are normalized by using the formula. Experimental results show better effectiveness when using this approach than traditional retrieval (i.e., using cosine distance). Eventually, the Probfuse algorithm proposed in [START_REF] Lillis | Probability-based fusion of information retrieval result sets[END_REF], whose aim is to combine results from several IR algorithms, outperforms the widely used CombMNZ algorithm.

Different to Bayesian Networks and GA, Monte Carlo and Las Vegas algorithms are used usually when the problem is hard to solve like NP problems or when algorithm input is non-deterministic. Las Vegas algorithms provide an answer, which is always correct and where in the worst case the execution time is the same as the deterministic version. In contrast to Las Vegas algorithms, Monte Carlo algorithms give an answer, which can be incorrect (i.e., the algorithm returns true, when the answer should be false, or vice-versa). When one of these answers is correct, it is called true-biased (the correct answer is true) or false-biased (the correct answer is false). When both answers can be incorrect, it is called two-sided errors.

Our Monte Carlo algorithm corresponds to the type two-sided errors. This is due to the fact that we are not sure about judgments of users with respect to whether a document is either relevant or not relevant regarding the query. Nonetheless, we assume that documents that appear at the top of the result list have more probability to be relevant than documents that appear at the bottom of the list.

Simulating IR Collections

Our method consists of two steps, based on prior work [START_REF] Gutiérrez-Soto | Evaluating the interest of revamping past search results[END_REF]. The first step aims at creating terms, documents, and queries. Both Heaps' and Zipf's laws are considered to build document collections. We assume that both processes, elimination of stop words, and stemming were carried out. Due to terms which compose a document can belong to several subjects, Zipf's law is applied to select terms from topics [START_REF] Poosala | Zipf's law[END_REF]. Exponential distribution can be applied as an alternative to Zipf's law. Then, past queries are created from documents and new queries are built from past queries. In the final step, to simulate judgments provided by users about relevance of documents for a specific query, Bradford's law is applied [START_REF] Garfield | Bradford's Law and Related Statistical Patterns[END_REF].

The most basic element that composes a document is a term. A term is composed of letters from the English alphabet. Both documents and queries are composed of terms. Each document is unique. Past queries are built from documents and their intersections are empty. A topic (i.e., subject of documents) is defined by terms. Several topics are used to built a document. The intersection among topics is empty. Aiming to build documents, Zipf and Exponential distributions are used to select terms from different topics. Uniform distribution is used to select documents, where terms are selected to built the past queries. Then, past queries are built from the documents. New queries are made up from past queries by either adding a new term or deleting a term. Bradford's law has been applied through Zeta distribution. In order to explain the mechanism to obtain the precision, we can assume two lists of documents. The first list of documents (for the query 1) is composed of the documents d 1 (1), d 3 (1), d 5 (1), d 6 (0), d 8 (0), d 9 (0) where d i (1) is a relevant document, meanwhile d i (0) is irrelevant. In the same way, the second list of documents is composed by the documents d 2 (0), d 3 (1), d 5 (1), d 6 (0), d 7 (1), d 10 (0). Thus, first, a subset of common documents is found (d 3 , d 5 and d 6 ). Second, from the common subset, relevant documents are determined for both queries by using Bradford's law (d 3 and d 5 ). Third, Bradford's law is applied for each list by conserving the relevant documents that belong to the common subset (for the first list d 1 , d 3 and d 5 are relevant documents). As a consequence, the precision (in our case P@10) is different for both queries.

Retrieval Using Past Queries

At the beginning, each submitted query is saved with its documents. Afterwards, each new query is compared with the past queries stored in the system. If there is a past query quite similar, then the relevant documents are retrieved from the most similar past query using our algorithm. Broadly speaking, our algorithm divides the list of documents retrieved from the past query, in groups of power two. For example, if the list of documents comprises 30 documents, the number of documents will be rounded up to the next number in power two, i.e., n = 32. Later on, groups of documents are defined as follows. The first group comprises 2 0 documents. The second group involves 2 1 documents, the third group is composed of 2 2 documents, and so on, in such a way that the sum of the documents does not outperform n = 32. Thus, the number of groups is 5. The biggest group is composed of documents that appear in the first positions (between the position 1 and 16). The next biggest group comprises documents that appear from the position 17 to 24, and so on. The likelihood of a document to be relevant is determined by two factors: the group it belongs to and its position in the group. The algorithm and a more detailed example are displayed in the next sections.

Definitions and Notations

Let DB be an IR dataset, composed of a set of documents D, and a set of past queries Q. Besides, let Q ′ be the set of new queries. V N (q) is a set of N retrieved documents given q, and sim(q, d j ) is the cosine distance between query q and the document d j . Besides, V N (q) = A(q) ∪ A ′ (q), where A(q) corresponds to the set of all relevant documents for the query q. A ′ (q) is the set all irrelevant documents for the query q. C = c(q, V N (q)) is the set of all retrieved documents with their respective queries. Definition 1. ∂ : R c (q ′ ) → A(q ′ ) is a function, which assigns the most relevant documents to the new query q ′ , such as q ′ ∈ Q ′ and R c (q ′ ) corresponds to a set of retrieved documents, from the most similar past query. (see Definition 2 and Definition 4).

In addition, let x be the integer part of a real number x, ⌈x⌉ corresponds to the upper integer of x and ⌊x⌋ corresponds to the lower integer of x. B[N ] is a binary array such as B has N elements, and a b is the proportion of values in B (see Algorithms 1, lines from 9 to 12), which have the value 1 (true). This array is the base to provide a level of general probability for all documents. Nevertheless, the probability of each document according to the position in V N (q), is computed by the Algorithm 1.

Definition 2. M (N ) = min{m | m ∈ N∧ m k=0 2 k ≥ N ∧N < 2 m+1
} be the upper bound set, which involves documents of V N (q)(in power two) (see Algorithm 1, lines from 2 to 4). Definition 3. Let i be the position of a document in V N (q), such as the first element (i = 1) represents the most similar document, then

f x (i, N ) = min{x | x ∈ N ∧ i ≤ x k=1 2 M (N )
2 k }, corresponds to the number of set assigned for the document i (see Algorithm 1, line 5).

Definition 4. Let v(i, N ) = (2 M(N )-f x (i,N ) -1) -[ ( f x (i,N ) k=1 2 M(N )-k ) -i mod(2 M(N )-f x (i,N ) )] be the value assigned to i, from 0 to 2 M(N )-f x (i,N ) (see Algorithm 1, line 15). Definition 5. Φ(i, N ) = log 2 (2 M(N )-f x (i,N ) -v(i, N )) -log 2 (2 M(N )-f x (i,N ) - v(i, N )) a decimal number, which is [0, 1[ (see Algorithm 1, lines from 16 to 19). Definition 6. Let K(i, N ) = ⌈Φ(i, N )⌉ * M (N ) -f x (i, N ) : if Φ(i, N ) ≥ 0.5 ⌊Φ(i, N )⌋ * M (N ) -f x (i, N )
: if Φ(i, N ) < 0.5 be the number of iterations to look for a hit in the array B (see Algorithm 1, lines from 20 to 25).

Thus, β : F (i) → {0, 1}, is the hit and miss function.

F (i) = 1 : P r i (1) = K(i,N ) l=1 2 M (N )-f x (i,N ) (2 M (N ) ) l , 0 : P r i (0) = 1 -P r i (1)
where P r i (1) is the probability of a hit (1), and P r i (0) corresponds to the probability of a miss (0) for the element i.

Our algorithm works as follows. The list of retrieved documents is split in subsets of elements in power two. In our case, V N (q) has 30 documents, however it can be approximated to 32 documents. Thus, if we apply Definition 2, then M (N ) = 5. Therefore, V N (q) is split in 5 subsets. In general terms, P r i (1) for every subset is different. Specifically on 2 M (N )-f x (i,N )

(2 M (N ) )
. Thus, the space of possible candidates for the first subset is 2 5-1)

(2 5 ) = 1 2 , for the second subset is 2 5-2) (2 5 ) = 1 4 and so on. To show how the probability decreases according to the subsets, two examples are provided, for the first subset and the third subset. The second element of the first subset is i = 2, thus applying the Definition 3, (2 5 ) l = 0.757. In the same way, v(26, 30) = (2 5-3 -1) -[ (16 + 8 + 4) -26 ) mod 2 5-3 ] = 1. Finally, P r 26 (1) = 2 l=1 2 5-3 (2 5 ) l = 0.128 5 Experiments

f x (2, 30) = 1, therefore, v(2, 30) = (2 5-1 -1) -[ ( 1 k=1 2 5-1 ) -2 ) mod 2 5-1 ] = 1 (see Definition 4

Experimental Environment and Empirical Results

The experimental environment was instantiated as follows. The length of a term is between 3 and 7. The length was determined using Uniform distribution. The total number of terms used in each experiment corresponds to 800. A document can contain between 15 and 30 terms. The number of topics used in each experiment is 8. Each topic is defined by 100 terms. Each experiment used 800, 1600, 2400, 3200, and 4000 documents. Terms for a query were between 3 and 8. We built 15 past queries from documents. From the set of past queries, 15 new queries were built. Thereby, we used 30 distinct queries. Simulations were implemented on C language and run on Linux Ubuntu 3.2.9, with Centrino 1350, 1.8 Ghz Intel processor, 1GB RAM, and gcc 4.6.3 compiler.

Three experimental scenarios were defined. For the first and second experiments, Exponential distributions (with parameters θ = 1.0 and θ = 1.5 ) were Algorithm 1. B[N ], A P ast (q), V N (q), q ′ Require: B[N ] is a boolean array, A P ast (q) is a set of relevant documents for the query q, V N (q) is the set of retrieved documents for the query q, q ′ is the most similar query for q Ensure: A New (q ′ ) is a set of relevant documents for the query q ′ 1: A New (q) ← ∅ 2: for i ← 0, sum ← 0, sum < N + 1 do 3: sum ← sum + 2 i 4: end for 5: k ← i -1 6: for i ← 1, N do 7: if ([idDoc = P osition(l of V N (q))] is in A P ast (q)) then 33: applied to build the collection of documents D. In the third experiment, Zipf distribution (with parameter θ = 1.6) was applied to build D. Simulations of user judgments were carried out under Zeta Distribution. Zeta distribution with parameters 2, 3, and 4 were applied on the 30 most similar documents with respect to the queries. Besides, the Student's Paired t-Test (Two Samples test) over each average P@10 (our approach with respect to traditional retrieval) were used to support the results. Final results are summarized and displayed in Table 1.

B[i] ← f
A New (q ′ ) ← A New (q ′ ) ∪ d idDoc 34: l ← l +

Discussion

Accepted ranges for Zipf's law regarding the distribution of word frequencies in a vocabulary are between 1.4 and 1.8. In our experiments, Zipf distribution was used with value 1.6 to select terms from topics. It is important to emphasize that every time the parameter S of Zeta distribution (to apply Bradford's law) was incremented, both averages of P@10, using Past Result (i.e., our approach) and Cosine (i.e., traditional IR) declined similarly. Additionally, if the number of queries was increased in the experiments, it should not have different final results. This is because for every past query it exists just one and unique query for which the intersection is not empty. Also, the final results show that increasing the number of documents have no impact on the significance test p-values.

Conclusions

In this paper, a new Monte Carlo algorithm for information retrieval using past queries have been presented. It is easy to implement, does not require time to learning, and provides acceptable results improving precision (i.e., P@10). Furthermore, this algorithm can be implemented not only inside an information retrieval system but also as external interface outside search engines. This algorithm relies on reuse of relevant documents retrieved from the most similar past query. In addition, different evaluation scenarios have been simulated. Simulation provides two advantages. First, it provides an ideal environment to evaluate our algorithm. Second it makes possible to build not only document and query collections but also relevance judgments for documents given a query. Empirical results showed better precision (P@10) of our algorithm compared with traditional retrieval.

  ). Applying Definition 5. Φ(2, 30) = log 2 (2 5-1 -1)log 2 (2 5-1 -1) = 3.906 -3 = 0.906. Applying Definition 11, K(2, 30) = ⌈Φ(2, 30)⌉ * 5 -1 = 1 * 4 = 4.Thus, P r 2 (

Table 1 .

 1 Results comparing our approach of reusing past queries with cosine distance

	Experiment	Relevance simulation	Percentage of	Average
	Distribution to build	Zeta distribution	improved queries improvement
	collection D	with parameter S	(Measure: P@10)
	Experiment 1	S = 2	83 %	+21 %**
	Exponential distribution	S = 3	74 %	+17 %**
	(with parameter θ = 1.0)	S = 4	65 %	+20 %**
	Experiment 2	S = 2	77 %	+17 %**
	Exponential distribution	S = 3	73 %	+18 %**
	(with parameter θ = 1.5)	S = 4	65 %	+16 %**
	Experiment 3	S = 2	85 %	+21 %**
	Zipf distribution	S = 3	84 %	+18 %**
	(with parameter θ = 1.6)	S = 4	77 %	+23 %**
	** p-value<0.01 (two sample t-test).


Brahim Hamid
email: hamid@irit.fr

Christian Percebois
email: percebois@irit.fr

A Modeling and Formal Approach for the Precise Specification of Security Patterns

Keywords: Pattern, Metamodel, Domain, Formalization, Model-Driven engineering, Security

Non-functional requirements such as Security and Dependability (S &D) become more important as well as more difficult to achieve. In fact, the integration of security features requires the availability of both application domain specific knowledge and security expertise at the same time. Hence, capturing and providing this expertise by the way of security patterns can support the integration of S&D features by design to foster reuse during the process of software system development.

The solution envisaged here is based on combining metamodeling techniques and formal methods to represent security pattern at two levels of abstraction fostering reuse during the process of pattern development and during the process of pattern-based development. The contribution of this work is twofold: (1) An improvement of our previous pattern modeling language for representing security pattern in the form of a subsystem providing appropriate interfaces and targeting security properties, (2) Formal specification and validation of pattern properties, using the interactive Isabelle/HOL proof assistant. The resulting validation artifacts may mainly complete the definitions, and provide semantics for the interfaces and the properties in the context of S&D. As a result, validated patterns will be used as bricks to build applications through a Model-Driven engineering approach.

Introduction

Recent times have seen a paradigm shift in terms of design by combining multiple software engineering paradigms, namely, Model-Driven Engineering (MDE) [START_REF] Schmidt | Model-Driven Engineering[END_REF] and formal methods [START_REF] Zhang | A MDE Based Approach for Bridging Formal Models[END_REF]. Such a paradigm shift is changing the way systems are developed nowadays, reducing development time significantly. Embedded systems [START_REF] Zurawski | Embedded Systems[END_REF] are a case where a range of development approaches have been proposed. The most popular are those using models as main artifacts to be constructed and maintained. In these approaches, software development consists of model specification and transformations. In addition to MDE, pattern-based development has gained more attention recently in software engineering by addressing new challenges that were not targeted in the past. In fact, they are applied in modern software architecture for distributed systems including middlewares, real-time embedded systems, and recently in security and dependability engineering.

Unfortunately, most of security patterns are expressed as informal indications on how to solve some security problems, using template like traditional patterns [START_REF] Alexander | A Pattern Language[END_REF][START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF]. These patterns do not include sufficient semantic descriptions, including those of security and dependability concepts, for automated processing within a tool-supported development and to extend their use. Furthermore, due to manual pattern implementation, the problem of incorrect implementation (the most important source of security problems) remains unsolved. For that, model driven software engineering can provide a solid basis for formulating design patterns that can incorporate security aspects and for offering these patterns at several levels of abstraction.

In this paper, we leverage on this idea to propose a new framework for the specification and the validation of security patterns intended for systems with stringent security requirements. Reaching this target requires to get a common representation of such a modeling environment for several domains and the ability to customize them for a specific domain. Here we propose two additional and complementary types of representations: a semi-formal representation through metamodeling techniques and a rigorous formal representation through interactive theorem proving approaches. Regarding the comparison with documentation template [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF] (informal representation) used to represent security patterns, our proposition is based on it. However, we keep the template elements in the form of attributes and we deeply refine them by the definition of new concepts in order to fit with security engineering needs. In this vision, a security or (in general an S&D) pattern is a subsystem exposing pattern functionalities through interfaces and targeting security properties. As it follows the MDE paradigm for system's design, using patterns on different levels of abstraction, it allows for integration into the system's design process, hence supports this process. To this end, the proposed representation takes into account the simplification and the enhancement of such activities, namely: selection/search, based on the classified properties, and integration, based on a high level description of interfaces.

The rest of this paper is organized as follows. An overview of the modeling approach we proposed including a set of definitions is presented in Section 2. Then, Section 3 presents the pattern modeling language and illustrates the pattern modeling process in practice. Section 4 presents the validation process through the example of the secure communication pattern. In Section 5, we review most related works addressing pattern specification and validation. Finally, Section 6 concludes this paper with a short discussion on future works. An appendix is added with the Isabelle/HOL code of our experiment.

The Nature of Patterns within PBSE (Pattern-Based System and software Engineering)

Usually, pattern design artifacts are provided as a library of models (subsystems) and as a system of patterns (framework) in the more elaborated approaches. However, there are still lacks in existing modeling languages and/or formalisms dedicated to model these design artifacts and the way how to reuse them in software development automation. The supporting research activities examine three distinct challenges: mining -discovering patterns from existing systems, hatching -selection of the appropriate pattern and application -effective use during the system development process.

In our work, we study only the two last challenges, targeting the (i) development of an extensible design language for modeling patterns for secure and dependable distributed embedded systems and (ii) a methodology to improve existing development processes using patterns. The language has to capture the core elements of the pattern to help its (a) precise specification, (b) selection and (c) integration. Supporting research tackles the presented challenges includes domain patterns, pattern languages and recently formalisms and modeling languages to foster their application in practice.

Here, we propose a novel approach to improve the security pattern representation by the combination of semi-formal semantics and rigorous formal semantics of some of its concepts.

Motivational Example: Secure Communication Pattern (SCP)

As example of a common and a widely used patterns we choose the Secure Communication Pattern referred to in the following as SCP. Messages passing across any public network can be intercepted. The problem is how to ensure that data being across this system is secure in transit. In other words, how to guarantee data authenticity. This is one of the goal to use the SCP.

However, those SCP are slightly different with regard to the application domain. For instance, a system domain has its own mechanisms and means to serve the implementation of this pattern using a set of protocols ranging from SSL, TLS, Kerberos, IPSec, SSH, WS-Security and so on. In summary, they are similar in the goal, but different in the implementation issues. So, the motivation is to handle the modeling of security patterns by following abstraction. In the following, we propose to use SSL mechanisms 1 to specialize the implementation of the SCP.

The establishment of a secure channel is composed of two phases. First, the client informs the server of the cryptographic algorithms it can handle. The actual choice is always made by the server, which reports its choice back to client. In the second phase, authentication takes place. The server is required to authenticate itself. It sends a certificate containing its public key signed by a certification authority CA to the client. In order to authenticate the client by the server, the client has to send a certificate to the server as well. The client generates a random number that will be used by both sides for building a session key, and sends this number to the server, encrypted with the server's public key. In the case of client required authentication, the client signs the number with its private key. At that point, the sever can verify the identity of the client, after which the secure channel can be established.

Definitions and Concepts

In [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF], a design pattern abstracts the key artifacts of a common design structure that make it useful for creating a reusable object-oriented design. Several generalizations on this basis to describe software design patterns in general are proposed in literature. We quote the following definition of security patterns from [START_REF] Schumacher | Security Engineering with Patterns[END_REF]: Definition 1 (Security Pattern). A security pattern describes a particular recurring security problem that arises in specific contexts and presents a well-proven generic scheme for its solution.

Security patterns are not only defined from a platform independent viewpoint (i.e. they are independent from the implementation), they are also expressed in a consistent way with domain specific models. Consequently, they will be much easier to understand and validate by application designers in a specific area. To capture this vision, we introduced the concept of domain view. Particularly a security pattern at domain independent level exhibits an abstract solution without specific knowledge on how the solution is implemented with regard to the application domain.

Definition 2 (Domain).

A domain is a field or a scope of knowledge or activity that is characterized by the concerns, methods, mechanisms, ... employed in the development of a system. The actual clustering into domains depends on the given group/community implementing the target methodology.

In our context, a domain represents all the knowledge including protocols, processes, methods, techniques, practices, OS, HW systems, measurement and certification related to the specific domain. With regard to the artifacts used in the system under development, we will identify the first classes of the domain to specialize such artifacts. For instance, the specification of a pattern at domain independent point of view is based on the software design constructs. The specialization of such a pattern for a domain uses a domain protocol to implement the pattern solution (see example of secure communication pattern given in Section 3.2.1 and Section 3.2.2).

The objective is to reuse the domain independent model security patterns for several industrial application domain sectors and also let them be able to customize those domain independent patterns with their domain knowledge and/or requirements to produce their own domain specific artifacts. Thus, the 'how' to support these concepts should be captured in the specification languages.

Pattern Modeling Process

We now present an overview of our pattern specification process. Along this description, we will give the main keys to understand why our process is based on a general and a constructive approach. We begin with our pattern specification metamodel.

Pattern Specification Metamodel (SEPM)

To foster reuse of patterns in the development of critical systems with S&D requirements, we are building on a metamodel for representing security pattern in the form of a subsystem providing appropriate interfaces and targeting security properties to enforce the S&D system requirements. Interfaces will be used to exhibit pattern's functionality in order to manage its application. In addition, interfaces support interactions with security primitives and protocols for the specialization for a specific application domain. The principal classes of the System and Software Engineering Pattern Metamodel (SEPM) [START_REF] Hamid | Enforcing S&D Pattern Design in RCES with Modeling and Formal Approaches[END_REF] are described with Ecore notations in Figure 1. Their meanings are more detailed in the following paragraphs. -SepmPattern. This block represents a security pattern as a subsystem describing a solution for a security particular recurring design problem that arises in specific design context. A SepmPattern defines its behavior in terms of provided and required interfaces. Larger pieces of a system's functionality may be assembled by reusing patterns as parts in an encompassing pattern or assembly of patterns, and wiring together their required and provided interfaces.

A SepmPattern may be manifested by one or more artifacts. -SepmDIPattern. It is an SepmPattern denoting some abstract representation of a security pattern at domain independent level. This is the key entry artifact to model patterns at domain independent level (DIPM). -Interface. A SepmPattern interacts with its environment with Interfaces which are composed of Operations. A SepmPattern owns provided and required interfaces. A provided interface highlights the services exposed to the environment. A required interface corresponds to services needed by the pattern to work properly. We consider two kinds of interface:

• External interface. Allows implementing interaction with regard to the integration of a pattern into an application model or to compose patterns. • Technical interface. Allows implementing interaction with security primitives and protocols, such as encryption, and specialization for specific underlying software and/or hardware platforms, mainly during the deployment activity. Please note, a SepmDIPattern does not have TechnicalInterfaces. -Property. Is a particular characteristic of a pattern related to the concern it is dealing with and dedicated to capture its intent in a certain way. For instance, security properties. Each property of a pattern will be validated at the time of the pattern validating process and the assumptions used, will be compiled as a set of constraints which will have to be satisfied by the domain application. -SepmDSPattern. Is a refinement of a SepmDIPattern. It is used to build a pattern at at domain specific level (DSPM). Furthermore a SepmDSPattern has Technical Interfaces in order to interact with the platform. This is the key entry artifact to model pattern at DSPM.

Specification Process

We propose an iterative specification process consisting of the following phases: (1) the specification of the pattern at domain independent level (DIPM), (2) the refinement of DIPM pattern to specify one of its representations at domain specific level (DSPM). These two levels of the secure communication pattern presented in Section 2.1 are illustrated. For the sake of clarity, many functions and artifacts of this pattern have been omitted. We only detail the properties and interfaces that we need to describe the validation process. Note that the artifacts representing the formalization and the proof are detailed in Section 4. The first step in our specification process is the understanding of the pattern's informal representation. The target representation is the SEPM metamodel, simplified in Figure 1 for the purpose of our study (semi-formal and formal representation of security pattern). The informal description given in Section 2.1 reflects our understanding from the representation of secure communication pattern given in literature [START_REF] Schumacher | Security Patterns: Integrating Security and Systems Engineering[END_REF]. At the DIPM level this description reveals the following elements: interfaces of type SepmEx-ternalInterface and security properties of type SepmProperties. At the DSPM level, the description reveals the following elements: interfaces of type SepmExternalInterface and SepmTechnicalInterface and security properties of type SepmProperties. The description with varying levels of abstraction is managed by inheritance. Once there is a good understanding of the pattern informal representation structure, the pattern can be specified using the SEPM metamodel. The first step is to create an instance of SepmPattern. The instance is given a set of attributes representing the pattern. In our example, an instance of SepmPattern is created and named 'SecureCommPattern'.

Once the basic pattern subsystem has been specified, interfaces are added to expose some of the pattern's functionalities. For each such interface, an instance of SepmExter-naInterface is added to the pattern's interfaces collection. The next step after creating interfaces is the creation of properties instances. An instance is created in the pattern's properties collection to specify every identified security property. A property is given a name and an expression on external interfaces in a property language. A complete specification of this pattern at both DIPM and DSPM levels is described below.

Domain Independent Pattern Model (DIPM).

At DIPM level, the security pattern subsystem and its related elements are created by inheritance. In our example, the DIPM of the secure communication pattern consists of:

-External Interfaces. The secure communication pattern exposes its functionalities through an external interface offering the following function calls:

- -Properties. At this level, we specify the security property: "authenticity of sender and receiver". We denote this property as auth(Send(C, S, ch(C, S), m), Receive(S, C, ch(C, S), m), S) where the server S invokes the primitives Send(C, S, ch(C, S), m) and Receive(S, C, ch(C, S), m).

Send(P, Q, ch(P, Q), m), -Receive(P, Q, ch(P, Q), m), with P, Q ∈ {C, S}, ch(C, S) = ch(S,

Domain Specific Pattern Model (DSPM).

At DSPM level, the security pattern and some of its related elements are also created by inheritance. Once a SEPMDSPAT-TERN is created, every pattern external interface is identified and modeled as a refinement of the SEPMEXTERNALINTERFACE in the pattern's interfaces collection. Then, each of the pattern's technical interface is identified and modeled by an instance of SepmTechnicalInterface in the pattern's interfaces collection. The next step is the specification of properties. Each property is represented by an instance of SepmProperty in the pattern's properties collection. A property is given a name and an expression on external and technical interfaces in a property language. For instance, when using SSL as a mechanism related to the application domain to refine the secure communication pattern at DSPM, we manage the following artifacts:

-External Interfaces. The DS external interface, a refinement of the DI external interface, can be specified as follows:

- -Technical Interfaces. The most important functions of the DS technical interface of the SSL pattern can be specified as follows:

-genRand(C, R C ), genRand(S, R S ): Client/server generate a random number.

verif yCert(): Client/server verify each others certificate and extract the respective public key.

encrypt(C, pubKey S , R C ): The client encrypts its random number using the server's public key.

sign(C, . . .): The client signs the SSL handshake messages.

verif ySig(S, . . .): The server verifies the client's signature.

-genM ac(C, macKey C , m, mac C (m)): The client generates the MAC for message m using its own SSL shared secret for MAC generation.

verif yM ac(S, macKey C , m, mac C (m)): The server verifies, using its shared secret for MAC verification (i.e. the client's key for MAC generation), that the MAC for m is correct and thus originates from the client.

send(), recv(): Send and receive of the SSL messages by client and server, respectively.

-Properties. In addition to the refinement of the authenticity property identified in the DIPM, at this level we may identify some related resource properties, e.g. the size of the cryptographic key.

Pattern Validation Process

We propose to use the interactive Isabelle/HOL proof assistant [START_REF] Nipkow | Isabelle/HOL[END_REF] for formalizing security patterns. The formal specification and verification of a pattern is represented through an Isabelle theory. It consists of a set of types, functions and theorems. In some situations, intermediate lemmas have been introduced in order to simplify what we have to prove. We have defined a set of transformation rules to map the pattern metamodel concepts onto those of Isabelle/HoL. In our case, we focus on interfaces and properties. These interfaces provide functionalities through function calls that are encoded as actions whose parameters are agents and data. On the other side, pattern properties denote some expected outcomes over these actions. A property is given a name and an expression on agents and actions. Sometimes a property may refer to another property.

Each concept involved in the modeling of interfaces and properties is translated in Isabelle as an abbreviation, i.e. a new name for an existing construction, using data-types, records and definitions. For instance, the record action and the abbreviation createAction allow to create the Send and Receive actions. Following this definitional approach, we build the pattern specification from the bottom.

The designer can then extend this theory by verifying properties using the Isabelle scripting language for writing proofs using tactics. The goal now is to identify the set of assumptions required to prove the properties. Then, the proof consists to find a scheduling of valid steps using Isabelle's tactics such as applying a simplification considering that each step corresponds to a sub-goal to resolve (command apply). Our proof only uses simplification rules which consist in rewriting specified equations from left to right in the current goal (command simp).

Correctness of the proof is guaranteed by construction from the first goal to resolve (a lemma or a theorem) until the message "no sub-goals" is produced by the framework which confirms that the proof is finished (command done). For instance, to prove the authenticity property expressed as the goal lemma authSendReceive : ′′ auth Send Receive server ′′ with respect to the definition auth, each subgoal auth, Send, Receive, . . . is rewritten according to its definition.

In the following, we apply the formalization and the verification processes to both DIPM and DSPM levels, and then we present the poof that the DIPM is an abstraction of the DSPM. The definitions introduced below are extracted from the code of our experiment. Definitions mainly concern the refinement process of SCP from the DIPM model to the DSPM model, using the SSL mechanism for the application domain.

Pattern Formalization

We first introduce the main concepts of authenticity, precedence and trust that are relevant for SCP. We call a particular action a authentic for an agent P after a sequence of actions if in all sequences that P considers to have possibly happened a must have happened. This is modeled by the auth(a, b, P ) predicate which denotes that whenever a particular action b has happened, it must be authentic for agent P that action a has happened as well. In the same way, precede(a, b) holds if all action sequences in the system's behavior that contain an action b also contain an action a. Finally, trust(P, prop) means that P trusts a property prop to hold in the system if the property holds in the agent's conception of the system. The following gives types for these predicates in Isabelle.

auth :: ′′ action => action => agent => bool ′′ precede :: ′′ action => action => bool ′′ trust :: ′′ agent => property => bool ′′ Before encoding the authenticity relation in Isabelle/HOL, one has to define what are an action, an agent and a property. All three are records i.e. tuples, with a name attached to each component. They will be independently introduced when defining the DIPM and DSPM pattern models respectively in Figure 2 and Figure 3.

1 : r e c o r d a c t i o n = a g e n t 1 : : " a g e n t T y p e " a g e n t 2 : : " a g e n t T y p e " c h a n n e l : : " f u n c t o r T y p e " me s s a g e : : " messageType " 2 : d e f i n i t i o n c r e a t e A c t i o n : : " a g e n t T y p e ==> a g e n t T y p e ==> f u n c t o r T y p e ==> messageType ==> a c t i o n " where " c r e a t e A c t i o n a1 a2 c a me== a g e n t 1 =a1 , a g e n t 2 =a2 , c h a n n e l =ca , m e s s a g e =me" 3 : d e f i n i t i o n Send : : " a c t i o n " where " Send == c r e a t e A c t a c t i o n s : : " a c t i o n s e t " p r o p e r t i e s : : " p r o p e r t y s e t " 1 0 : d e f i n i t i o n c r e a t e A g e n t : : " a g e n t T y p e == >( a c t i o n s e t )== >( p r o p e r t y s e t )== > a g e n t " where " c r e a t e A g e n t a a s p s == name=a , a c t i o n s = as , p r o p e r t i e s = p s " 1 1 : d e f i n i t i o n c l i e n t : : " a g e n t " where " c l i e n t == c r e a t e A g e n t C { Send } { } " 1 2 : d e f i n i t i o n s e r v e r : : " a g e n t " where " s e r v e r == c r e a t e A g e n t S { Send , R e c e i v e } { p r e c e d e S e n d R e c e i v e } " 1 3 : d e f i n i t i o n a u t h : : " a c t i o n ==> a c t i o n ==> a g e n t ==> b o o l " where " a u t h a1 a2 a == a1 IN ( a c t i o n s a ) AND a2 IN ( a c t i o n s a ) " 1 4 : d e f i n i t i o n t r u s t : : " a g e n t ==> p r o p e r t y ==> b o o l " where " t r u s t a p == p IN ( p r o p e r t i e s a ) " 1 5 : d e f i n i t i o n a u t h I f T r u s t : : " a c t i o n ==> a c t i o n ==> a g e n t ==> b o o l " where " a u t h I f T r u s t a1 a2 a == t r u s t a ( p r e c e d e a1 a2)-> a u t h a1 a2 a " Fig. 2. The DIPM formalization of the Secure Communication Pattern

Domain Independent Pattern Model (DIPM).

As previously defined in Section 3.2.1, the secure communication pattern exposes its functionalities through the two primitives Send and Receive. Applying the previous definition auth, we have to define these two primitives at the DIPM level. Figure 2 highlights the corresponding formalization in Isabelle owing to the createAction definition and the Send and Receive constants (lines 2-4). In the same way, an agent is introduced by the createAgent definition and the subject constant nominates the active computational entity of the pattern (line 10). The modeled cooperating system is so composed of a set of agents (e.g. some clients and a server) and a set of actions (e.g. the Send and Receive interface actions introduced above). We consider that the set of all possible sequences of actions models the behavior of the system and that an agent's initial knowledge about the system consists of all traces the agent initially considers possible. An agent may assume for example that a message that was received must have been sent before, and this is the case for any validation of a security property holding in a system. In our example, the SCP's DIPM level states that a Receive action from a client C using a specific channel ch is always preceded by the respective Send generation action triggered by the server S (line 8).

Domain Specific Pattern Model (DSPM).

The formal model corresponding to the DSPM introduced in Section 3.2.2, as the refinement of the DIPM using the SSL mechanism, contains the same set of agents, namely C and S. some of these DSPM artifacts using the Isabelle definitions. Its actions correspond to the external and technical DS interface function calls. They can be considered as a refinement of the actions of the DIPM formal model. The code defines also a specific DSPM server S suitable for the SSL protocol (line 11). The security property that is provided by this SSL pattern and that corresponds to the trust property assumed to hold for the DIPM model is that the server trusts into the precedence of its own MAC verification action by the MAC generation action of the client (line 12).

Pattern Validation

Now we present the verification of the secure communication pattern at both DIPM and DSPM levels.

Domain Independent Pattern Model (DIPM).

The DIPM formal model of Figure 2 defines the SCP's collaborative agents of the pattern refined at Figure 3 using the SSL mechanism. The former figure also introduces the Send and Receive actions corresponding to the external DI interface (lines 3 and 4). We further assume that each agent can only see its own actions. According to Section 3.2.1, the required authenticity property is expressed as: lemma authSendReceive : ′′ auth Send Receive server ′′ (P-DI)

In order to prove this constraint between Send and Receive messages, we use the result of [START_REF] Fuchs | A Formal Notion of Trust -Enabling Reasoning about Security Properties[END_REF] which states that the properties trust(P, precede(a, b)) and auth(b, c, P ) imply the property auth(a, c, P ). Setting b = c and instantiating a, b, P with the concrete Send and Receive actions and the server S of property P-DI, we conclude that P-DI holds if the following properties (assumptions) hold: -lemma trustSendReceive : ′′ trust server precedeSendReceive ′′ (A-DI) -lemma authReceiveReceive : ′′ auth Receive Receive server ′′ We may assume that the latter property holds because any action identified by the server is authentic. Hence, this concludes our proof with respect to the DIPM model the assumption (A-DI) must be assumed to hold.

We emulate these constraints in Isabelle by the theorem: theorem authIf T rustSendReceive : ′′ authIf T rust Send Receive server ′′ which terminates the P-DI proof of the DIPM model assuming the assumption A-DI. For simplification purpose, we consider that trust of the server into the precedence of a corresponding Receive action by a client Send action is given by the set membership relation of the same action to the set of actions of mapped agents. Recall that Figure 2 introduces the definitions which encodes the precedence, auth and trust properties between a Send action and a Receive action for the couple client and server (lines 8, 13, 14 and 15).

The fact that no more DIPM definition can be applied shows that we now have to consider the DSPM level, i.e. we have to find and validate the SSL implementation that provides an equivalent property. This will be discussed in the next paragraph.

Domain Specific Pattern Model (DSPM).

The security property that is provided by this SSL pattern and that corresponds to the trust property assumed to hold for the DIPM model is that the server trusts into the precedence of its own signature verification action by the signature generation action of the client: lemma trust : ′′ trust server precedeGenM acV erif yM ac ′′ (P-DS)

In order to prove P-DS, we isolate assumptions provided by the SSL protocol as a random number is only generated once, the server trusts into the confidentiality of its own private RSA key and into the confidentiality of the certificate authority's private key. These statements captures the semantics of an RSA encryption and allows to conclude that S trusts in the confidentiality of the shared secrets derived from the SSL handshake and yields that indeed property P-DS holds. For more details, the complete proof was introduced in [START_REF] Hamid | Enforcing S&D Pattern Design in RCES with Modeling and Formal Approaches[END_REF]. In our case, we introduce the genM ac and verif yM ac actions and their temporal dependency precedeGenM acV erif yM ac, as illustrated by Figure 3 (lines 3, 4 and 8). We also defined the trust predicate for the DSPM server (line 12). This predicate will be used by the refinement process from the DIPM model to the DSPM model (line 1 of Figure 4).

We synthesize the P-DS proof by introducing the genM ac and verif yM ac actions and their temporal dependency precedeGenM acV erif yM ac, as illustrated by Figure 3 (lines 3, 4 and 8). However we need what is trust for a DSPM server; this is defined by the code of line 12. This predicate will be used by the refinement process from the DIPM model to the DSPM model (see line 1 of Figure 4).

Correspondence between DIPM and DSPM

Note that a system specification does not require a particular level of abstraction. Different formal models of the same system are partially ordered with respect to different levels of abstraction. Formally, abstractions can be mapped to action sequences of a finer abstraction level to action sequences of a more abstract level while respecting concatenation of actions.

Correspondence between the DIPM and DSPM formal models is assumed when proving that the property introduced at the DIPM model is transferred to the DPSM model. More precisely, this means that the DIPM model is an abstraction of the DSPM model. In particular, we must show that using a specific mechanism for verifying the property together with function calls of the specific domain is a specific case of proving the upper-level property.

We so have to map actions of the DSPM model onto the actions of the DIPM model by an appropriate homomorphism h and then prove that this homomorphism preserves trust in precede. In practice, h is required to preserve each operation or a pseudooperation which summarizes the behavior of a set of operations. Figure 4 specifies h in Isabelle and the resulting trustW ithH theorem. Since we assume property A-DI to hold for the DIPM model, all server Receive actions are preceded by a client Send action in the server's abstract initial knowledge. On the other hand, the server's concrete initial knowledge reflects the MAC mechanism, i.e. reflects that a verif yM ac action is always preceded by the respective genM ac action. This is assumed by the buildP roperty definition of Figure 4 (line 2) introduced as assumption and by the precedeGenM acV erif yM ac definition of Figure 3 (line 8).

Note that we consider P-DS as the premise of an implication where DSP M.trust a1 (buildP roperty l) refers to trust for the DSPM model of Figure 3, while DIP M.trust a2 (applyH l) refers to trust for the DIPM counterpart of Figure 2. More generally, the DIPM and DSPM call or type prefixes of Figure 4 are related to each modeling. Thereby, setting up and proving the trustW ithH theorem (line 5) requires defining both a DIPM server and a DSPM server; these two servers have the same functionality in practice. Based on these assumptions, the homomorphism h preserves trust into precedence and property A-DI transferred to the DSPM model is identical to property P-DS.

Related Works

Design patterns are a solution model to generic design problems, applicable in specific contexts. Supporting research tackles the presented challenges includes domain patterns, pattern languages and recently formalisms and modeling languages to foster their application in practice. To give an idea of the improvement achievable by using specific languages for the specification of patterns, we look at pattern formalization and modeling problems targeting the integration of the pattern specification and validation steps into a broader MDE process.

Several tentatives exist in the literature to deal with patterns for specific concerns [START_REF] Di Giacomo | Using Security and Dependability Patterns for Reaction Processes[END_REF][START_REF] Yoshioka | A survey of security patterns[END_REF]. They allow to solve very general problems that appear frequently as sub-tasks in the design of systems with security and dependability requirements. These elementary tasks include secure communication, fault tolerance, etc. The pattern specification consists of a service-based architectural design and deployment restrictions in form of UML deployment diagrams for the different architectural services.

To give an overview of the improvement achievable by using specific languages, we look at the pattern specification and formalization problems. UMLAUT [START_REF] Guennec | Precise modeling of design patterns[END_REF] is an approach that aims to formally model design patterns by proposing extensions to the UML metamodel 1.3. They used OCL language to describe constraints (structural and behavioral) in the form of meta-collaboration diagrams. In the same way, RBML (Role-Based Metamodeling Language) [START_REF] Kim | A UML-Based Metamodeling Language to Specify Design Patterns[END_REF] is able to capture various design perspectives of patterns such as static structure, interactions, and state-based behavior.

While many patterns for specific concern have been designed, still few works propose general techniques for patterns. For the first kind of approaches [START_REF] Gamma | Design Patterns: Elements of Reusable Object-Oriented Software[END_REF], design patterns are usually represented by diagrams with notations such as UML objects, annotated with textual descriptions and examples of code. There are some well-proven approaches [START_REF] Douglass | Real-time UML: Developing Efficient Objects for Embedded Systems[END_REF] based on Gamma et al. However, this kind of technique does not allow to reach the high degree of pattern structure flexibility which is required to reach our target.

Formal specification has also been introduced in [START_REF] Mikkonen | Formalizing design patterns[END_REF] in order to give rigorous reasoning of behavioral features of a design pattern in terms of high-level abstractions of communication. In this paper, the author considers an object-oriented formalism for reactive system (DisCo) [START_REF] Jarvinen | DisCo specification language: marriage of actions and objects[END_REF] based on TLA (Temporal Logic of Actions) to express high-level abstractions of cooperation between objects involved in a design pattern. However, patterns are directly formalized at the pattern level including its classes, its relations and its actions, without defining a modeling language.

The work in [START_REF] Cheng | Using security patterns to model and analyze security[END_REF] introduces a new specification template inspired on secure system development needs. The template is augmented with UML notations for the solution and with formal artifacts for the requirement properties. Another approach [START_REF] Gasparis | LePUS3: An Object-Oriented Design Description Language[END_REF] provides a formal and visual language for specifying design patterns called LePUS. It defines a pattern in an accurate and complete form of formula in Z, with a graphical representation. The framework promoted by LePUS is interesting but the degree of expressiveness proposed to design a pattern is too restrictive.

UMLsec [START_REF] Jürjens | UMLsec: Extending UML for Secure Systems Development[END_REF] is an approach based on the integration of modeling security in UML and formal methods for object-oriented system development. UMLsec is defined in form of a UML profile and semantics to assist in the automated analysis of the UMLsec models with respect to security requirements. UMLsec and our approach are not in competition but they complement each other by providing different view points to the secure information system, mainly in applying security patterns for system security engineering.

Moreover, [START_REF] Hatebur | A security engineering process based on patterns[END_REF] used the concept of security problem frames as analysis patterns for security problems and associated solution approaches. The analysis activities using these patterns are described with a highlight of how the solution may be set, with a focus on the privacy requirement anonymity. For software architecture, [START_REF] Halkidis | A qualitative analysis of software security patterns[END_REF] presented an evaluation of security patterns in the context of secure software architectures. The evaluation is based on the existing methods for secure software development, such as guidelines as well as on threat categories.

To summarize, in software engineering, design patterns are considered effective tools for the reuse of specific knowledge. However, a gap between the development of systems using patterns and the pattern information still exists. This becomes even more visible when dealing with specific concerns namely security and dependability properties for several application sectors such as presented recently in [START_REF] Fernandez | Software Engineering for Secure Systems: Industrial and Research Perspectives[END_REF]. In an other point of view, we agree with the argumentations given in [START_REF] Zdun | Modeling Architectural Patterns Using Architectural Primitives[END_REF] to justify why the precise specification and formalization of a pattern by definition restricts its "degree of freedom for the design", and hence there is no success stories of works dealing with pattern formalization. This is not only related to security patterns. Note however, that this work does not address the validation activity which is an important issue in any design activity and more particularly in security engineering. We think that security is subject to rigorous and precise specification and the proposed literature (in our best knowledge) fails to meet these two objectives. To remedy these contradictory needs, we support the specifications of security patterns at two levels of abstractions, domain independent and domain specific, in both a semi-formal representation through metamodeling techniques and a rigorous formal representation through interactive theorem proving approach. This allows to support some variability of the pattern.

Conclusion and Future Work

A classical form of pattern is not sufficient to tame the complexity of safety critical systems -complexity occurs because of both the concerns and the domain management. To reach this objective and to foster reuse, we introduced the specification at domain independent and domain specific levels. The former exhibits an abstract solution without specific knowledge on how the solution is implemented with regard to the application domain. Following an MDE process, the domain independent model of patterns is then refined towards a domain specific level, taking into account domain artifacts, concrete elements such as mechanisms to use, devices that are available, etc. Consequently, a security pattern at domain specific level contains the respective information.

These two levels of abstractions are captured using new concepts related to the different kind of knowledge described by the pattern had; not with existing software constructs. In our work, we used the MDE philosophy. We do not use the software concepts (object or component constructs) recommended by Model-Driven Architecture (MDA), for example. However, the SEPM language is subject to target specific software modeling languages such as those recommended by MDA, using model transformation techniques. Regarding the well known MDA levels (PIM and PSM), there is an overlap between these levels and our two abstraction levels. For example, in the Intelligent Transport Systems (ITS) domain, the ISO/IEC 15118 highly recommends to use TLS for ensuring security properties. For that domain, we can find different platforms supporting such a DSPM pattern.

We also provide an accompanying formalization and validation framework to help precise specification of patterns based on the interactive Isabelle/HOL proof assistant. The resulting validation artifact's may mainly (1) complete the definitions, and (2) provide semantics for the interfaces and the properties in the context of S&D. Like this, validation artifacts may be added to the pattern for traceability concerns. In the same way, the domain refinement is applied during the formal validation process for the specification and validation of patterns.

Furthermore, we walk through a prototype of EMF tree-based editors supporting the approach. Currently the tool suite named Semcomdt2 is provided as Eclipse plugins. The approach presented here has been evaluated on two case studies from the TERESA project3 resulting in the development of a repository of S&D patterns with more than 30 S&D patterns.

The next step of this work consists in defining a correct-by-construction patternbased security engineering process. It aims to provide the correct-by-construction integration of a design pattern into an application while offering a certain degree of liberty to the designer using it. In order to be able to validate the integration, we must have a formal specification of the pattern, i.e., its properties, constraints and related validation artifacts, as input to the pattern-based development process. Another objective for the near future is to provide automated tool support for pattern-based development, preferably based on a widely known and accepted model-based approach in industry such as UML [START_REF] Omg | OMG Unified Modeling Language (OMG UML), Superstructure[END_REF]. For that, we plan to investigate the possibility to transform these design artifacts into UML [START_REF] Omg | OMG Unified Modeling Language (OMG UML), Superstructure[END_REF] and their corresponding validation artifacts into OCL [19].

A. Isabelle/HOL Formalization and Validation of the Secure Communication Pattern

The complete formalisation and verification of the secure communication pattern, using Isabelle/HoL, are available online via http://www.semcomdt.org/semco/ resources/SCP_Isabelle.zip. d e f i n i t i o n t r u s t K e y : : " a g e n t ==> p r o p e r t y K e y ==> b o o l " where " t r u s t K e y a p == p IN ( p r o p e r t i e s K e y a ) " d e f i n i t i o n t r u s t I n C o n f i d e n t i a l i t y : : " a g e n t ==> b o o l " where " t r u s t I n C o n f i d e n t i a l i t y a == ( t r u s t R a n d o m a n o t Pre c e d e G e n R an dG en Ra nd ) AND ( t r u s t K e y a c o n f P r i v K e y S ) AND ( t r u s t K e y a confPrivKeyCA ) " d e f i n i t i o n t r u s t I n S i g n a t u r e : : " a g e n t ==> b o o l " where " t r u s t I n S i g n a t u r e a == ( t r u s t M a c a ( p r e c e d e genMac v e r i f y M a c ) ) " d e f i n i t i o n t r u s t S C P : : " a g e n t ==> b o o l " where " t r u s t S C P a == t r u s t I n C o n f i d e n t i a l i t y a -> t r u s t I n S i g n a t u r e a "

A.1. DIPM Validation

Fig. 1 .

 1 Fig. 1. The SEPM metamodel -Overview

  C) denoting the communication channel of client and server, and m a message.

  send(C, S, mac C (m), m): The client C sends m and the corresponding MAC (Message Authentication Code) to the server S. -recv(S, C, mac C (m), m): The server receives m and corresponding MAC.

  i o n C S ch m" 4 : d e f i n i t i o n R e c e i v e : : " a c t i o n " where " R e c e i v e == c r e a t e A c t i o n S C ch m" 5 : r e c o r d p r o p e r t y = a c t i o n 1 : : " a c t i o n " a c t i o n 2 : : " a c t i o n " 6 : d e f i n i t i o n c r e a t e P r o p e r t y : : " a c t i o n ==> a c t i o n ==> p r o p e r t y " where " c r e a t e P r o p e r t y a1 a2 == a c t i o n 1 =a1 , a c t i o n 2 = a2 " 7 : d e f i n i t i o n p r e c e d e : : " a c t i o n ==> a c t i o n ==> p r o p e r t y " where " p r e c e d e a1 a2 == c r e a t e P r o p e r t y a1 a2 " 8 : d e f i n i t i o n p r e c e d e S e n d R e c e i v e : : " p r o p e r t y " where " p r e c e d e S e n d R e c e i v e == p r e c e d e Send R e c e i v e " 9 : r e c o r d a g e n t = name : : " a g e n t T y p e "

Fig. 3 .

 3 Fig. 3. The DSPM formalization of the Secure Communication Pattern

1 :Fig. 4 .

 14 Fig. 4. Proving trust in precede for the Secure Communication Pattern

  t h e o r y DIPM i m p o r t s Main b e g i n ( * S e c u r e C o mmu n i c a t i o n DIPM P a t t e r n d e f i n i t i o n s * ) . . . d e f i n i t i o n a u t h I f T r u s t : : " a c t i o n ==> a c t i o n ==> a g e n t ==> b o o l " where " a u t h I f T r u s t a1 a2 a == t r u s t a ( p r e c e d e a1 a2 ) -> a u t h a1 a2 a " ( * S e c u r e C o mmu n i c a t i o n DIPM P a t t e r n v a l i d a t i o n * ) t h e o r e m a u t h I f T r u s t S e n d R e c e i v e : " a u t h I f T r u s t Send R e c e i v e s e r v e r " a p p l y ( simp o n l y : a u t h I f T r u s t _ d e f ) a p p l y ( simp o n l y : t r u s t _ d e f ) a p p l y ( simp o n l y : s e r v e r _ d e f ) a p p l y ( simp o n l y : c r e a t e P r o p e r t y _ d e f c r e a t e A g e n t _ d e f ) a p p l y ( simp o n l y : S e n d _ d e f R e c e i v e _ d e f ) a p p l y ( simp o n l y : c r e a t e A c t i o n _ d e f ) a p p l y ( simp o n l y : a u t h _ d e f ) a p p l y ( simp ) done end A.2. DSPM Formalization and Validation t h e o r y DSPM i m p o r t s Main b e g i n ( * S e c u r e C o mmu n i c a t i o n DSPM P a t t e r n d e f i n i t i o n s * ) . . . d e f i n i t i o n t r u s t R a n d o m : : " a g e n t ==> p ro p e rt y R a n d o m ==> b o o l " where " t r u s t R a n d o m a p == p IN ( p r o p e r t i e s R a n d o m a ) "

  ( * S e c u r e C o mmu n i c a t i o n DSPM P a t t e r n v a l i d a t i o n * ) t h e o r e m p r o o f T r u s t S C P : " t r u s t S C P s e r v e r " a p p l y ( simp o n l y : t r u s t S C P _ d e f ) a p p l y ( simp o n l y : t r u s t I n C o n f i d e n t i a l i t y _ d e f t r u s t I n S i g n a t u r e _ d e f ) a p p l y( simp o n l y : n o t Pre c e d e G e n R a n d G e n R a n d _ d e f c o n f P r i v K e y S _ d e f c o n fPri v K e y C A _ d e f ) a p p l y ( simp o n l y : genMac_def v e r i f y M a c _ d e f ) a p p l y ( simp o n l y : n o t P r e c e d e _ d e f p r e c e d e _ d e f c o n f _ d e f ) a p p l y ( simp o n l y : c r e a t e P r o p e r t y M a c _ d e f c r e a t e A c t i o n M a c _ d e f ) a p p l y ( simp o n l y : c r e a t e P r o p e r t y R a n d o m _ d e f c r e a t e A c t i o n R a n d o m _ d e f ) a p p l y ( simp o n l y : c r e a t e P r o p e r t y K e y _ d e f c r e a t e A c t i o n K e y _ d e f ) a p p l y ( simp o n l y : t r u s t M a c _ d e f t r u s t R a n d o m _ d e f t r u s t K e y _ d e f ) a p p l y ( simp o n l y : g e n R a n d _ d e f p r i v K e y 1 _ d e f p r i v K e y 2 _ d e f ) a p p l y ( simp o n l y : s e r v e r _ d e f ) a p p l y ( simp o n l y : c r e a t e A c t i o n M a c _ d e f c r e a t e A c t i o n R a n d o m _ d e f c r e a t e A c t i o n K e y _ d e f c r e a t e A g e n t _ d e f ) a p p l y ( simp ) a p p l y ( simp o n l y : n o t Pre c e d e G e n R a n d G e n R a n d _ d e f c o n f P r i v K e y S _ d e f c o n fPri v K e y C A _ d e f ) a p p l y ( simp o n l y : p re c e d e G e n M a c V e ri fy M a c _ d e f ) a p p l y ( simp o n l y : p r e c e d e _ d e f n o t P r e c e d e _ d e f c o n f _ d e f ) a p p l y ( simp o n l y : c r e a t e P r o p e r t y M a c _ d e f c r e a t e P r o p e r t y R a n d o m _ d e f c r e a t e P r o p e r t y K e y _ d e f ) a p p l y ( simp o n l y : genMac_def v e r i f y M a c _ d e f p r i v K e y S _ d e f p ri v K e y C A _ d e f g e n R a n d _ d e f ) a p p l y ( simp o n l y : c r e a t e A c t i o n M a c _ d e f c r e a t e A c t i o n R a n d o m _ d e f c r e a t e A c t i o n K e y _ d e f ) a p p l y ( simp ) done end A.3. Correspondence between DIPM and DSPM Formalization and Validation t h e o r y DIPMtoDSPM i m p o r t s DIPM DSPM b e g i n ( * From DIPSM P a t t e r n t o DSPM P a t t e r n d e f i n i t i o n s * ) . . . d e f i n i t i o n buildAndApplyH : : "DSPM . a g e n t ==> DIPM . a g e n t ==> (DSPM . a c t i o n * DIPM . a c t i o n ) l i s t ==> b o o l " where " buildAndApply H a1 a2 l == DSPM . t r u s t a1 ( b u i l d P r o p e r t y l ) -> DIPM . t r u s t a2 ( applyH l ) " ( * From DIPSM P a t t e r n t o DSPM P a t t e r n v a l i d a t i o n * ) t h e o r e m t r u s t W i t h H : " buildAndApply H DSPM . s e r v e r DIPM . s e r v e r h " a p p l y ( simp o n l y : b u i l d A n d A p p l y H _ d e f ) a p p l y ( simp o n l y : DIPM . t r u s t _ d e f DSPM . t r u s t _ d e f ) a p p l y ( simp o n l y : b u i l d P r o p e r t y _ d e f ) a p p l y ( simp o n l y : a p p l y H _ d e f ) a p p l y ( simp ) a p p l y ( simp o n l y : h _ d e f ) a p p l y ( simp o n l y : S e n d _ d e f R e c e i v e _ d e f ) a p p l y ( simp o n l y : DIPM . c r e a t e A c t i o n _ d e f ) a p p l y ( simp o n l y : genMac_def v e r i f y M a c _ d e f ) a p p l y ( simp o n l y : DSPM . c r e a t e A c t i o n _ d e f ) a p p l y ( simp o n l y : DIPM . s e r v e r _ d e f DSPM . s e r v e r _ d e f ) a p p l y ( simp ) a p p l y ( simp o n l y : DIPM . c r e a t e A g e n t _ d e f DSPM . c r e a t e A g e n t _ d e f ) a p p l y ( simp o n l y : S e n d _ d e f R e c e i v e _ d e f genMac_def v e r i f y M a c _ d e f ) a p p l y ( simp ) a p p l y ( simp o n l y : p r e c e d e S e n d R e c e i v e _ d e f p re c e d e G e n M a c V e ri fy M a c _ d e f ) a p p l y ( simp o n l y : DIPM . p r e c e d e _ d e f DIPM . c r e a t e P r o p e r t y _ d e f DSPM . p r e c e d e _ d e f DSPM . c r e a t e P r o p e r t y _ d e f ) a p p l y ( simp ) a p p l y ( simp o n l y : S e n d _ d e f R e c e i v e _ d e f genMac_def v e r i f y M a c _ d e f ) a p p l y ( simp o n l y : DIPM . c r e a t e A c t i o n _ d e f DSPM . c r e a t e A c t i o n _ d e f ) a p p l y ( simp ) done end

http://www.semcomdt.org

http://www.teresa-project.org/