Elia Kouzari
email: ekouzari@csd.auth.gr

Lazaros Sotiriadis

Ioannis Stamelos

Process mining for process conformance checking in an OSS project: An empirical research

Keywords: open source software, process mining, open source communities, software event logs, process conformance

With almost 20 years of research, Process Mining can now be considered to be in a mature phase allowing its application to a variety of sectors. In this article, the bug closure process that is followed by a community of an open source software project is investigated in order to perform process conformance checking. Actual data that reveal the process steps have been extracted from the project's Bugzilla database and have been used as input in Disco process mining tool. The data includes extracted information for more than 19,000 bugs for the past 15 years in a csv form, formatted appropriately to construct an event log suitable for process mining. The extracted models have been compared to the process described in the project's blogs and wikis by the community. The same models are also compared to the bug closure process that Bugzilla suggests to be used by the projects using this software for bug tracking purposes. The findings reveal that indeed the process followed in the OSS project is very similar to the declared one but variations do occur under specific circumstances. However, the process is not identical to the one proposed by Bugzilla suggesting that each OSS project can customize its processes in order to better address the needs of the project and the community. This empirical research highlights the importance of process mining in OSS projects in order to investigate the processes followed and identify outliers helping to standardize and improve the processes and enhance the collaboration among the members of the communities.

Introduction

Scientific research has been focusing in the field of Process Mining, developing platforms, tools and algorithms for almost 20 years now. Process Mining is extensively applied in a variety of fields and sectors like healthcare, insurances, software etc. [START_REF] Rojas | Process mining in healthcare: a literature review[END_REF] [2][3][4] [START_REF] Rubin | Process mining can be applied to software too![END_REF]. Dozens of algorithms can be applied in the context of process mining either on a standalone basis or through the platforms that have been designed to facilitate this.

The majority of applied research in this field focuses on process discovery since this minimizes the cost of understanding the current 'As-is' process [START_REF] Rozinat | The added value of process mining[END_REF]. However, a lot of interest arises in the aspect of process conformance as well. According to van der Aalst [START_REF] Van Der | Process Mining[END_REF] process discovery is the technique that takes an event log and produces a process map explaining the behavior recorded in the log. On the other hand, process conformance is the procedure where an existing process model is compared with an event log of the same process to indicate whether the reality, as recorded in the log, meets the proposed model and vice versa.

Kouzari and Stamelos [START_REF] Kouzari | Process Mining in software events of Open Source Software projects[END_REF] suggested that the application of process mining in open source software could reveal not only the variety of processes followed by open source communities but it could also help standardize or improve core activities like the way tasks are shared and bugs are closed. Given the fact that in Open Source Software there is a huge amount of process-relevant data publicly available online, OSS communities are a great opportunity to discover and analyze software processes. These data can be usually extracted from mailing lists, discussion forums, source repositories and binary release sections [START_REF] Jensen | Data mining for software process discovery in open source software development communities[END_REF].

In this article, the authors proceed to process conformance checking of the bug reporting and closing process of a large Open Source Software project by examining the documentation of the project and extracting the process model that is believed to be followed against the 'As-is' process that is extracted from the event log. In addition, this process is also compared with the general Bugzilla guidelines for bug reporting and resolution.

The rest of the article is structured as follows: Section 2 describes the background of this work and poses the research question. Section 3 explains the methodology followed and Section 4 presents the findings of the research. Finally, Section 5 contains the discussion, conclusions and future work.

2

Background Work

Bugzilla

Bugzilla is an open source software system for bug tracking. It is currently the most widely used bug tracking system [START_REF] Barnson | The Bugzilla Guide-2.17. 5 Development Release[END_REF]. This bug tracker allows open source communities to handle the discovered bugs by facilitating the communication of problems effectively throughout the data management chain. This ensures that each reported bug is stored in the project's Bugzilla database along with each detail regarding its state and the steps taken or not towards its resolution. The lifecycle of a bug in Bugzilla is illustrated in Figure 1. This workflow can be customized to meet the needs of every community and every project using it as a back-tracking system. In Figure 1 only the default bug statuses are shown. The main process followed in Figure 1 is as follows: When a bug is first reported in the system, its status changes to "UNCONFIRMED". The bug remains in this state until it receives a specific number of votes by community members that is indeed reproduced. By the time the votes are sufficient, the bug status changes to "NEW". A bug can automatically at first be set to "NEW" when the user/developer reporting it has the right to change its status. Following, the bug can be assigned to a specific developer or can be left open for anyone to resolve it. At this moment, the status of the bug is set to "ASSIGNED". The developers resolve the bug, and a patch is sent for Quality Assurance (QA). When the QA tests are successful, the bug becomes "RESOLVED" and "VERIFIED". In case QA tests fail, the bug can be set to "REOPEN" and short after this to "ASSIGNED" or "RESOLVED" once again. A bug must be "CLOSED" by the person who first reported it. It is obvious that a lot of variations are also possible depending on the nature of the bug and the authority of the person who first reports it [START_REF] Akbarinasaji | Predicting bug-fixing time: A replication study using an open source software project[END_REF].

Koha Open Source Integrated Library System

Koha is a web-based open source ILS written in Perl and distributed under GNU General Public License1 . With a very active community of developers around the world, Koha was first released in 2000 and since then it has gained wide acceptance, as it is utilized in hundreds of organizations (both in the governmental and private sector) around the world [START_REF] Kouzari | Process Mining applied on library information system usage-A case study[END_REF]. Koha interacts with a MySQL database and supports a variety of library activities with the most widely used being cataloguing, acquisition, circulation and administration [START_REF] Macan | Open Source Solutions for Libraries: ABCD vs Koha[END_REF]. Being able to be installed and function in all Operating Systems (Linux, Unix, Windows, MacOS), Koha offers a very configurable and adaptable user interface, allowing each organization to set it up accordingly to the procedures and policies followed in each case.

For bug tracking purposes, Koha maintains its own Bugzilla database. Since the project has an active community, there are wikis2 , IRC3 (chats) and blogs4 that describe the procedures followed in the project and facilitate the communication and coordination of the community.

The Koha blog describes the bugs workflow process as follows: A user or a developer can report a bug through Bugzilla. Everyone should file a bug report, even developers who intend to immediately fix one. The Koha project does not actively use the Priority field in Bugzilla. However, severity field is indicated to be important. For this reason, along with the bug report the user has to also assign the severity of a bug. For unclear situations "normal" severity is suggested. Once a bug is reported it is assigned to a developer. At this stage, a bug can be left idle, if no one takes action on it, and it can also be reassigned. Once a person decides to work on a bug, he has to first accept it and update its status from New to Assigned. When a solution to a bug is available, a patch is submitted turning the status of a bug to "Patch-Sent". The Koha Release Manager evaluates the submitted patch and if the patch works it is marked as "pushed". A resolved bug is altered from "Assigned" to "Resolved -Fixed". Koha Wiki clearly suggests that the user should review the Bugzilla Bug Writing Guidelines prior to submitting a bug to Koha.

Based on all these characteristics and its large and active community of developers and users, Koha is considered at the time as an ideal candidate in the context of this research

Research Question

In section 2.2 the Koha bugs workflow is presented as declared in the official pages of Koha project. In terms of process mining, the abovementioned process is considered the "As-Is" process followed. Since Koha is an open source project its data and code are available through the tools used by the community. It would be of great interest to mine the actual process followed to resolve the bugs using data from the project's Bugzilla database and perform process conformance checking. As a result, the research question investigated in this paper is the following:

RQ: Does the community of Koha Open Source ILS conforms to the bug resolution process described in the project's pages or not? If not, what is the actual process followed?

Methodology

Anyone can register in the Bugzilla page for Koha project in order to view all the bugs listed along with the history of each bug. The main Bugzilla page illustrates all current bugs with their current state. In order to get all the actions performed for the resolution of a bug, one must locate a bug and then using the bug id provided he may visit the specific page that illustrates in tabular format the actions taken so far for it. The methodology shown in Figure 2 was used to gather all information for all bugs listed in Koha project so far for cleaning/transformation of data for process mining.

Locate Relevant Data

First, the relevant data was located in the Bugzilla database. Using Bash scripting and Wget tool, the data was extracted in html form and appended in a single html file. This procedure gathered historical data for 19,311 bugs between 15/06/2002 and 14/12/2017.

Data Preparation

Html2text was used to remove any text formatted from the gathered data. In addition, to be able to further format the data in a csv form and to create a tabular representation suitable of an event log for process mining, further scripting was required (grep, icony, recode, sed, tr, cat, uniq, sort, echo). As a result, a csv file with 359,395 records was created containing information for 19,311 bugs.

Clean Data

For each record, the following columns were present: Event_Id, Bug_Id, Bug_Description, User_Email, Action_datetime, Action_Type and Action_Data.

Although this file contained all the required columns to be used as an event log [START_REF] Van Der Aalst | Process mining put into context[END_REF], further cleaning of the file had to be performed in order to keep those data that would reveal the process followed for bug resolution. While the first 5 columns reveal their role, columns Action_Type and Action_Data were used to keep the most important information. For every variable mentioned in column Action_Type, a different set of values was used in column Action_Data. After analysis of each variable in the Ac-tion_Type column and taking in mind the described process followed for bug resolution in Koha Blogs and Wikis, the csv file was filtered to keep the records for the following variables of Action_Type column: Status, Priority, Severity, Resolution. Table 1 below presents the Action_Data values per Action_Type selected for filtering. Finally, a csv file with 97,372 records for 19,311 bugs was extracted that was used as an event log for Process Mining. The rest of the steps that concern the process mining and the process conformance check are presented in section 4.

Findings

Process Mining

For Process Mining, Disco5 process mining tool was used. Initially the event log was used as input to Disco. Prior to the process mining, the columns of the event log had to be assigned as Case_ID (Bug_Id), Resource (User_Email), Timestamp (Ac-tion_Datetime), and Activity (Action_Type and Action_Data). Event_ID and Bug_Description were ignored as they had no role in affecting the bug resolution process.

The event log was then used for process mining revealing a "spaghetti model" that it was impossible to highlight useful information regarding the process mined. The extracted model highlighted the most used statuses but it was hard to analyze and compare to the suggested process. To extract safest conclusions, 47,9% of the most common activities of the diagram were filtered creating a new, clearer process model.

Despite the second process model was significantly more clear than the first one, it was clearly affected by the status of the first 283 bugs in the event log. This was proved by Status/Closed that was shown to be the first step of the process (and the last) for the majority of the cases. With further analysis of the event log, the authors noticed that for the first 283 bugs only a record indicating that a bug's status was set to "CLOSED" existed. This could affect the actual process followed since no history for the resolution process of these bugs was available. In the next session, this is further explained. 6A new event log, ignoring the first 283 bugs was used as a new input with the same parameters in Disco. The process map created for the new event log is shown in Figure 3. In this model, the process is almost identical to Figure 3 with an exception towards the end of the process. However, the bug resolution process remains unaltered even though a significant number of cases are not included indicating that the community is consistent to the steps taken to resolve a bug.

Process Conformance Check

By observing Figures 3 and4 one can conclude that the discovered process is very similar to the one described in the community's blogs and wikis. By these means we can clearly say that the Koha community does conform to the process suggested for bug resolution. Focusing on Figure 3, where the model contains more cases since it includes all the bugs and not just those that have been fixed, it is obvious that there is a main process, identical to the one proposed by the community but this is not exclusive. There are some exceptions, some process variations that are obvious. Disco has the ability to reveal these paths along with their frequency. As a result, Table 2 presents the 5 most frequent process variances that do not follow the proposed guidelines for bug resolution.

RESOLVED -> FIXED -> CLOSED 4,14% PATCH-Sent -> RESOLVED -> FIXED -> CLOSED 1,64% ASSIGNED -> PATCH-Sent -> RESOLVED -> FIXED -> CLOSED 1,42%
Needs SignOff -> Failed QA 0,37% ASSIGNED -> RESOLVED -> FIXED -> CLOSED 0,32% 4,14% of the time, a bug is automatically Resolved and Closed. This happens either because it is an old bug and no other relevant historical data is available, either because the person who identifies a bug automatically fixes it. However, it is recommended by the community to report each and every bug even if that means the bug is instantly resolved. For this reason, the abovementioned path does not conform to the bug resolution process.

The same seems to happen with the rest of the process variances. In all of the variances, either the bug is not set to Needs SignOff from the beginning of the bug resolution process or several process steps are omitted until the bug is set to Closed.

In the Discussion session below this is further discussed and compared to the Bugzilla suggested process for bug resolution.

Discussion and Future Work

The event log created by the Bugzilla database of Koha OSS ILS revealed that the community does follow in practice the bug resolution process described in the official documentation of the project. However, there are some cases where this is not true. It was mentioned earlier that the first 283 bugs did not include any other information rather than a record indicating they were closed. This indicates that 15 years back, when the project was not in a mature phase the community was using another bug resolution process. This might have happened due to a limited number of bugs or due to the lack of mature bug tracking tools. Starting from bug with bugID=284 there is precise information about the bug and all of its states throughout the resolution process. At the same time, one can observe that although the community follows a specific process for bug resolution, there are some process variances that do not conform to the proposed guidelines. This illustrates that in an open source software community there is freedom to act and modify procedures that are not as strict as in proprietary software. A developer might decide to act based on his knowledge and experience in a specific situation.

Comparing the bug resolution process of Koha with the proposed guidelines for bug resolution by Bugzilla it is obvious that there are a lot of differences. With a closer look a correlation is identified in some of the states. The RESOLVED status of Bugzilla corresponds to Needs SignOff of Koha and VERIFIED status of Bugzilla corresponds to Signed Off of Koha. This reveals that open source software tools can be freely customized to address the needs of each community of users and developers. At the same time, each OSS community is free to investigate how OSS tools can be modified to be used in favor of their own processes.

As stated earlier, Koha is a very active and serious community that is well organized. In addition, the project contains excellent documentation that the users can address in order to find answers to their questions. For even better communications there are IRC chat rooms where users and developers can further discuss any related issues. The documentation of the project and the good communication between the members of Koha community is illustrated in the process conformance check performed in this article.

However, other communities, less structured and active might face a variety of problems in the management of their processes. Process mining not only can highlight problems in the existing processes followed by OSS communities but it can also use projects like Koha as a benchmark to reveal aspects of processes that can be further improved in other projects. Nonetheless, the extracted process models can be used for predictions regarding the future of a given project in terms of survival, software quality and maturity.

Recently, Bugzilla released newer documentation containing a newer version of the lifecycle of a Bugzilla bug. It would be of great interest to investigate projects following the new guidelines for bug resolution and also see which of the projects currently following the former guidelines will decide to modify their processes and the effect this will bring to process efficiency. Future work includes further empirical research on process conformance for OSS projects. Especially for bug management, the newly released Bugzilla process needs to be taken into account.

Fig. 1 .

 1 Fig. 1. The lifecycle of a bug in Bugzilla (source: https://wiki.documentfoundation.org/QA/Bugzilla/Fields/Status)

Fig. 2 .

 2 Fig. 2. The methodology followed in this article for process conformance check

Fig. 3 .

 3 Fig. 3. The process model extracted when the first 283 bugs are removed from the event logIn the diagram of Figure3a clearer process is extracted. The dark process steps indicate the most common statuses and the darker arrows indicate the most frequent transitions from these process steps. One can identify from this diagram that the most common process path followed is the following:

Fig. 4 .

 4 Fig. 4. A process model extracted for all bugs that are FIXED

Table 1 .

 1 Action_Data values per Action_Type variable

	Action_Type variable	Corresponding Action_Data values
		P1, P1-high, P2, P3, P4, P5, P5-low, PATCH-
	Priority	Sent, PATCH-Sent-P5
		--, DUPLICATE, FIXED, INVALID, LATER,
	Resolution	MOVED, REMIND, WISHLIST, WONTFIX, WORKSFORME
		blocker, critical, enhancement, major, minor, new-
	Severity	feature, normal, trivial
		ASSIGNED, BLOCKED, CLOSED,
		REOPENED, RESOLVED, UNCONFIRMED,
	Status	VERIFIED Failed QA, InDiscussion, Needs Si-gnoff, NEW, Passed QA, Patch doesn't Apply,
		Pushed by Module Maintainer, Pushed for QA,
		Pushed to Master, Pushed to Stable, Signed Off

Table 2 .

 2 The 5 most frequent process variances that do not conform to the process guidelines

	Process Variance

https://koha-community.org

https://wiki.koha-community.org

https://koha-community.org/get-involved/irc/

https://www.myacpl.org/koha/

https://fluxicon.com/disco/

Additional information on the first process models extracted by the event log and discussed in this section are available online at http://switch.csd.auth.gr/

All of the process steps mentioned are associated with the value "Status" of the Ac-tion_Type field, except from Fixed that is associated with the value "Resolution" of the Action_Type field. The same event log was inserted into Disco, keeping only dimensions "Status" and "Resolution" of the column "Action_Type". To extract a more precise model, focused on the resolved bugs, an endpoint filter was applied to the event log. The end event value was set to "FIXED" keeping 10% of the cases and 17% of events. As a result, the process model of Figure4was produced.


Madeline Cheah
email: cheahh2@coventry.ac.uk

Nga Hoang
email: hoang.nguyen@coventry.ac.uk

Jeremy Nguyen

Siraj A Bryans

Shaikh

Formalising Systematic Security Evaluations using Attack Trees for Automotive Applications

Keywords: automotive security, attack trees, secure design, security testing, Bluetooth

Vehicles are insecure. To protect such systems, we must begin by identifying any weaknesses. One approach is to apply a systematic security evaluation to the system under test. In this paper we present a method for systematically generating tests based on attack trees. We formalise the attack trees as provably-equivalent process-algebraic processes, then automatically generate tests from the process-algebraic representation. Attack trees may include manual input, (and thus so will some test cases) but scriptable test cases are automatically executed. Our approach is inspired by model based testing, but allows for the fact that we do not have a specification of the system under test. We demonstrate this methodology on a case study and find that this is a viable method for automation of systematic security evaluations.

Introduction

Vehicles are extremely reliant on software and connectivity to enable the functionality desired by customers. The explosion of diverse technologies in cars has meant that cybersecurity of vehicles has become a mainstream concern for manufacturers; such concerns arise out of a number of attacks on components [START_REF] Checkoway | Comprehensive Experimental Analyses of Automotive Attack Surfaces[END_REF][START_REF] Koscher | Experimental Security Analysis of A Modern Automobile[END_REF], internal vehicular network [START_REF] Cho | Error Handling of In-vehicle Networks Makes Them Vulnerable[END_REF][START_REF] Hoppe | Security threats to automotive CAN networks -Practical examples and selected short-term countermeasures[END_REF] and through external interfaces [START_REF] Checkoway | Comprehensive Experimental Analyses of Automotive Attack Surfaces[END_REF][START_REF] Greenberg | Hackers Remotely Kill a Jeep on the HighwayWith Me in It[END_REF]. Systematic and automated testing to assure against many such attacks is a challenge, and an ad-hoc approach (i.e. a subjective prioritisation of when and where to test) usually means there is less than optimal coverage of vulnerabilities.

The contribution of this paper is a well-founded methodology to systematically evaluate the cybersecurity of a vehicle, using a model checker and a translation of attack trees into a process algebra. The methodology is inspired by model-based security testing.

The rest of the paper is organised as follows. In Section 2, we discuss related work. Section 3 contains the semantics of attack trees as source-sink graphs and the traces model of CSP [START_REF] Roscoe | Understanding Concurrent Systems[END_REF]. This is followed by an overview of our methodology in Section 4, including a translation function for attack trees into the traces model of CSP, and a demonstration of the equivalence of the two models. We then discuss the implementation of this methodology (Section 5) and apply it to a case study involving diagnostic devices that attach to the vehicular on-board diagnostics port (Section 6). Section 7 concludes the paper.

Related Work

We discuss the attack tree formalism in an automotive context in Section 2.1 and model based security testing in Section 2.2.

Attack Trees

The foundations of formal descriptions of attacks were laid by [START_REF] Mauw | Foundations of Attack Trees[END_REF] and in particular their process algebraic nature was recognised in [START_REF] Vigo | Automated generation of attack trees[END_REF]. Automotive specific attack trees have also been discussed in literature where [START_REF] Salfer | Efficient Attack Forest Construction for Automotive On-board Networks[END_REF] looked at attack tree generation and gave formal descriptions of the trees. This is orthogonal to our research (in translating low level attack trees) as in our case the trees have already been pre-built based on reconnaissance of a black box system, rather than the automatic generation of an attack tree from a fully specified systemunder-test (SUT).

Attack tree generation is still challenging as the SUT has unknown specifications (black box). Other examples of attack trees in the automotive context are those as described in the 'E-safety vehicle intrusion protected applications' (EVITA) project [START_REF] Ruddle | EVITA Project: Deliverable D2.3 -Security requirements for automotive on-board networks based on dark-side scenarios[END_REF] and the SAE J3061 Cybersecurity Guidebook for Cyber-Physical Vehicle Systems [START_REF]Cybersecurity Guidebook for Cyber-Physical Vehicle Systems[END_REF], although these are informal. Application of executable attack trees has been demonstrated [START_REF] Cheah | Towards a systematic security evaluation of the automotive Bluetooth interface[END_REF], however, automation was limited to test case execution. The attack trees were informally described and manually created.

Model-based Security Testing

Model-based security testing (MBST) is a special case of model-based testing (MBT) with a focus on security requirements. One can find a succinct classification of different approaches with respect to MBT and MBST in [START_REF] Felderer | Model-based security testing: a taxonomy and systematic classification[END_REF][START_REF] Utting | A taxonomy of model-based testing approaches[END_REF], where MBT is comprised of the following: (1) A formal model of the SUT is collected usually from specification documents as the result of the design phase of the SUT, or constructed from system requirements. This model can be at different abstraction levels where the most abstract one contains all possible behaviours;

(2) Test case filter criteria are then determined. They are usual informal descriptions capturing a subset of behaviours of the formal model which can be drawn from the requirements or the structure of the formal model (e.g., state coverage, transition coverage). In terms of MBST, these criteria concentrate on system security such as security properties (e.g.,confidentiality, integrity and availability), security mechanisms, and the environment (e.g., attack strategies). (3) These criteria are then formalised into test case specifications, usually compatible with the formal model. ( 4) Given the formal model of the SUT and the test case specifications, test cases are automatically generated by different technologies such as model checking, theorem proving, or graph search algorithms. Finally, (5) these test cases are executed on the SUT to provide verdicts. This involves translation of test cases from the abstract level of the formal model into concrete test scripts that are executable on SUT. Then, the execution result is translated back to the abstract level for comparison with the expected output of the generated test cases.

Semantic models

In this section we give the formal notation and source-sink semantics of attack trees (Section 3.1) and the notation and finite trace semantics of the formal language Communicating Sequential Process (CSP) (Section 3.2).

Attack Trees

Attack trees were first created to describe the actions of an attacker in an methodical manner [START_REF] Schneier | Attack Trees: Modeling Security Threats[END_REF].

Attack trees contain a set of leaf nodes, structured using the operators conjunction (AND) and disjunction (OR). The leaf nodes represent atomic attacker actions, the AND nodes are complete when all child nodes are carried out, and OR nodes are complete when at least one child node is complete.

Extensions have been proposed using Sequential AND (or SAND) [START_REF] Jhawar | Attack Trees with Sequential Conjunction[END_REF]. There are two types of ordering: time dependent or condition dependent. In this paper we adopt the condition dependent paradigm.

We follow the formalisation of attack trees given in [START_REF] Jhawar | Attack Trees with Sequential Conjunction[END_REF][START_REF] Mauw | Foundations of Attack Trees[END_REF]. If A is the set of possible atomic attacker actions, the elements of the attack tree T are A ∪ {OR, AND, SAND}, and an attack tree is generated by the following grammar, where a ∈ A:

t ::= a | OR(t, . . . , t) | AND(t, . . . , t) | SAND(t, . . . , t) Attack tree semantics have been defined by interpreting the attack tree as a set of series-parallel (SP) graphs [START_REF] Jhawar | Attack Trees with Sequential Conjunction[END_REF]. Definition of SP graphs requires first the definition of source-sink graphs and here we use the definitions from [START_REF] Jhawar | Attack Trees with Sequential Conjunction[END_REF].

Definition 1: A source-sink graph over A is a tuple G = (V , E , s, z ) where V is a set of vertices, E is a multiset of edges with support E * ⊆ V × A × V , s ∈ V
is a unique source and z ∈ V is a unique sink, and s = z .

The sequential composition of G and another graph G , denoted by G • G results from the disjoint union of G and G and linking the sink of G with the source of G . Thus, if ∪ denotes the disjoint union and E [s/z ] denotes the multiset of E where vertices z are replaced by s, then G.G can be defined as:

G • G = (V \ {z } ∪V , E [s /z ] ∪E , s, z )
Parallel composition, denoted by G G is similar (differing only in that two sources and two sinks are identified) and can be defined as:

G G = (V \ {s, z } ∪V , E [s /s,z /z ] ∪E , s , z ) Definition 2:
The set G SP over A is defined inductively by: For a ∈ A, a -→ is an SP graph, If G and G are SP graphs, then so are G • G and G G .

Hence, the full SP graph semantics for attack tree T can be given by the function:

• SP :

T → P(G SP )
This is defined recursively. If a ∈ A, t i ∈ T, and 1 ≤ i ≤ k , then

a SP = { a -→} OR(t1, . . . , t k ) SP = k i=1 ti SP AND(t1, . . . , t k ) SP = {G1 || . . . || G k | (G1, . . . , G k ) ∈ t1 SP × . . . × t k SP } SAND(t1, . . . , t k ) SP = {G1 • . . . • G k | (G1, . . . , G k ) ∈ t1 SP × . . . × t k SP }
where t SP = {G1, . . . , G k } corresponds to a set of possible attacks Gi Since, in this paper, we base the construction of the attack tree on penetration testing techniques, all leaves on the tree can be considered actions. The combination of these actions can be translated into the processes that form part of a test case. This is conducive to the use of process algebra such as Communicating Sequential Processes (CSP) and furthermore the equivalence of the semantics (see Section 3.2) means that we can use synonymous operators to transform a pre-built attack tree.

CSP

We give here a brief overview of the subset of CSP that we use in this paper. A more complete introduction may be found in [START_REF] Roscoe | Understanding Concurrent Systems[END_REF].

Given a set of events Σ, CSP processes are defined by the following syntax:

P ::= Stop | e → P | P 1 2 P 2 | P 1 ; P 2 | P 1 A P 2 | P 1 ||| P 2
where e ∈ Σ and A, B ⊆ events. For convenience, the set of CSP processes defined via the above syntax is denoted by CSP.

To mark the termination of a process, a special event is used.

In the above definition, the process Stop is the most basic one, which does not engage in any event and represents deadlock. In addition, Skip is an abbreviation for → Stop. It only exhibits and then behaves as Stop.

The prefix e → P specifies a process that is only willing to engage in the event e, then behaves as P . The external choice P 1 2 P 2 behaves either as P 1 or as P 2 . . The sequential composition P 1 ; P 2 initially behaves as P 1 until P 1 terminates, then continues as P 2 .

The generalised parallel operator P 1 A P 2 requires P 1 and P 2 to synchronise on events in A ∪ { }. All other events are executed independently. Finally, the interleaving operator P 1 ||| P 2 allows both P 1 and P 2 to execute concurrently and independently, except for .

There are different semantics models for CSP processes [START_REF] Roscoe | Understanding Concurrent Systems[END_REF]. For the purpose of this paper, we recall the finite trace semantics. A trace is a possibly empty sequence of events from Σ and may terminate with . As usual, let Σ * denote the set of all finite sequences of events from Σ, the empty sequence, and tr 1 tr 2 the concatenation of two traces tr 1 and tr 2 ; then the set of all traces is defined as

Σ * = {tr en | tr ∈ Σ * ∧ en ∈ { ,
}}. The trace tr 1 is a prefix of a trace tr 2 , written as tr 1 ≤ tr 2 , iff ∃ tr : tr 1 tr = tr 2 . Events in A ⊆ Σ ∪ { } may be abstracted away from a trace tr by a hiding operator, written as tr \ A and defined as

tr \ A =      if tr = a (tr \ A) if tr = a tr ∧ a / ∈ A tr \ A if tr = a tr ∧ a ∈ A.
For convenience, when A = {a}, we shall simply write tr \ a. In general, the trace semantics of a process P is a subset traces(P ) of Σ * consisting of all traces which the process may exhibit. It is formally defined recursively as follows:

- ∈ A:

• A = { }; A a = ∅; A b = { b }; • a tr 1 A b tr 2 = { b tr | tr ∈ a tr 1 A tr 2 }; • a tr 1 A a tr 2 = { a tr | tr ∈ tr 1 A tr 2 } • a tr 1 A a tr 2 = ∅ where a = a ; • b tr 1 A b tr 2 = { b tr | tr ∈ tr 1 A b tr 2 }∪ { b tr | tr ∈ b tr 1 A tr 2 } -traces(P 1 ||| P 2 ) = {tr ∈ tr 1 ||| tr 2 | tr 1 ∈ traces(P 1 ) ∧ tr 2 ∈ traces(P 2 )} where tr 1 ||| tr 2 = tr 1 ∅ tr 2 .
Therefore, traces(P

1 ||| P 2 ) = traces(P 1 ∅ P 2 ).
A process P is said to trace-refine a process Q (written Q T P ) if traces(P ) ⊆ traces(Q). There are other flavors of refinement, but we restrict ourselves to trace refinement below.

Methodology

In this section we present an overview of the whole methodology (Figure 1) of our paper. The context of our work is the automotive industry. Vehicle manufacturers often incorporate off-the-shelf (OTS) components into their work, and their specifications are not always available. Manufacturers thus have to approach testing with this uncertainty.

We begin by assuming a System under Test (SUT), which may be either an OTS component or contain one. We also assume the existence of a corresponding attack tree (see Figure 1). Section 6 illustrates our approach with an attack tree developed for a vehicle network that includes a Bluetooth connection. It is worth observing here that an attack tree for Bluetooth systems essentially systematises the known attacks on Bluetooth, and therefore although it may be updated as new attacks are constructed, the development of the attack tree is a one-off cost. The same attack tree will work for any Automotive Bluetooth system.

If a specification (or abstract model) of the SUT is available we use it, but in many cases (including the example in Section 6) the specification of the SUT is confidential or contains confidential components. In this case we can underapproximate a specification to begin the process. Successive iterations of the process allow us to refine this under-approximation. We illustrate this underapproximation in Section 5. The approach is to generate tests against this model. Tests are automatically generated using FDR, the refinement checker for CSP. The specification and the attack tree are compared. Each possible route through the attack tree represents a potential attack, and the Test Case Generator compiles a list of all the attacks that the specification permits. Note that in the case of an under-approximated specification all possible attacks will be permitted.

The next step is to convert the formal tests into implementation tests. This process is detailed in Section 5.2. Note that these implementation tests are in fact attacks (or potential attacks) on the SUT. Not all the test implementation tests generated from an attack tree can be fully automated. The attack tree may contain nodes that require manual input, in which case the implementation tests will require (partial) manual interaction. The ones that do not require manual input may be executed directly on a Testbed. The report contains the test results. Since tests are really attacks on the SUT, we consider a test to be successful if the attack succeeds.

In the remainder of this section we present in more detail the transformation of attack trees to CSP processes (Section 4.1), as well as a proof of the equivalence of the semantic models.

Transforming Attack Trees into CSP processes

In this section we use the process algebra CSP to describe the attack tree. We choose CSP because as a process algebra it is able to represent and combine the actions of the attack tree into a set of processes that could subsequently be used for test case generation.

In principle, the logic gates of the attack tree can be considered CSP operators [START_REF] Hoare | Communicating Sequential Processes[END_REF] as follows:

-Since the AND logic gate demands that all actions must be successful for the branch to be considered complete, the interleave operator ( ||| ) is used. This operator joins processes that operate concurrently but without them necessarily interacting or synchronising. -The sequential composition operator ( ; ) is used for the SAND logic gate. The former echoes the SAND logic gate, in that the first process must terminate successfully before the next is allowed; -The external choice operator ( 2 ) (where any process could be chosen dependent on the environment in which it operates) is used for the OR logic gate.

Formally, we define the following transformation function trans : T SAND → CSP where Σ = A:

trans(a) = a → Skip for a ∈ A; trans(OR(t 1 , . . . , t n )) = trans(t 1 ) 2 . . . 2 trans(t n ); trans(AND(t 1 , . . . , t n )) = trans(t 1 ) ||| . . . ||| trans(t n ); trans(SAND(t 1 , . . . , t n )) = trans(t 1 ); . . . ; trans(t n );

In order to show the correctness of the above transformation, it is necessary to make the two semantics in G SP and Σ * compatible for comparison. Recall from [START_REF] Jhawar | Attack Trees with Sequential Conjunction[END_REF] that each SP graph represents a possible way to carry out an attack. In such a graph, an AND vertex indicates that actions along its branches must be executed. However, there is no restriction on the order of their executions. In other words, their executions are interleaving in general. Therefore, it is possible to serialise the actions from a SP graph where parallel compositions of graphs is considered as interleaving and sequential composition as concatenation. Given G in G SP , let serials(G) denote the set of all possible ways to serialise G, which is formally defined as follow:

serials(

a -→) = { a }; -serials(G 1 G 2 ) = {tr ∈ tr 1 ||| tr 2 | tr 1 ∈ serials(G 1 ) ∧ tr 2 ∈ serials(G 2 )}; -serials(G 1 • G 2 ) = {tr 1 tr 2 | tr 1 ∈ serials(G 1 ) ∧ tr 2 ∈ serials(G 2 )}.
For convenience, we denote the set of all prefixes from serials(G) by pserials(G), i.e., pserials(G) = {tr | ∃ tr ∈ serials(G) : tr ≤ tr }. We also denote pserials(t) = G∈ t SP pserials(G) for all attack trees t ∈ T SAND .

The correctness of transforming attack trees into CSP processes is guaranteed by the following result:

Lemma 1. ∀ t ∈ T SAND , pserials(t) = traces(trans(t)) \ .
Proof. The proof is done by induction on the structure of t. Base case: Consider t = a; then, t SP = { a -→} and pserials(t) = { , a }. We also have trans(t) = a → Skip and traces(trans(t)) = { , a , a, }. Hence, it is straightforward that pserials(t) = traces(trans(t)) \ . -

Induction step: Case t = OR(t 1 , . . . , t n ): It is straightforward that -t SP = i=1,...,
tr ∈ pserials(t) ⇔ ∃ G ∈ t SP : tr ∈ pserials(G) ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP : tr ∈ pserials(G 1 . . . G n ) ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP , tr ∈ serials(G 1 . . . G n ) : tr ≤ tr ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP , tr i ∈ serials(G i ) : tr ∈ tr 1 ||| . . . ||| t n ∧ tr ≤ tr ⇔ ∀ i ∈ {1, . . . ,
t SP = {G 1 • . . . • G n | G i ∈ t i SP ∀ i = 1, .
. . , n}, and traces(trans(t)) = traces(trans(t 1 ); . . . ; trans(t n )). Then we have:

tr ∈ pserials(t) ⇔ ∃ G ∈ t SP : tr ∈ pserials(G) ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP : tr ∈ pserials(G 1 • . . . • G n ) ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP , tr ∈ serials(G 1 • . . . • G n ) : tr ≤ tr ⇔ ∀ i ∈ {1, . . . , n}, ∃ G i ∈ t i SP , tr i ∈ serials(G i ) : tr ∈ tr 1 . . . t n ∧ tr ≤ tr ⇔ ∀ i ∈ {1, . . . ,

Implementation

We provide a prototype implementation of our proposed methodology. This implementation is built using Python 2.7 and requires as input an attack tree and a formal model of the SUT. It then automatically carries out three main tasks:

(1) translates an input attack tree into a CSP process; (2) uses this process and the formal model of the SUT to generate test cases; and (3) executes all the generated test cases by associating each one with a sequence of predefined primitive test scripts. Task 1 is a straightforward implementation of function trans from Section 4.1. In the rest of this section, we discuss the implementation of tasks 2 and 3 in detail.

Test Case Generation

Let us assume that the formal model of the SUT is given as a CSP process Sys. Furthermore, the behaviours of the attacker are also given in terms of an attack tree t, which is then transformed into a CSP process trans(t). We shall use trace refinement in CSP to extract test cases following [START_REF] Nogueira | Test generation from state based use case models[END_REF]. To this end, trans(t) acts as a filter criterion to select test cases among all possible runs of the system captured by Sys. As in [START_REF] Nogueira | Test generation from state based use case models[END_REF], we define a fresh event attackSucceed to mark the end of an attack, which indicates that an attack is successfully executed. We form the following filter TestPurpose = trans(t); (attackSucceed → Stop) which captures all attacks extended with the marking event attackSucceed at the end. Then, we establish the following trace refinement:

Sys 2 TestCases T Sys Σ\{attackSucceed} TestPurpose
In this refinement, TestCases encodes test cases that have previosuly been generated. By combining it with Sys using the external choice operator, a fresh test case, i.e., different from the generated ones, will be generated if one exists. Sys

Σ\{attackSucceed}

TestPurpose encapsulates all attack traces that can be carried out with respect to the formal model Sys. These attack traces are ended with the marking event attackSucceed, which does not belong to Sys, hence, gives rise to counter examples of the refinement. Initially, TestCases = TestCases 0 = Stop, i.e., corresponding to an empty set of test cases. This refinement is checked by calling FDR [START_REF]FDR3 -The CSP Refinement Checker[END_REF]. If an attack trace exists, FDR will provides a counter example of the form a 1 , . . , a n , attackSucceed where a 1 , . . . , a n ∈ Σ \ {attackSucceed}. We encode this trace as a test case tc 1 = a 1 → . . . → a n → attackSucceed → Stop. After TestCases is rebuilt as TestCases = TestCases 1 = TestCases 0 2 tc 1 , the above refinement check is called again and again to extract further test cases tc 2 , . . . and to construct TestCase 2 , . . . until no further counter example can be found. In this implementation, the calls to checking refinements and extracting counter examples are facilitated by API functions provided by FDR [START_REF]FDR3 -The CSP Refinement Checker[END_REF].

Test Case Execution

Test cases that are generated can now be assigned programmatic functions that would allow for execution. This is dependant on implementation of the system and so would necessarily be specific rather than abstract. Furthermore, as the attack tree in this case is based on penetration testing, not all actions (such as "social engineering") are scriptable, largely due to requiring manual intervention. All such actions are indicated in the implementation.

Given an attack tree t, let scriptable(t) denote the set of its scriptable leaves. Then, each scriptable leaf a ∈ scriptable(t) is associated with a primitive test script script(a). A generated test case tc = a 1 → . . . → a n → attackSucceed → Stop is automatically executable if a i ∈ scriptable(t) for all i = 1, . . . , n. Then, executing an automatically executable test case means to execute all test scripts script(a 1 ), . . . , script(a n ) sequentially. If all such scripts are executed successfully, the test case is called passed, otherwise failed. Note that a passed test case means that the SUT is not secure with respect to the attack encoded by this test case. Conversely, the SUT is impervious to this attack.

In this paper, we use the example of an aftermarket on-board diagnostics (OBD-II) dongle attached to the vehicle (see Section 5). Executable test cases are written in Python 2.7 to enable compatibility with Bluetooth functions.

Case study

We take here a case study of evaluating the intra-vehicular network with the attack goal of vehicle compromise. The attack tree (see Section 6.2) for this goal is based around access through a Bluetooth-enabled aftermarket device that attaches to the vehicle's on-board diagnostic (OBD-II) port. These devices were originally created so that enthusiasts and hobbyists were able to read information from their own vehicles for diagnostic and maintenance purposes. The devices (or dongles) contain an ELM327 chip [START_REF]ELM Electronics: OBD[END_REF] which serves as an RS-232 interpreter. "Attention Modem" (AT) commands are used to configure the chip through any serial terminal. The device used for this case study was the OBDLINK MX, with an ELM chip version of 1.3, attached to a 2013 small hatchback from a major manufacturer. Through such a device, an attacker is able to gain access to the intra-vehicular CAN bus remotely and potentially push messages directly into the vehicle [START_REF]Argus Cybersecurity: Argus Cyber Security Working With Bosch to Promote Public Safety and Mitigate Car Hacking[END_REF][START_REF] Cheah | Threat Intelligence for Bluetooth-enabled Systems with Automotive Applications : An Empirical Study[END_REF]. The risk of compromise is exacerbated by the fact that these OBD-II devices are usually highly insecure, being wireless, and with weak PINs that are made public (such as 0000 or 1234) [START_REF] Oka | Survey of Vehicle IoT Bluetooth Devices[END_REF].

Vehicular Communications

Messages that are sent through the dongle on to the CAN bus takes the form of either a raw Controller Area Network (CAN) frame (Section 6.1) or a diagnostic message (Section 6.1) (that is translated into a CAN frame by the dongle). CAN Messages. The CAN protocol is the primary mode of communication inside the vehicle. The latest version is CAN 2.0, first specified in 1991 [START_REF] Bosch | CAN Specification version 2.0[END_REF] and embodied as an ISO standard (ISO11898) in 2003.

The standard CAN packet comprises (up to) 11 bits for the message ID, followed by (up to) 8 bytes of data, then a cyclic redundancy check (16 bits) for error detection. The full 8 bytes of data need not be used. Information for a door sensor, for example, may only require 1 bit. Conversely a message can be spread across many frames.

Arbitration, should nodes on the CAN network transmit simultaneously, is based on message prioritisation. This prioritisation is determined using the message ID, with the lowest ID being the highest priority; implementation usually means that mission-critical messages are the ones assigned lower IDs.

Assignment of IDs along with data payload is manufacturer specific, however, reuse is common to save on the cost of redesigning a network [START_REF] Pretschner | Software engineering for automotive systems: A roadmap[END_REF].

Reverse engineering of CAN messages is difficult considering volume and variety of content that is transmitted. This is especially the case without an Original Equipment Manufacturer's (OEM's) typically confidential CAN database, which contains definitions for every message and signal. However, specific CAN messages for discrete events (such as unlocking doors) can be obtained relatively easily through trial and error.

CAN data is transmitted in a bus configuration; any Electronic Control Unit (ECU) on the network has access to all messages. There is no addressing; each ECU listens to a set of IDs which then triggers pre-determined functionality. Diagnostic Messages. Parameter IDs (PIDs) are used to perform diagnostic functions or request data from the vehicle specifically through OBD-II port; done through a query-response mechanism where a PID query comprises the CAN ID 7DF followed by 8 data bytes. The first byte is data length (usually 02) with the second byte the mode and the third byte typically the PID. The combination of modes and PIDs can then be transmitted and a response received from whatever in-vehicle module is responsible. The response CAN ID is typically 8 (in hex) higher than the message ID that the responding ECU answers to.

The first ten modes (01 to 0A, described in SAE J1979 (E/E Diagnostic Test Modes) [START_REF]E/E Diagnostic Test Modes[END_REF], are standard to all compliant vehicles: PID is only the 2nd byte, with the 3rd to 8th byte unused. With non-standard modes, PIDs could extend to 3rd byte. Manufacturers, are not obliged to implement all standard commands, and additionally could also define functions for non-standard PIDs. There is much information that could be gathered through this port. For example, sending the mode 09 with PID 02 retrieves the Vehicle Identification Number (VIN), which is unique to vehicles, used for maintenance to recovery of stolen vehicles.

Attack Tree Translation

The attack tree used for this case study is shown in Figure 2. Figure 2 also lists test scripts corresponding to leaves in this attack tree. If a leaf is not scriptable, it is denoted as a manual leaf.

The function trans(Vehicle Compromise) (see Section 4.1), gives the translation of this tree into CSP as below: Reconnaissance was defined as "to find as much information as possible" (meaning the subsequently generated formal attack tree would be much larger). Many of the steps were manual and non-sequential.

Results

We generate test cases using the implementation in Section 5.1. Given the small size of the attack tree, we use the most abstract model for the SUT where all behaviours are accepted (the most insecure model) to generate a total of 15 test cases. Results from the run of test cases against an actual implementation are given in Figure 1. Three of the test cases passed (i.e. they were executed successfully) (see Figure 3). We highlight test case 3 (TC 3 in Figure 3) for further analysis.

The action of flooding with a particular diagnostic message resulted in loss of function in the vehicle of both electronics and engine. This violates the security property of availability by causing a denial of service. Additionally, injection of messages into the CAN bus also changes the stream of CAN bus signals that would normally be expected in vehicles. This violates the security property of integrity (in which no unauthorised modification should be allowed). Protecting against this could involve the addition of gateways in the SUT, which could either filter out floods of messages (by defining thresholds for the number of these messages that could be sent through at any given time). Alternatively, such messages (unless from an authorised source) could be disallowed completely.

The other test cases (all involving permutations of finding a link key, and changing the address) were not scripted because they required manual intervention. The former because it would need a remote device set to enable logging on the Host Controller Interface (not always possible) or to manually acquire data from a vehicle to find where the link key has been stored (which would have required hardware removal). The latter is automatable (for example, using a tool called Spooftooph [START_REF] Dunning | Spooftooph[END_REF]), however, either hardware removal or social manipulation is involved to find knowledge of an address that is already stored on the vehicle.

Other branches that were unscripted involves reverse engineering CAN messages to inject, which involves manual trial and error due to the sheer volume and variety of messages that are on the CAN bus at any one time. Using an OEM CAN database would enable automation, but availability is often non-existent due to commercial confidentiality. The branch that ended with successful test cases all involved using a legitimate device. That is, a device that was under our control, which we could use to test weaknesses in the vehicular implementation.

Conclusion and Future Work

We have demonstrated the translation of an informal attack tree into a formal structure using the process algebra CSP and proved equivalence. We use this tree to generate test cases automatically, and assign executions to scriptable test cases. We execute the test cases on a real-world vehicle (although this could be substituted with a testbed, with input from an OEM to reflect a real architecture, without the cost or risk to a test vehicle [START_REF] Fowler | Towards a testbed for automotive cyberecurity[END_REF]). Thus, the full testing process is one step further to automation, and furthermore, the formal model of the attack tree could also be used for formal verification should the specifications of the systemunder-test be available. Limitations are around how a tree is created (still largely manual) and certain actions within the attack tree requiring manual intervention. The aim is for the entire process (at an abstract level) to resemble Figure 1. The work with testbeds (as in work done by [START_REF] Fowler | Towards a testbed for automotive cyberecurity[END_REF]) as well as manual testing could continue to assist in further refinement of the models created.

1 AP 2 ) = {tr ∈ tr 1 Atr 2 | 1 Atr 2 = tr 2 A

 1212122 traces(Stop) = { }; traces(e → P ) = { } ∪ { e tr | tr ∈ traces(P )}; traces(P 1 2 P 2 ) = traces(P 1 ) ∪ traces(P 2 ); traces(P 1 ; P 2 ) = traces(P 1 ) ∩ Σ * ∪ {tr 1 tr 2 | tr 1 ∈ traces(P 1 ) ∧ tr 2 ∈ traces(P 2 )}; traces(P tr 1 ∈ traces(P 1 ) ∧ tr 2 ∈ traces(P 2 )} where tr tr 1 is defined as follows with a, a ∈ A and b, b /

Fig. 1 .

 1 Fig. 1. Overview of our formal systematic security methodology

Attacker =Fig. 2 .

 2 Fig. 2. Attack tree, with attack goal of compromising the vehicle through an aftermarket Bluetooth-enabled OBD-II device

  n}, ∃ tr i ∈ traces(trans(t i )) \ : tr ∈ tr 1 ||| . . . ||| t n ∧ tr ≤ tr by induction hypothesis ⇔ ∀ i ∈ {1, . . . , n}, ∃ tr i ≤ tr i ∈ traces(trans(t i )) \ : tr ∈ tr 1 ||| . . . ||| t n ⇔ tr ∈ traces(trans(t)) \ . Case t = SAND(t 1 , . . . , t n ): It is obvious that:

  n}, ∃ tr i ∈ traces(trans(t i )) \ : tr ∈ tr 1 . . . t n ∧ tr ≤ tr by induction hypothesis ⇔ ∀ i ∈ {1, . . . , n}, ∃ tr i ≤ tr i ∈ traces(trans(t i )) \ : tr ∈ tr 1 . . . t n ⇔ tr ∈ traces(trans(t)) \ .

Table 1 .

 1 Test cases that were run against a real world vehicle

	TC# Execution result
	1	unexecutable action Find the link key from local or remote device
	2	unexecutable action Change address of local device
	3	Passed
	4	unexecutable action Find the link key from local or remote device
	5	unexecutable action Change address of local device
	6	Passed
	7	unexecutable action Find the link key from local or remote device
	8	Passed
	9	unexecutable action Using OEM CAN database
	10	unexecutable action action Using reverse engineering
	11	unexecutable action Change address of local device
	12	unexecutable action Find the link key from local or remote device
	13	unexecutable action Change address of local device
	14	unexecutable action Change address of local device
	15	unexecutable action Find the link key from local or remote device

TC (3) = action Determine pairing status → action Connect to serial port → action Flood with set OBD messages → attack succeed → Stop TC (6) = action Determine pairing status → action Connect to serial port → action Run through standard → action Run through non standard → attack succeed → Stop TC (8) = action Determine pairing status → action Connect to serial port → action Using passive monitoring → action Send flood with CAN messages → attack succeed → Stop Fig. 3. Test cases that succeeded


Pau Conejero-Alberola

M Francisca Hinarejos
email: xisca.hinarejos@uib.es

Josep-Lluís Ferrer-Gomila

A Selective Privacy-Preserving Identity Attributes Protocol for Electronic Coupons

Keywords: E-coupon, Security, Identity, Privacy

Electronic coupons (e-coupons) are a very effective marketing tool. In some scenarios, it is necessary to check some customer's personal attributes at the redeeming phase (e.g. age, title, citizenship, etc.). But customers may be reluctant to use e-coupons if their privacy is in danger. Digital certificates and credentials could be suitable for validating customer attributes. However, a bad use of such electronic documents entails a loss of privacy, revealing more identity attributes than necessary. Here, we present the first secure protocol for e-coupons, achieving verification proofs of identity, with selective disclosure of customer's certified attributes. On the other hand, our proposal meets other necessary security requirements, such as forging protection and doubleredeem protection.

Introduction

A coupon is a usually small piece of printed paper that lets you get a service or product for free or at a lower price (Merriam-Webster definition). It is an effective marketing instrument [1], and quite used because merchants and customers are benefited. One one hand, merchants can increase loyalty of their customers or attract new customers. On the other hand, customers can achieve better prices or gifts. In this paper we deal with a type of e-coupon that is addressed to a group of customers that must meet certain identity requirements, for example, being in a certain age group, being resident in a specific country, etc. A real example of this type of promotions is found in a well-known chain of hamburgers [START_REF]Terms and Conditions -Christmas promotion 31 days[END_REF], whose promotional bases indicate: customers must be over a certain age, resident in X, and have to purchase product Y.

Paper based coupons, redeemed face-to-face, allow the merchant to easily verify compliance with established requirements, using paper documents (such as an identity card). Such verification does not usually result in a high loss of privacy, because verification is instantaneous without the merchant registering private information of the customers in their systems. But in the case of e-coupons, exchanges are made electronically, and therefore "verification documents" must also be in electronic form to be redeemed face-to-machine.

Digital certificates and credentials are suitable to provide authenticated information about customers. These documents are signed by a trusted third party, which assumes the responsibility of validating the data contained in them. But those documents contain more information than may be necessary in certain ecoupon scenarios, with the consequent risk of loss of privacy. As a result, many customers are reluctant to provide personal data, beyond the strictly necessary for the purpose they want to perform. Our goal is to maximize the privacy of customers, that is, only that information strictly necessary to validate compliance with the requirements of the e-coupon must be disclosed.

Contribution. We present the first e-coupon scheme with a selective and verified personal data disclosure mechanism, which provides a better degree of privacy, allowing the issuance of e-coupons for eligible customers. On the other hand, customer's compliance of requirements is verified during the redeem.

This paper is organized as follows. Section 2 reviews the related work. Section 3 defines the proposed scheme, the security requirements and the cryptographic background. Section 4 specifies in detail all the phases of the proposed protocol. Section 5 includes a brief security analysis, and finally, Section 6 lists the conclusions of this paper.

Related work

In this section, we will review those most significant proposals that have shown concern about the authentication and privacy of customers.

As a first contribution of e-coupons, Kumar et al. [START_REF] Kumar | Sales promotions on the Internet[END_REF] show that targeted ecoupons are intended for a group of customers who meet certain requirements, and they indicate that customers must be identified.

In contrast, Jakobsson et al. [START_REF] Jakobsson | Secure and lightweight advertising on the web[END_REF] state that an e-coupon system should not expose customer privacy more than other advertising system. They present a proposal where no attribute of the customer is verified.

Chang et al. [START_REF] Chang | A Secure E-coupon System for Mobile Users[END_REF] present a scheme with a registration phase, where the customer provides personal information to the issuer. Therefore, e-coupons are identified, but merchants do not receive this information from the customer.

Aigner et al. [START_REF] Aigner | A system of secure virtual coupons using NFC technology[END_REF] explain two e-coupon schemes. One of them has an authentication process for the customer in front of the issuer and merchant.

Chang et al. [START_REF] Chang | A secure and efficient authentication scheme for ecoupon systems[END_REF] explain a scheme where the customer and merchant must be registered at a trusted third party, indicating a mutual authentication.

Chang et al. [START_REF] Chang | Secure electronic coupons[END_REF] provide two e-coupon schemes, one for specific registered customers (with better discounts) and the other for non-specific customers.

Liu et al. [START_REF] Liu | Efficient E-coupon systems with strong user privacy[END_REF] provide a proposal, in which customers remain anonymous if they are honest. Their scheme achieves traceability against dishonest customers.

As a conclusion, we can affirm that there is no previous solution that requires the authentication of some attributes of the customer, and that this authentication takes place without revealing other data related to that customer. That is, the selective disclosure of attributes is a problem that has not been addressed so far in the area of e-coupons.

Scheme: Scenario and Security

In this section, we describe our proposal. First, we detail the scenario, the entities involved, their role and we outline the e-coupon structure. Then, the security requirements and the cryptographic background are defined.

Scenario

We define a custom environment, offering an online distribution marketing portal, using daily e-coupons promotions to be redeemed in manufacturer's branches for eligible and registered customers. The proposed scenario allows different grades of privacy using an Idemix [START_REF] Camenisch | A formal model of identity mixer[END_REF] service, a selective method to disclose customer identity attributes. We consider the following entities: Trusted Third Party (TTP), Issuer, Merchant and Customer.

Trusted third party T is in charge of issuing the Idemix credentials based on a digital certificate, and carrying the system public parameters.

Issuer I is in charge of issuing and distributing e-coupons. In this scenario, I has to ensure that the credential has not been used previously for registering, and only one-time e-coupon is delivered per customer C. A registered C can request the e-coupon policy from the portal, which defines the redemption requirements to compute the identity proof. If the proof is valid then I issues the e-coupon.

Merchant M is in charge of verifying if the e-coupon is valid and has not been used before at the same M. As the e-coupon was issued for a specific C, the merchant M has to ensure if C has the right to use it.

C is the actor who makes use of the platform to generate the identity proofs of its credential attributes, and requests and redeems the e-coupons.

Next, the promotional e-coupon is detailed as follows: SN represents the identifier of the selected e-coupon, I 1 includes the offer data of the promotion, I 2 contains all the public parameters to prove the ownership of the e-coupon during the redemption phase, and T 1 -T 2 define the time interval for redeeming.

Security requirements

The protocol has to consider and guarantee the following security requirements:

-Owner authentication: Merchants should be able to verify the customer's e-coupon ownership during the redeem phase. -Anonymity: The system has to provide full anonymity during the registration phase and redeem phase. The scheme allows a selective personal data disclosure during the issuance phase. -Unforgeability: All the parts have to be able to verify if an e-coupon has been issued by an authorized issuer, and if the e-coupon has not been manipulated. -Double-redeem protection: The system must provide protection about intents of reusing an e-coupon at the same merchant in an offline mode. -Issuer non-repudiation: Once a valid e-coupon has been issued, issuer should not able to deny it. -Non-transferability: Customers should not be able to share e-coupons.

Cryptographic background

We briefly review the cryptography techniques that will be used in our proposal.

ZKP: Zero-knowledge proof

The aim of a zero-knowledge proof is to prove the validity of a statement given to a verifier. This kind of proof is suitable to prove the possession of a secret without revealing the content. The Schnorr protocol [START_REF] Schnorr | Efficient signature generation by smart cards[END_REF] is an identification scheme based on discrete logarithms, that can be used as a interactive zero knowledge proof. Figure 1 shows in detail the three steps (commitment, challenge and response) involved in the protocol.

ABC: Attribute-Based Credential

The aim of an attribute-based credential is to provide an authentication mechanism based on a selective attributes method. In this way, every credential contains attributes that the user can either reveal or keep hidden. Idemix is an ABC protocol based on a Camenisch-Lysyanskaya (CL) signature scheme [START_REF] Camenisch | A Signature Scheme with Efficient Protocols[END_REF], that provides a solution for strong privacy-preserving authentication with a disclosure method of certified attributes. Table 1 defines the Idemix parameters involved in the protocol.

Proposal

This section is divided into two main subsections. The first subsection defines the prerequisites for the system set-up, and the second subsection explains in detail each step of the proposed protocol.

V

System Set-up

In this scheme, the entities T and I previously generated an asymmetric key pair. As a first step, C generates a master secret key x as m H1 and enrolls a digital residence certificate with two fields: P ersonalID as m H2 and Zipcode as m H3 in T . Then, T generates a serial number attribute to identify the credential as m K1 . Once the structure of the credential is defined, both parties agree to run the CL-signature scheme (Algorithm 1) to create the signature over the attributes specified in the credential structure. As a first step, C calls the function CL.commit to build the commitment for each of the hidden {m Hi } attributes using the system parameters retrieved from T ((n, S, Z, {R i } i∈M )). As a result, C obtains U as an aggregation of commitments. Then, C sends U to I, and I has to call the function CL.sign to prepare the pre-signature with the aggregation of U and the known {m Ki } attributes. Finally, I sends the pre-signature to C, and C calls the function CL.build to compute the signature. Figure 2 shows the credential [(m H1 , m H2 , m H3 , m K1 ),(CL Signature)].

Algorithm 1 Camenisch-Lysyanskaya signature

1: function CL.commit({m i } i∈M H , (n, S, Z, {R i } i∈M )) 2:
v ← Random( )

3:

U ← S v mod n

4:

for each i ∈ M H do 5:

U ← U • R m i i mod n 6: return (U, v )
7: function CL.sign(U, {m i } i∈M \M H , (n, S, Z, {R i } i∈M ), (p , q )) 8:

v ← Random( )

9:

U ← U • S v mod n 10:

for each i ∈ M \ M H do 11: U ← U • R m i i mod n 12: Q ← Z • U -1 mod n
13:

e ← RandomPrime( )

14:

d ← e -1 mod (p • q )

15:

A ← Q d mod n 16: return (A, e, v )
17: function CL.build(v , (A, e, v )) 18:

v ← v + v 19: return (A, e, v)
Fig. 2. Idemix credential structure

Phases

The phases of our system are: Customer registration, where the system checks the eligibility of the user and gets registered in the portal; Issue, that consists of selecting an eligible promotion and disclose the required identity attributes for issuing an e-coupon; Redeem, where the customer redeems an e-coupon at a merchant. Table 2 defines the notation used in the description of the phases. Phase 1 Customer registration As a first step, C contacts with I to prove her eligibility to be registered in the portal, following the protocol flow described in Figure 3. Then, I sends a random value n i to C, required to build a proof (Algorithm 2). First, C has to define the proof specification, which contains the disclosed and undisclosed attributes. That is, m K1 as a known attribute, while m H1 , m H2 , m H3 remain hidden. During the registration phase there is not a disclosure of hidden attributes. C calls the function ProveCL.randomise to generate a randomised signature, and the function ProveCL.tvalues to compute the commitment T over the aggregation of the undisclosed attributes, and the randomised signature (t-values). Next, C calls the ProveCL.challenge function to compute the challenge c, and computes the responses {s i } for every t-value. As a result, the following certified and signed P proof is generated: P=(c,(ê, v, { m1 }, { m2 }, { m3 }), common). The computed proof P will be used to demostrate the eligibility of C as a physical person who has certified attributes. r ← Random( )

3:

A ← A • S r mod n 4:

Common ← A 5: v ← v -e • r 6: return (e, v ), A 7: function ProveCL.tvalues([{m i } i∈m H , (n, S, Z, {R i } i∈M )], (A )) 8: ẽ ← Random( ) 9: ṽ ← Random( ) 10: Z ← A ẽ • S ṽ mod n 11: for each i ∈ m H do 12: mi ← Random( ) 13: Z ← Z • R mi i mod n 14: return (ẽ, ṽ, { mi } i∈m H ), Z
15: function ProveCL.challenge(context, common,T, n i ) 16:

c := H(context, common,T, n i ) 17: return (ê, v, { mi } i∈m H ) 18: function ProveCL.svalues({m i } i∈m H , (e, ẽ, ṽ, { mi } i∈m H ), c) 19: ê ← ẽ + c • e 20: v ← ṽ + c • v

21:

for each i ∈ m H do 22:

mi ← mi + c • m i 23: return (ê, v, { mi } i∈m H ) Algorithm 3 Verify Proof 1: Protocol : V erif yP roof [ IN: {S, (c,s-values,common), n i }, OUT: { accept or reject P} ] 2: V erif yCL.tvalues(S,P) → T ' 3: V erif yCL.challenge(context,common,T ',n i ) → c' 4: return If c ≡ c' accept P or reject otherwise Algorithm 3.1 Verify CL 1: function VerifyCL.tvalues([{m i } i∈m K ), (n, S, Z, {R i } i∈M ), [c, (ê, v, { mi } i∈m H ), A ]) 2: Ẑ ← Z -c • A ê • S v mod n 3:
for each i ∈ m K do 4:

Ẑ ← Ẑ • R c•m i i mod n 5:
for each i ∈ m H do 6:

Ẑ ← Ẑ • R mi i mod n 7:
return Ẑ 8: function VerifyCL.challenge(context, common,T , n i ) 9:

c := H(context, common,T, n i ) 10:

return c
Phase 2 Issue protocol When C wants to request a promotion from the portal, has to follow the protocol flow described in Figure 4. As a first step, she has to request the specified e-coupon using its SN . Next, I replays with the policy of the selected e-coupon and a fresh random number n i to C, required to build a proof (Algorithm 2). First, C has to use the proof specification of the received promotion policy, which defines the disclosed and undisclosed attributes to be proven. In our schema all the promotions have to be redeem by customers who live in a specified area. So, the zip code attribute m H3 has to be disclosed as m K2 to check the residence requirement. That is, m K1 , m K2 are known attributes, while m H1 , m H2 remain hidden. C calls the function ProveCL.randomise to generate a randomised signature, and the function ProveCL.tvalues to compute the commitment T over the aggregation of the undisclosed attributes and the randomised signature (t-values). Next, C calls the ProveCL.challenge function to compute the challenge c, and computes the responses {s i } (s-values) for every t-value. As a result, the following certified and signed proof P is generated: P=(c,(ê, v, { m1 }, { m2 }), common). The computed proof P will be used to demostrate the residence area of C, in particular the zip code.

Phase 3 Redeem protocol

During the redeem protocol (see Figure 5), M has to check that Sign(Coupon) presented by C, is not a fake copy. Thus, M has to verify the signature using the I's pk I . If the verification is successful, M has to check if C is the legitimate owner of Coupon. To do that, M starts the Schnorr identity protocol (see Section 3.3) to verify if C is able to answer a generated challenge using the information inside the I 2 . M generates a time-variant random challenge c and sends it to C. Then, C has to compute the response s and send it back to M. As a result, M verifies the received response to know if C is eligible to redeem Coupon. If the verification is successful, M checks if the SN has not been used before, and if the time interval between T 1 and T 2 have not expired. If both verifications are successful, M redeem Coupon and stores the SN in a local non-persistent database. In our scheme, portal offers e-coupons with a small limited lifetime period of use since the moment that I issues the e-coupons. As a last step, M sends an ACK to C.

Security Analysis

In this section we include a brief security analysis of the following requirements:

1. Owner authentication: During the issuance phase, C generates a public value y linked to the master secret key x. Only the legitime owner of x will be able to resolve the challenge-response step during the redemption phase. 2. Anonymity: During the registration phase, C sends the disclosed attributes to I. In our scheme only the known attributes, as the serial number of the credential, was disclosed, while the other identity attributes remains hidden. 3. Unforgeability: I generates a digital signature Sign(Coupon) during the issuing phase. Any forged e-coupon that is not generated by I, or it is modified will be detected during the redemption verification as illegal. 4. Double-redeem protection: In our scheme we only consider the double-redeem issue if C tries to use the e-coupon more than one time in the same M, which is resolved by using a memory database to check the redeemed e-coupons. Also, there is a lifetime period to mitigate the impact if the same C tries to use the e-coupon in different M. In addition, it is possible to use a global database between all the merchants. 5. Issuer non-repudiation: A credential proof can be verified with the corresponding pk T , so the T can not deny it. An e-coupon can be verified with the corresponding pk I , so the I can not deny it. 6. Non-transferability: If C shares the e-coupon, it has to expose its master secret key x to other customers to pass the challenge-response step during the redeem phase. Thus, the protocol must to discourage customers to reveal a valuable secret which is linked with the credential.

Our proposal offers a portal to retrieve e-coupons, depending on the issuer promotion requirements. Customers can generate proofs from a digital certificate to prove identity requirements with a selective privacy mechanism. We offer a trusted registration mechanism providing anonymity. The design of the system has been performed taking into account security and privacy requirements described for e-coupons. As a future work, we want to extend this solution to other scenarios and build a prototype. Moreover, the security and the performance analysis will be presented in a formal way.

Fig. 1 .

 1 Fig. 1. Schnorr protocol

Fig. 3 .Algorithm 2

 32 Fig. 3. Redeem protocol flow

Fig. 4 .

 4 Fig. 4. Issue protocol flow C sends the generated proof P to I, and I has to verify the proof P (Algorithm 3). Then, I calls the function VerifyCL.tvalues to validate the received P, computing the aggregation of the randomised signature, the disclosed {m Ki } attributes and the undisclosed {m Hi } attributes. Then, I calls the function VerifyCL.challenge to compute the challenge c' to be compared against the received proof P. If the proof P is accepted, I sends an ACK to C. Then, C contacts with T to obtain the Schnorr public parameters to compute the Schnorr public key y and the Schnorr commitment t. After that, both values are sent to I. Next, I includes the Schnorr parameters obtained from C inside I 2 , and prepares all the remaining data to be included inside the Coupon as the offer information and the time interval to be redeem. As the last step, I signs the issued Coupon and delivers Sign(Coupon) to C.

Fig. 5 .

 5 Fig. 5. Redeem protocol flow

Table 1 .

 1 Idemix protocol parameters

	S	CL-signature scheme, Credential structure, Context
	x	Master secret key
	Master secret key attribute Credential/Proof hidden attributes Credential/Proof known attributes common Public parameters m H 1 m H i m K i
	T	Commitment prove values (Aggregation of t-values)
	T '	Commitment verify values (Aggregation of t-values)
	c	Challenge prove
	c'	Challenge verify
	s i	Response values (s-values)
	P	Proof = (c,s i ,common)
	n i	Random value

Table 2 .

 2 Protocol parameters

	x	Master secret key
	y	Schnorr public key
	z	Schnorr value
	t	Schnorr commitment
	c	Schnorr challenge
	r	Schnorr response
	P olicy	e-coupon promotion policy
	Coupon	SN | I 1 | I 2 | T 1 | T 2
	Sign(Coupon) I's signature on the e-coupon
	pk I pk T	Issuer public key Trusted Third Party public key

Acknowledgments. This work is partially financed by the European Social Fund and the Spanish Government under the projects TIN2014-54945-R and TIN2015-70054-REDC.