Ying He
email: yingh@dcs.gla.ac.uk

Chris Johnson
email: christopher.johnson@glasgow.ac.uk

Yu Lu

Arniyati Ahmad
email: a.ahmad.1@research.gla.ac.uk

Improving the Exchange of Lessons Learned in Security Incident Reports: Case Studies in the Privacy of Electronic Patient Records

Keywords: Lessons Learned, Security Incident, Electronic Patient Record, Generic Security Template, Empirical Study

The increasing use of Electronic Health Records has been mirrored by a similar rise in the number of security incidents where confidential information has inadvertently been disclosed to third parties. These problems have been compounded by an apparent inability to learn from previous violations; similar security incidents have been observed across Europe, North America and Asia. This paper presents the results of an empirical study that evaluates the utility and usability of conventional text-based security incident reports with a graphical formalism based on the Goal Structuring Notation. The two methods were compared in term of the users' ability to identify a number of lessons learned from investigations into previous incidents involving the disclosure of healthcare records. These lessons included both the causes of the incident but also the participants' ability to understand the reasons why particular recommendations were proposed as ways of avoiding future violations. Even using a relatively small sample, we were able to obtain statistically significant differences between the two approaches. The study showed that the graphical approach resulted in higher accuracy in terms of number of correct answers generated by participants. However, subjective feedback raised further questions about the usability of both approaches as the readers of security incident reports try to interpret the lessons that can increase the security of patient data.

Introduction

According to Symantec, the healthcare accounted for 42% in the total number of attacks on electronic information systems in 2012 [START_REF]Symantec: Internal security threat report 2011 trends[END_REF]. At 36% in 2013, healthcare continues to be the sector responsible for the largest percentage of disclosed data breaches by industry [START_REF]Symantec: Internet security threat report[END_REF]. Almost identical breaches have occurred across Europe, North America and Asia [START_REF] He | Generic security cases for information system security in healthcare systems[END_REF]. Learning from the incident enables the organisation to extract meaningful information from incidents, and use this information to improve security management systems [START_REF] Hadgkiss | Computer security incident response teams: Exploring the incident learning capability[END_REF]. Effective communication mechanism is needed to synthesis the information from the incident into the security incident management system so as to prevent a similar incident.

Popular communication mechanisms include formal reports, less formal meetings, newsletters, emails, as well as presentations to management [START_REF] Hadgkiss | Computer security incident response teams: Exploring the incident learning capability[END_REF]. However, the detailed incident reports that are produced in the post-incident activity [START_REF] Hadgkiss | Computer security incident handling[END_REF] have not been given enough attention. Those reports contain comprehensive information, which is typically classified into two types, business impact and remediation information [START_REF] Hadgkiss | Computer security incident handling[END_REF]. Business impact information involves how the incident is affecting the organisation in terms of mission impact, financial impact, etc. For example, "The missing external hard drive is believed to contain numerous research-related files containing personally identifiable information and/or individually identifiable health information for over 250,000 veterans, and information obtained from the Centres for Medicare & Medicaid Services (CMS), Department of Health and Human Services (HHS), on over 1.3 million medical providers" [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF], Remediation information information mainly refers to the suggested remediation actions, plans, procedures, and lessons learned. For example, "We recommend that the Assistant Secretary for Information and Technology revise VA Directive 6601 to require the use of encryption, or an otherwise effective tool, to properly protect personally identifiable information and other sensitive data stored on removable storage devices when used within VA." [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF].

As for a purpose of sharing, it is suggested to avoid sharing business impact information with outside organisations unless there is a clear value proposition or formal reporting requirements. When sharing information with peers and partner organisations, incident response teams should focus on exchanging remediation information [START_REF] Hadgkiss | Computer security incident handling[END_REF]. The remediation information information reported describes [START_REF]Symantec: Internal security threat report 2011 trends[END_REF] the security issues, e.g. "The position sensitivity level for the IT Specialist was inaccurately designated as moderate risk, which was inconsistent with his programmer privileges and resulted in a less extensive background investigation", (2) the security objectives violated during this process, e.g. "Position Sensitivity Level Assessments were Not Adequately Performed", and (3) the recommendations, e.g."We recommend that the Under Secretary for Health direct the Medical Centre Director to re-evaluate and correct position sensitivity levels and associated background investigations for positions at the Birmingham VAMC " [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF]. Those granular information are inter-related, however, they are scattered documented in a pure textual based report that makes it difficult for the readers to identify the relationships among them. This issue has been compounded by the lengthy security incident report, which is usually around hundred of pages [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF]. The stakeholders responsible for protecting patient data lack the time and the motivation to spend the many hours needed to read and digest existing reports. This creates significant problems within the wider scope of security management systems; it can be difficult to accurately assess the likelihood or consequences of future attacks when managers are unaware of previous incidents.

Graphical techniques can address some of these limitations. The Generic Security Template (G.S.T.) has been developed [START_REF] He | Generic security cases for information system security in healthcare systems[END_REF][START_REF] He | An empirical study on the use of the generic security template for structuring the lessons from information security incidents[END_REF] to help readers understand the lessons learned from previous security incidents. In particular, it extends the Goal Structuring Notations (GSN) [START_REF] Kelly | Arguing safety-a systematic approach to safety case management[END_REF] to provide an overview of previous data breaches. The intention is to map out the security objectives, security issues and recommendations that are embedded in the many pages of text that are used in conventional reports. More information on the GSN and the G.S.T. is provided in section III. Fig. 1 provides an excerpt from one of these diagrams. It is based on a report into the disclosure of personal information about 250,000 veterans and over 1.3 million medical providers by the US Veterans Affairs Administration (VA) [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF]. This incident report provides the case study that is used throughout this paper. The leaf nodes in this diagram are used to gather together the recommendations that were intended to avoid future incidents. The internal nodes are used to show how each of these findings supports higher level goals and sub-goals intended to ensure that systems meet an acceptable level of security, defined in terms of the US Government's Federal Information System Controls Audit Manual (FISCAM) [START_REF] Dacey | Federal Information System Controls Audit Manual (FISCAM)[END_REF]. Further information about the graphical technique is provided in [START_REF] He | Generic security cases for information system security in healthcare systems[END_REF][START_REF] He | An empirical study on the use of the generic security template for structuring the lessons from information security incidents[END_REF][START_REF] He | Improving the information security management: An industrial study in the privacy of electronic patient records[END_REF]. The use of graphical overviews is intended to make it easier to identify recommendations that can be transferred from a previous incident to prevent similar breaches from occurring in other organisations.

Previous work has shown that GSN can be used to map common lessons from data breaches in healthcare organisations in healthcare organisations in both the United States and in China [START_REF] He | Generic security cases for information system security in healthcare systems[END_REF]. Although these incidents occurred in very different contexts, the security concerns and the consequences for patient confidentiality show remarkable similarities. This previous work provided initial case studies but did not, present empirical support for the benefits of using graphical representations compared to text-based reports of security incidents. This paper, therefore, presents a controlled experiment to investigate whether graphical approaches can be used to augment conventional, text-based documents. The remainder of the paper is structured as the following, section 2 reviews the related work, section 3 briefly introduces the G.S.T., section 4 outlines the experiment design, section 5 presents the experiment procedure, section 6 prepares data to analyse the results, section 7 analyses the results, and section 8 summarises the paper.

Related Work

There is a natural reluctance to share details of previous security breachesreports may inspire new attacks or publicize vulnerabilities. However, a growing number of regulatory agencies now provide detailed reports that are intended to help avoid any recurrence of previous failures. Security management systems have also been introduced into many healthcare organisations to ensure previous security incidents inform threat and risk assessments [START_REF] Commissioner | Directive 2009/140/ec of the european parliament and of the council of 25 november 2009[END_REF]. Improving situation awareness, in particular about security breaches, help persuade end users of the importance of existing policies and procedures. There are further benefits from the wider dissemination of incident reports. Security engineers can learn important lessons about the analysis, containment, eradication, and recovery from previous attacks. The introduction has argued that existing, text-based reports can be supported through the use of graphical notations that provide an overview of many dozens of pages of detailed prose. Fig. 1 uses the Goal Structuring Notations to summarize key findings from an enquiry into a loss of confidential patient data from the US Veterans Affairs Administration [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF]. The aim is to present the security objectives in a structured and coherent manner. It is also hoped that this use of a semi-formal notation will encourage greater consistency and correctness [START_REF] Craigen | Formal methods technology transfer: Impediments and innovation[END_REF][START_REF] Hinchey | Confessions of a formal methodist[END_REF]. However, the notation introduces unfamiliar syntax and semantics. There is a danger that our use of these techniques can prevent stakeholders from understanding the arguments in security incident reports [START_REF] Finney | An empirical study of specification readability[END_REF][START_REF] Finney | Mathematical notation in formal specification: Too difficult for the masses? Software Engineering[END_REF][START_REF] Carew | An empirical investigation of the comprehensibility of requirements specifications[END_REF]. This paper, therefore, presents a controlled experiment to evaluate the utility of graphical representations for security incident reports.

The Generic Security Template

As mentioned, the G.S.T. extends the Goal Structuring Notations (GSN) [START_REF] Kelly | Arguing safety-a systematic approach to safety case management[END_REF] to provide an overview of previous security breaches. GSN is the dominant approach in the UK defence sector, increasingly being used in safety-critical industries to improve the structure, rigor, and clarity of design requirements. A particular strength is that it also links the evidence to show that particular requirements have been met. The same approach has more recently been extended to document security requirements [START_REF] He | Generic security cases for information system security in healthcare systems[END_REF][START_REF] He | An empirical study on the use of the generic security template for structuring the lessons from information security incidents[END_REF]. There are four principal notations used in the GSN, A Goal is a claim, the statements that the goal structure is designed to support. Evidence exists to support the truth of the claimed goal, which can be documented by providing a solution in GSN. Strategy is inserted between goals at two levels of abstraction, to explain how the top-level goal is addressed by the aggregation of the goals presented at the lower level. Context is used to declare supplementary information and provide adequate understanding of the context surrounding the claim (or strategy). Usually it presents concepts clarification introduced in the claim (or strategy) [START_REF] Kelly | Arguing safety-a systematic approach to safety case management[END_REF].

The G.S.T. has customised the GSN. Instead of collecting evidence to support design and development requirements, it collects lessons (i.e. security causes and recommendations) from previous security incidents. These lessons are defined to be the knowledge or understanding gained by experience [START_REF] Weber | Intelligent lessons learned systems[END_REF]. In the G.S.T., it refers to the security issues that cause a security breach, and the security recommendations intended to avoid any recurrence. The evidence of compliance with the security objectives is presented in the form of a specific security standard or guideline applied to the organisation where the security incident happened. This has reflected the granular information described in section 1. Generic, is defined as "characteristic of or relating to a class or group of things; not specific". In other words, the intention is to create a GSN diagram that conveys the lessons learned from specific previous security breaches at a level of abstraction that helps others to use them to improve the security of other systems. Fig. 2 presents the notations used in the Generic Security Template. Fig. 2 presents the notations used in the Generic Security Template. In particular, rather than using the evidence derived from validation and verification to support safety arguments. The G.S.T. uses the findings from previous data breach incidents (i.e. leaf nodes of Fig. 1) to support security arguments in terms of the compliance with the security guideline (i.e. internal nodes of Fig. 1). The other concepts remain the same between both application areas.

Experiment Design

Experiment Objective and Scope

A controlled experiment was conducted to evaluate whether the use of graphical techniques helps improve the comprehension of the lessons from previous security incident reports compared to conventional text-based approaches. The aim was not to show that graphical techniques could replace conventional reports; in contrast the focus was in the use of our extended GSN approach to provide a map or overview of complex text-based reports. Accuracy, efficiency and task load are compared quantitatively in this experiment and the following hypotheses are proposed for the comparison.

H1: Participants will be better able to identify the Lessons learned (security issues, security recommendations) in security incident report with the help of the G.S.T. than using Text-based Document alone; H2: Participants will be better able to identify the compliance with the security objectives in security incident report with the help of the G.S.T. than using Textbased Document alone; H3: The time taken to complete the designed task will be less using the G.S.T. than that using the text-based Document alone; H4: The task load will be lower using the G.S.T. than using the text-based Document alone.

Ease of use is compared qualitatively based on the feedback obtained from participants.

Experiment Variables

Dependent Variables We evaluate the usability [START_REF] Folmer | Architecting for usability: a survey[END_REF] in terms of the accuracy, efficiency, ease-of-use and task load compared to the conventional, textbased approach. Accuracy, is measured by assessing the quality of the security causes, recommendations and the compliance with the security objectives from the security incident. Efficiency, is measured by the time it takes to complete the experiment task. Ease of use, is evaluated by the feedback obtained from the post-experiment questionnaire. Task load, is measured by the application of NASA's Task Load Index to assess workload [START_REF] Hart | Development of nasa-tlx (task load index): Results of empirical and theoretical research[END_REF].

Independent Variables Generic Security Template (G.S.T.), we used the same G.S.T. across all participants. This presents findings from the US Veteran's Affairs administration 2007 Dataloss Incident [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF].Text-based approach, we developed an executive summary (reduced to four pages) and a simplified security guidelines (reduced to three pages) from the FISCAM. More details on the experiment material preparation are provided in 4.3.

Controlled Variables Participants, the participants were post-graduate and undergraduate students with different education background. Tasks, the experiment itself lasted for maximum one hour. Participants had to identify causes, recommendations and the relationships with security objectives using either a conventional text-based document or using the graphical overview plus the existing report.

Extraneous Variable Experience with GSN, is defined as an extraneous variable in this experiment. People who have experience with GSN will have an obvious advantage in comprehending the security incident with the help of the G.S.T. People who have experience with GSN were excluded from this experiment.

Experiment Materials

Security Incident Report. Security Incident Report. The technical context of the task focused on a data loss incident involving the Veterans Affairs' Administration [START_REF] Administration | Administrative investigation loss of va information va medical center birmingham[END_REF]. The original report was around 80 pages long and hence we could not use it directly within the time available for the experiment. We also felt that our more focused approach was more appropriate for an initial study that could, in turn, inform future empirical work over a longer period of time and with a larger number of participants. We, therefore, provided both groups with the executive summary from the VA report reduced to four pages. As is mentioned, the evidence of compliance with the security objectives is presented in the form of a specific security standard or guideline applied to the organisation where the security incident happened. Therefore, a simplified version of security guidelines (reduced to three pages) cited from the FISCAM that are relevant to this incident are also provided as a part of the security incident report.

The G.S.T. The G.S.T. used in this experiment is created from the above mentioned security incident report only. It is an abstraction and extraction of the desirable information and did not bring any other information that can bias the results of the experiment.

The Questionnaire. We developed separate tasks description for the two groups and a post-experiment questionnaire, to provide subjective insights into perceived workload. A slightly different version of this post-experiment questionnaire was developed for the group using the graphical overview of the security incident. They were asked to provide information about the usability of the approach by completing subjective questionnaire.

The Pilot Study

Two security experts reviewed the design of the experiment pilot studies then helped to identify issues that had not been identified during the preparation of the materials. In the first pilot study, participants had to identify security issues, recommendations and compliance with the security objectives; writing them down using freestyle text. This was to simulate how security incident reports are analysed in practice, where people normally have no tools assisting them throughout this process. The feedback from the participants showed that the task was very mentally demanding and they were not able to complete it within one hour. We corrected this problem by introducing a table that provided guidance on the security issues and recommendations. The participants are required to fill in the blanks cells in the table. For the measurement of compliance with the security objectives, we have used multi-choice questions as the measurement mainly focuses on the relationships between the security objectives and the recommendations for prevention. Two more participants conducted a pilot test of the new experiment design. They were able to finish the tasks and stated that the level of mental effort was acceptable.

Experiment Task Design

In Group A, the experiment materials included the textual incident report (reduced executive summary and reduced security guidelines from FISCAM), the graphical G.S.T. and a task description. The pilot study had confirmed the arguments presented in the opening sections of this paper; that it can be difficult for readers to identify the causes, recommendation and the compliance with the security objectives of previous security incidents from existing textual reports. We, therefore, created tasks that guided the participants' analysis:

Task 1: Identify security issues and recommendations from the security incident report with the help of the G.S.T. They had to complete missing information from a table that provided partial information about the causes and recommendations. Table 1 is an exempt of the table. Issue Category and Description are provided. The participants need to fill in the blank about the recommendation description.

Issue Category Issue description Recommendations description

Access Control Related

The IT Specialist was improperly given access to multiple data sources.

Table 1. An exempt of the security issue and recommendation table

Task 2: Answer multiple-choice questions on compliance of the security objectives. This removed the additional contextual support of the tabular format used in task one and provided a stepping stone towards the open ended analysis of security incident reports that proved problematic in the pilot studies.

In Group B, the experiment materials included the textual incident report without the G.S.T. but participants had the same task descriptions as the first group.

Experiment Procedures

Experiment Treatment

There was only one treatment in the experiment using a between groups (Group A and B) design. The empirical comparisons are between one group using a conventional text-based document and another using the graphical overview as well as the existing report.

Participants

Twenty-four subjects were assigned to either of the two experimental conditions using the textual report only or using both the textual report and the graphical overview. Group A consists of one undergraduate student and eleven postgraduate students, within which three of them have information security experience; Group B has one undergraduate student and eleven postgraduate students, within which three of them have information security experience. Each of the group have three females and nine males.

Training of the Participants

A pre-scripted familiarisation tutorial was provided before the experiment. Participants from both Group A and B attended the same tutorial session. This was to ensure that they received equal knowledge related to the handling of security incidents. The participants were introduced to the Goal Structuring Notations and G.S.T.

Experiment Execution

The experiment was conducted on a one-to-one mode to provide any support needed during the whole process including the familiarization tutorial session, the experiment session and the post-experiment questionnaire session. During the familiarization tutorial session, the participant had unlimited time to study the material and to have any question clarified. The participants were allowed to refer to the tutorial document or notes. The participants were instructed to inform the experiment conductor if they had any trouble in understanding the questions. During the post-experiment questionnaire session, an informal interview was conducted to make sure their attitudes were consistent with the answers they have provided. They are also requested to write down their subjective feedback on the G.S.T.

6 Results -Prepare the data

Scoring Scheme for the Experiment Tasks

Sample answers for the experimental tasks were agreed on by two independent security experts.

Preparation for Task 1 -Open-ended questions

For Task 1, the answers expected were qualitative. The marking was based on the description of security issues and recommendations expected from the sample answers. The answers for each task were marked by two further independent experts (Rater A and B) using an agreed scoring scheme. The participants' answers were classified into four categories, which are "Correct", "Incomplete", "Wrong" and "Blank". A correct answer completely described the recommendation to support the given issue; incomplete answers show that the participant had a partial understanding of the recommendation, but lacked comprehension of an important aspect of it. Wrong answers showed that the participant did not understand a particular recommendation. Blank, no answer was provided at all. The following paragraph provides an example from task one:

The report identifies the security concern: "The IT Specialist was improperly given access to multiple data sources". An answer is marked as, Correct, if the participant states that the recommendation associated with this issue was to "Consider the conditions under which programmer level access may be granted for research project". A correct answer completely describes the recommendation to support the given issue; Incomplete, if the answer is stated as "Ensure the access control is appropriately granted". Incomplete answers show that the participant had a partial understanding of the recommendation, but lacked comprehension of an important aspect of it; Wrong, if the answer provided is not relevant to a particular recommendation. Blank, if no answer was provided at all.

Each participant was free to use his or her own words to describe the recommendations in this part of the study. The group identifiers were removed so that Rater A and B marked the answers without knowing whether or not the participants had access to the G.S.T. diagram.

Preparation for Task 2 -Multi-choice questions

Task 2 used multi-choice questions to examine the participant's ability in understanding the compliance with the security objectives. Less subjectivity was involved in interpreting the answers. There can be more than one correct choice for each question and participants were asked to select all of the responses they believe were relevant to the questions. Below is an example.

What are the security recommendations for addressing the security objective "User Access Control"? a. Develop and implement policies describing the conditions under which programmer level access may be granted for research purposes. b. Effective procedures are implemented to determine compliance with authentication policies.

c. Attempts to log on with invalid passwords are limited. Use of easily guessed passwords (such as names or words) is prohibited.

d. None of the above

Correct answer: a, b

The sample answers were prepared by the independent security expert A.

Each answer was classified as, Correct, Correct but broad, Incomplete, Incomplete and broad, Wrong, and Blank. A correct answer contained and only contained all the acceptable choices (e.g. a, b); Correct but broad contained all the acceptable choices, but also incorrect choices (e.g. a, b, c); Incomplete answers contained only some of the acceptable choices but not all (e.g. a). Incomplete and broad answers contained some of the acceptable choices and also other choices. (e.g. a, c); Wrong answers contained none of the acceptable choices (e.g. c).There was only one blank answer out of 144 responses; therefore we ignore this in the subsequent analysis.

7 Results -Analysis Out of a total number of 168 answers to the seven questions by 24 participants, three were left blank with one in Group A and two in Group B. During the debrief, the participants stated that, for the blank response, they could understand the questions but could not find the answer in the given materials. We ignore these blank answers in the subsequent analysis. Inter-rater reliability was checked for each question in Task 1, recall that these open ended questions assessed by two independent raters. The results are listed in Table 2. Questions 1, 2 have achieved "almost perfect agreement"; Questions 3, 4, 5, and 6 have achieved "substantial agreement"; Question 7 has achieved "Fair agreement" [START_REF] Landis | The measurement of observer agreement for categorical data[END_REF]. A third independent security expert was invited to decide whether he agreed with Rater A or Rater B. The third security expert came to a 65.3% agreement with the Rater A and a 34.7% agreement with Rater B. Their interpretation was definitive for our analysis; in other words where there was disagreement between the first two assessments, the third rater decided which score was correct.

Inter

Comparing the performance of Task 1

Since the results are categorical data, we use cross-tabulation analysis to analyse the results. As is shown in Table 3, the results from the Cross-tabulation analysis (Table 3) show that 62.7% of the responses from Group A were correct, which is 17.6% higher than Group B. This might seem a relatively low level of accuracy. However, it is important to recall that our marking scheme was careful to distinguish between complete, perfect responses and partially correct or incomplete answers. The total percentage of Incomplete and Correct answer is 81.9% in Group A, which is 13.8% higher than Group B. As is shown in Table 4, the Chi-Square Test (P = 0.048 < 0.05) shows that these results are statistically significant. Therefore, hypothesis H1 "Participants will be better able to identify the recommendations and causes in security reports with the help of a graphical method than using text alone" is supported.

This result again shows that Group A has demonstrated a slightly higher level of comprehension than Group B. Therefore, hypothesis H1 "Participants will be better able to identify the recommendations and causes in security reports with the help of a graphical method than using text alone"is supported. The results from the cross-tabulation analysis show that the participants from Group A achieved a 33.3% accuracy rate, which is 9.7% higher than Group B. The total percentage of Correct, Broad, Incomplete, and Incomplete but broad answer is 87.5%, which is 18.1% higher than Group B. As is shown in Table 5, the Chi-Square Test (P = 0.038 < 0.05) shows that these results are statistically significant. This multi-choice results were not due to coincidence. Therefore, hypothesis H2 "H2: Participants will be better able to identify the compliance with the security objectives in security incident report with the help of the G.S.T. than using Text-based Document alone" is supported in Task 2. The mean total time used by Group A was almost equal that in Group B; 47.3 versus 47.8 minutes. The total time taken across all tasks is not statistically significant (P = 0.932 > 0.05). Therefore, we can accept the null hypothesis that "the mean time taken to complete our experimental tasks using a textual security incident report and a textual report with a graphical overview are not significantly different."Hypothesis H3 is not supported. One interpretation of these results is that significant time is required to understand security incidents, irrespective of whether they are presented in graphical or textual format. However, this would require further empirical support to determine whether or not other graphical notations might lead to significant differences in the time taken to understand security incident reports. It is also important for further work to consider the learning effects that might be expected through repeated use of the graphical maps.

The Results for Task Load Index (TLX)

We used NASA's Task Load Index [START_REF] Hart | Development of nasa-tlx (task load index): Results of empirical and theoretical research[END_REF] to assess workload using a post-evaluation questionnaire. The t-test results show a significant difference (P = 0.047 < 0.05) in the first dimension of the task load index regarding "how mentally demanding was the whole task". With a mean value of task load, 12.75 versus 15.50, participants expressed a lower subjective level of workload in terms of "mentally demand"when using the G.S.T. The results for the other four dimensions of the Task Load Index are not significantly different. However, a more sustained analysis is required to replicate these findings across a wider range of workload measures and with a larger sample of potential users.

Subjective Feedback

In Group A, approximately half of the participants expressed some difficulty in understanding the text based Security Incident Report. Half of the participants reported that they have no difficulty in completing task 1 of Group A: identifying security elements from the security incident report with the help of the G.S.T. Group B reported a slightly higher level of understanding of the Security Incident Report. However, less than half of the participants suggested that they have no difficulty in completing task 1 of Group B: identifying lessons learned from the security incident report, and the rate is much lower than that of Group A. These subjective findings are consistent with the quantitative results in section 6.3. The participants' answers to the open questions regarding the overall experience of using the graphical overviews suggested that a longer training session might have helped them to better prepare for the tasks. Several participants mentioned that they had experienced learning effects; their confidence in answering the questions increased as they worked their way through the questions. This finding from Group A reveals generally positive feedback for the G.S.T. Group B did not use the G.S.T. during the experiment. They were asked to review the G.S.T. after the experiment and provide the feedback by completing Questionnaire Section 6 designed for Group B. Almost all of them suggested that they would have no difficulty in understanding the G.S.T. and agreed that the G.S.T. can help them better comprehend existing security incident reports. Two thirds of the participants reported their willingness to use the G.S.T. if they are requested to do a similar task in future. "It will help to understand terminologies security elements easily, less confusing, very structured and don't have to waste time, most importantly very easy to understand with less information". In summary, the participants overall experience with the G.S.T. is positive, however, questions remain about the ability of participants to apply the lessons from the report within their own organisation rather than answering directed questions about the contents of a security report.

Conclusions and Future Work

There have been numerous empirical studies to evaluate the utility and usability of graphical notations, including Entity-Relationship diagrams [START_REF] Shoval | Entity-relationship and object-oriented data modeling-an experimental comparison of design quality[END_REF], UML [START_REF] Glezer | Quality and comprehension of uml interaction diagrams-an experimental comparison[END_REF] [23] etc. However, as far as we are aware, there have been no previous studies to assess the strengths and weaknesses of graphical notations to help transfer the lessons learned from previous security incidents. These studies are urgently needed as both the Obama administration and the European Commission have recently published proposals to support the mandatory reporting of security incidents across national critical infrastructures, including healthcare. In this paper, we have presented the results derived from an initial study into the use of Goal Structuring Notation (GSN) to represent and reason about the recommendations made in a report of a data confidentiality breach involving the US Veterans' Affairs Administration. We were able to show significant benefits from the use of a graphical technique in answering a number of comprehension questions when compared to the more conventional use of text-based incident reports. However, we could not demonstrate any significant benefits in terms of the time taken to complete our experimental tasks, nor could we demonstrate significant benefits when participants were asked to identify the compliance with the security objectives provided by multiple-choice questions.

It is important to stress that this was a preliminary study. The sample size was relatively small due to practical reasons: (1) the approach is new and people have little experience with security incident analysis; (2) the tasks were mentally demanding; (3) participation was voluntary. However, our work did yield important insights into the difficulties that engineers face when trying to understand the implications that previous security incident reports have for their own organisations.

Fig. 1 .

 1 Fig. 1. Generic Security Template -VA dataloss 2007

Fig. 2 .

 2 Fig. 2. Customised GSN Notations

7. 1

 1 Results for Accuracy (Task 1)

-rater reliability check for each question

	Question No.	1	2	3	4	5	6	7
	Kappa Value	0.85	0.80	0.75	0.57	0.72	0.78	0.50

Table 2 .

 2 Inter-rater reliability for each question (Rater A and B)

Table 3 .

 3 The performance of Task 1 using Cross-tabulation

	Task	Total

Table 4 .

 4 Chi-Square Tests performance of Task 1 using Cross-tabulation 7.3 The Results for Accuracy (Task 2)

Table 5 .

 5 Chi-Square Tests performance of Task 2 using Cross-tabulation 7.4 The Results for Efficiency (Time)

					Task
			Wrong	Incomplete	Correct	Total
	Group A	Count	14	15		54	83
		% within Group	16.9%	18.1%	65.1%	100.0%
	Group B	Count	28	17		37	82
		% within Group	34.1%	20.7%	45.1%	100.0%
	Total	Count	42	32		91	165
		% within Group	25.5%	19.4%	55.2%	100.0%
						Task
			Wrong	Incomplete	Incomplete	Broad	Correct	Total
					and broad
	Group A	Count	9	11	19	9		24	83
		% within Group	12.5%	15.3%	26.4%	12.5%	33.3%	100.0%
	Group B	Count	22	4		18	11	17	82
		% within Group	30.6%	5.6%	25.0%	15.3%	23.6%	100.0%
	Total	Count	31	15	37	20	41	165
		% within Group	21.5%	10.4%	25.7%	13.9%	28.5%	100.0%
				Chi-Square Tests
			Value	df	Asymp. Sig. (2-sided)
	Pearson Chi-Square	10.140a	4		.038
	Likelihood Ratio		10.449	4		.034
	Linear-by-Linear Association	2.995	1		.084
	N of Valid Cases		144
			Symmetric Measures
			Value	Asymp.Std. Error a	Approx. Tb	Approx. Sig.
	Measure of Agreement Kappa	.497		.154	3.251		.001
	N of Valid Cases		24

Acknowledgment

The first author would like to thank the China Scholarship Council (CSC) for funding this research work.


Alessandro Aldini
email: alessandro.aldini@uniurb.it

A Calculus for Trust and Reputation Systems

Trust and reputation models provide soft-security mechanisms that can be used to induce cooperative behaviors in user-centric communities in which user-generated services and resources are shared. The effectiveness of such models depends on several, orthogonal aspects that make their analysis a challenging issue. This paper aims to provide support to the design of trust and reputation infrastructures and to verify their adequacy in the setting of software architectures and computer networks underlying online communities. This is done by proposing a formal framework encompassing a calculus of concurrent systems, a temporal logic for trust, and model checking techniques.

Introduction

Cooperation is a key factor for the success of service-and user-centric networks in which user-generated contents are exchanged, remote resources are shared, and services provided by third parties are executed online. Trust and reputation systems provide extrinsic motivations to favor cooperation in spite of selfishness, malicious behaviors, and mistrust towards unknown users. The metrics provided by these systems help to estimate quantitatively the subjective reliance on the ability, integrity, honesty and disposition of each user, to be shared within the community with the aim of making explicit a collective notion of reputation. Even more important, reputation is defined not only to give a perception of the public trustworthiness of users, but also to provide enabling conditions for participating actively in the community by exchanging services and resources.

The design and implementation of trust and reputation systems is not an easy task as it depends on several, orthogonal aspects. Solutions can be centralized or distributed, can rely (or not) on the presence of a trusted third party, can use first-hand or second-hand reputation systems using (non-)linear adjustment mechanisms, can involve explicit (based, e.g., on voting) or implicit evaluation means, and so on [START_REF] Jøsang | Foundations of Security Analysis and Design IV (FOSAD'07)[END_REF]. As a consequence, the analysis of the effectiveness of these systems against the typical obstacles to cooperation (lack of motivation, selfishness, free-riding, . . . ) and the variety of attacks (slandering, self-promoting, sybil, . . . ) is a challenging issue.

In this paper, we propose a framework for:

the formal modeling of the behavior of cooperative, concurrent, and distributed systems;

the formal specification of trust and reputation infrastructures governing the interactions in these systems; the formal verification of the effectiveness of the trust policies adopted by these infrastructures to stimulate cooperation and to contrast attacks.

These objectives are achieved by means of a process algebraic approach to software architecture design, in which functional modeling (through typical process algebraic operators) and specification of the trust model are defined separately at the syntactic level and joined automatically at the semantic level. This separation of concerns facilitates all the design issues and the execution of sensitivity analysis aimed at evaluating the effects of the chosen system architecture and trust model. The formal specification of trust-based properties relies on a temporal logic for trust that extends classical state-based and action-based logics, while the verification of such properties is supported by model checking techniques.

In the rest of the paper, we first introduce a real-world case study, which accompanies the presentation of the formal framework as a running example through which we show how to apply our approach in practice. Afterwards, we present the syntax for a calculus of concurrent processes and the syntax for a specification language of trust systems. We then define a unifying formal semantics, which subsumes the definition of specific labeled state-transition systems, and the temporal logic for specifying trust properties that can be model checked through standard techniques. Conclusions about related work and future directions terminate the paper.

Running Example

As a real-world example, we consider an incentive-based cooperation model for wireless and mobile user-centric environments recently proposed [START_REF] Bogliolo | Virtual Currency and Reputation-Based Cooperation Incentives in User-Centric Networks[END_REF]. Basically, cooperative networks involve users providing services, called requestees, and recipients of such services, called requesters. For the sake of simplicity, we assume that each user behaves either as requester or as requestee. The cooperation model is based on soft-security mechanisms (like trust management and virtual currency) and a process entailing four phases: (i) the requester looks for a service in the community and then sends a request to the chosen requestee; (ii) the two parties negotiate parameters and cost of the transaction; (iii) if an agreement is reached, the requestee provides the negotiated service and the requester pays for it; (iv) both parties evaluate the quality of experience and provide feedback. In each phase, trust is used to govern choices and to provide incentives for both parties, e.g., by making offered quality of service and related cost directly dependent on trust. The objective consists of inducing a prosocial attitude to collaboration while isolating selfish and cheating behaviors.

In the following, we abstract away from the details of the specific incentive strategies and we concentrate on showing how to employ our approach in order to model a scenario like the one surveyed above, specify the underlying trust and reputation models, and perform model checking based sensitivity analysis aiming at demonstrating the influence of each policy and configuration parameter chosen by the involved parties.

In this section we show how to define separately functional behavior of the system and trust infrastructure. In both cases, we present formal syntax, semantics, and examples related to our running case study.

By following principles inspired by architectural description languages [START_REF] Aldini | A Process Algebraic Approach to Software Architecture Design[END_REF], we distinguish between process behaviors, which describe behavioral patterns, and process instances, which represent specific entities exhibiting a certain behavioral pattern, as well as we separate the definition of individual entities from the specification of their parallel composition and communication interfaces. This separation of concerns is applied also to distinguish the description of a system of interacting entities from the specification of the reputation infrastructure governing any interaction based on trust. The objective is an improvement of usability concerning the modeling issues of the different aspects that come into play in the specification of trust-based distributed systems.

Modeling Individual Processes

We start by introducing a calculus for the specification of individual process terms, which represent process behaviors modeling behavioral patterns. We denote with Name the set of visible action names, ranged over by a, b, . . .. Moreover, we assume a special name τ to denote invisible, internal actions.

The set of process terms of our calculus is generated through the following syntax:

P ::= 0 | a . P | τ . P | P + Q | a.P ∓ b.Q | B
where:

-0 represents the inactive, terminated process term.

a . P (resp., τ . P ) denotes the process term that executes a (resp., τ ) followed by the behavior of P . -P + Q represents a nondeterministic choice between process terms P and Q.

a.P ∓ b.Q, which is called trusted choice operator, denotes an external, guarded choice based on trust. -B represents a process constant equipped with a defining equation of the form B def = P , which establishes that process constant B behaves as process term P , thus enabling the possibility of defining recursive behaviors.

In the following, we restrict ourselves to consider guarded process terms, i.e., all of the (finite) occurrences of process constants are immediately preceded by the action prefix operator. Before detailing the interpretation of these operators, we introduce the underlying semantic model, which is based on classical labeled transition systems. Definition 1. A labeled transition system (lts) is a tuple (Q, q 0 , L, R) where Q is a finite set of states, of which q 0 represents the initial one, L is a finite set of labels, and R ⊆ Q × L × Q is a finitely-branching transition relation, such that (p, l, q) ∈ R is denoted by p l --→ q.

Given Act = {τ } ∪ Name ∪ {a -| a ∈ Name}, which is ranged over by α, . . ., the behavior of a process term P is defined by the smallest lts [[P ]] such that the states in Q represent process terms (with P being the initial state q 0 ), the labels in L are given by actions in the set Act, and the transitions in R are obtained through the application of the following operational semantic rules:

prefix a . P a --→ P τ . P τ --→ P choice P α --→ P P + Q α --→ P Q α --→ Q P + Q α --→ Q trusted choice a.P ∓ b.Q a --→ P a.P ∓ b.Q b - --→ Q recursion B def = P P α --→ P B α --→ P
The rules for prefix, nondeterministic choice, and recursion are standard, while the trusted choice operator establishes that a.P ∓ b.Q executes either a followed by P or (a decorated version of) b followed by Q. The intuition is that this operator is used to communicate one of two possible actions to another process and that the choice will be guided by the trust towards such a process: if trust is beyond a certain threshold, then the offered action is a, otherwise it is b. The isolated semantics of this operator offers both actions, as the identity of the interacting process is still unknown, but it uses a decoration to distinguish which action is to be considered in the absence of sufficient trust.

Example 1. With respect to our running example, let us model the behavior of a generic (potentially dishonest) requester possibly interacting with n requestees and the behavior of a generic requestee possibly interacting with m requesters.

The process term describing the requester behavioral pattern is: A process instance, called entity, is an element exhibiting the behavior associated to a process term. The kernel [[I]] of the semantics of an entity I belonging to the behavioral pattern defined by process term P is given by the behavior of P , in which every action α is renamed to I.α [START_REF] Aldini | A Process Algebraic Approach to Software Architecture Design[END_REF]. With abuse of terminology, we say that I is of type P , and we write I.B to specify that the behavior of I in the current state is given by the process term associated to B.

Requester def = send
Example 2. In our running example, we consider a system with a single requester, modeled by the entity Req A of type Requester , and three requestees, which are represented by the entities Req 1 , Req 2 , and Req 3 , each one of type Requestee.

Modeling Trust and Reputation

The execution of the interactions in which every entity in a system is involved depends strictly on the trust infrastructure regulating the communications within the community. Hence, before introducing the semantics for interaction, we first define formally such an infrastructure with respect to a set S of individual entities, by assuming that each entity name is unique to avoid ambiguity.

Let IName = {I.a | I ∈ S ∧ a ∈ Name} be the set of interacting action names. Moreover, T represents the domain of trust values. Even if in principle we may adopt any trust domain by adequately defining the semantics of the structures manipulating trust values, for the sake of presentation in the following we assume it to be a totally ordered set, the maximum (resp., minimum) value of which is denoted by (resp., ⊥).

A trust system is a tuple consisting of a set S of interacting processes and of the following structures: -Trust function tf : S × S → T, such that tf (I, J) computes the trust of I towards J according to a trust formula taking into account direct trust (deriving from the trust table) and reputation (deriving from the recommendation table ).

-Trust table tt : S × S → T,
We implicitly assume that the trust structures are parameterized with respect to a given type of service, and that several, mutual independent structures are needed if we intend to model a system offering different types of services, each one requiring separate trust information. In this case, every action must be parameterized as well with respect to the service type, in order to guide each interaction among entities according to the related trust information.

As far as the trust function tf is concerned, here we do not define it as its specification strictly depends on the chosen trust model and, as we will see, it does not affect the definition of the semantics for interacting processes. Function tf may be based on several different methods [START_REF] Kamvar | The Eigentrust Algorithm for Reputation Management in P2P Networks[END_REF][START_REF] Zhou | PowerTrust: A Robust and Scalable Reputation System for Trusted Peer-to-Peer Computing[END_REF][START_REF] Zhang | Balancing Trust and Incentive in Peer-to-Peer Collaborative Systems[END_REF], an example of which will be given with respect to our case study. We can argue similarly in the case of the specific relation existing between trust table and recommendation table and, in particular, the way in which an entity provides feedback to other entities on the basis of personal experience. However, some aspects of such a relation (that change depending whether the reputation system is centralized or distributed) deserve discussion here.

In a centralized scenario, we can envision a trusted third party collecting trust information from all the entities. Such a collection contributes to form the reputation of each entity as perceived by the community. Hence, it is reasonable to assume that every entity requiring a recommendation has access to such information in the same way and obtains the same feedback. From a semantics viewpoint, this scenario is captured by formalizing the relation between trust table and recommendation table.

For instance, in a very simple scenario, the recommendation provided by I about J is exactly the trust of I towards J, under the assumption that I had some direct experience with J (otherwise the suggested value would be simply the dispositional trust of I). Let ct : S×S → {0, 1} be the contact table, such that ct[I; J] = 1 if and only if entities I and J interacted with each other (initially, ct[I; J] = 0 for each pair of entities in the set S). Then, the relation between trust table and recommendation table is described by the following equation:

rt[I; J] = tt[I; J] if ct[I; J] = 1 δ otherwise (1)
thus assuming that all the entities recommend exactly the trust values resulting from their own experience, if any. Notice that this would not be the case in the presence, e.g., of entities providing inaccurate feedback or attackers cheating deliberately other entities. In order to model such a case, it is sufficient to alter some rows (or specific entries) of the recommendation table with respect to the trust table.

In a distributed scenario, the absence of a centralized trusted third party has two important effects. Firstly, different entities may have access to different information if they are in contact with different neighbors. Secondly, an entity may provide, for the same recommendation, different values to different entities. These situations are managed by adding a dimension to the recommendation table, such that each recommendation is specified by the identities of the recommender entity, the recommended entity, and the entity receiving the recommendation. Formally, if ct[I; J] = ct[I; K] = 1 then rt[I; J; K] denotes the trust value recommended by I about J to K. In this case all the formulas depending on the recommendation table are changed accordingly.

Example 3. In our running example, let trust be a discrete metric such that T = [0..10]. Initially, the trust table is as follows:

Req A Req 1 Req 2 Req 3 Req A 8 8 8 Req 1 2 2 2 Req 2 3 3 3 Req 3 5 5 5
The recommendation table is calculated by means of Equation 1(notice that we are not considering self-promoting behaviors, which, however, could be modeled). Even if we assume a distributed scenario, requester and requestees are connected without any restriction and can communicate with each other. The trust threshold function establishes that the requester issues requests without any reputation constraint, tth(Req A ) = 0, and that for each requestee the service trust threshold is equal to requestee's dispositional trust: tth(Req 1 ) = 2, tth(Req 2 ) = 3, and tth(Req 3 ) = 5.

The trust variation function establishes that the requester increases (resp., decreases) by one unit the trust towards any requestee accepting (resp., refusing) a request, namely tv (Req A .rec accept i) = 1 and tv (Req A .rec refuse i) = -1 for 1 ≤ i ≤ 3. Each requestee increases trust towards the requester in case of paid service, tv (Req i .rec pay 1) = 1 for 1 ≤ i ≤ 3. The first two requestees decrease trust by the same amount in case of unpaid service, tv (Req i .not rec pay 1) = -1 for 1 ≤ i ≤ 2, while the third one is more cautious and applies the maximum penalty, tv (Req 3 .not rec pay 1) = -10. All the other actions do not imply any trust variation.

Finally, the trust formula is abstracted as follows. Let:

Rec I,J = S\{{I, J} ∪ {K | rt[K; J] = δ}}
be the set of entities from which I receives recommendations about J. Then:

tf (I, J) = tt[I; J] if Rec I,J = ∅ ρ I • tt[I; J] + (1 -ρ I ) • K∈Rec I,J rt[K;J] |Rec I,J |
otherwise where ρ I represents the risk factor for I, i.e., how much of its trust towards other entities depends on previous direct experience. The factor that is multiplied by 1 -ρ I represents the average trust towards J resulting from recommendations provided by third entities. For the three requestees, in the following we assume that the risk factor is equal to 0.5, 0.8, and 0.8, respectively.

In general, notice that the most risky profile is adopted by the first requestee, while the third requestee is characterized by the most cautious behavior [START_REF] Aldini | Formal Approach to Design and Automatic Verification of Cooperation-Based Networks[END_REF].

Modeling Interacting Processes

The semantics of interacting entities arises from the parallel composition of a set S of individual entities following the communication rules established by a synchronization set SS , which is a set of names of the form I.a to J.b. In particular, I.a to J.b denotes a synchronization between I and J in which I offers action a and J responds with action b. In other words, I.a is the output part of the communication, J.b represents the input counterpart, and I.a to J.b is the name of the synchronized action.

Example 4. In our running example, the synchronization set for the group of entities {Req A , Req 1 , Req 2 , Req 3 } includes the actions: The system topology resulting from such a synchronization set reveals that the requester may interact with every requestee, while communications among requestees do not occur, except for the potential exchange of recommendations. Notice that such an exchange is modeled implicitly through the definition of the recommendation policy. According to the trust infrastructure described in the previous section, the system topology has the following effect on the calculation of reputation. Each requestee receives recommendations from any other requestee if such a requestee has interacted with the requester, while the requester does not receive recommendations, meaning that tf (Req A , Req i ) = tt[Req A ; Req i ] for 1 ≤ i ≤ 3 independently of the risk factor chosen by Req A .

Req A .
The interacting semantics of S is given by the parallel composition of the semantics [[I]] of all the entities I ∈ S. In the semantic rules for parallel composition, let P, P , Q, Q , . . . denote process terms representing the local behavior [[I]] of any entity I ∈ S. Moreover, let P be a vector of local behaviors with as many elements as the number of entities in S, each one expressing the current local behavior of the related entity. Then, P[P /P ] denotes the substitution of P with P in P. The semantic rule for internal actions is as follows:

P ∈ P P I.τ --→ P P I.τ

--→ P[P /P ]

The rule establishes that every entity executes its internal actions independently from each other. Then, based on the trust information, interactions among entities occur (or do not occur) and their execution provides feedback. In order to emphasize the separation of concerns between trust modeling and behavior modeling, the rule premises concerned with the trust structures are specified syntactically as external side conditions. Hence, the semantic rules expressing interactions are: where function update formalizes the effect of the interaction upon the trust between the involved parties. For instance, if we assume T to be a finite set of integers and tv (I.a) to denote the trust gain/loss, then we have:

update(v, k) = max (⊥, v + k) if k < 0 min( , v + k) if k > 0
Intuitively, the first rule states that if entities I and J enable, respectively, the interacting actions I.a and J.b, the communication guided by I is allowed, i.e., I.a to J.b ∈ SS , and J is trusted enough by I, i.e., tf (I, J) ≥ tth(I), then the interaction is executed and both I and J update their mutual trust accordingly.

The second rule behaves essentially the same, except that it models the case in which the communication from I to J occurs if I does not trust J enough, see action I.a -and the premise tf (I, J) < tth(I), in compliance with the use of the trusted choice operator. Notice that, in order to consider the case in which the contact table is necessary for the trust calculation, the update ct[I; J] = 1 must be added to the premises to keep track of the interaction. The separation of concerns -between functional behavior modeling and trust representation -is realized at the syntax level and favors independent reasoning and control. All the information and policies concerning trust are not involved syntactically in the specification of the process terms modeling the functional behavior of systems. Instead, they are described in a separate infrastructure, thus facilitating modeling and then sensitivity analysis. Functional behavior and trust management are combined at the semantics level in a fully automatic way governed by the operational semantic rules.

As far as the resulting semantic model is concerned, if trust has a finite value domain, then a concrete treatment of semantics is applied, meaning that the actual instantiations of the trust parameters become part of the formal semantics by contributing to label the states of the labeled transition system expressing the system behavior. Such a condition is achieved easily whenever trust is a finite, discrete metric, as usual in several trust-based systems [START_REF] Jøsang | Foundations of Security Analysis and Design IV (FOSAD'07)[END_REF]. In order to define the formal semantics of a system of interacting entities, we need to extend the notion of lts in order to take into account in each state the trust information affecting the application of the semantic rules. In particular, it is worth noticing that the variables of the trust infrastructure needed to determine the enabled transitions are represented by the entries of the trust and recommendation tables. In the following, we limit ourselves to consider the case of the trust table, as the extension including both tables is straightforward. Definition 2. Given a domain V of trust variables and a domain T of trust values, a trust labeled transition system (tlts) is a tuple (Q, q 0 , L, R, T, P ) where (Q, q 0 , L, R) is a lts, T is a finite set of trust predicates of the form v = k, with v ∈ V and k ∈ T, and P : Q → 2 T is a labeling function that associates a subset of T to each state of the tlts.

Hence, the semantics of a trust system made of a set {I 1 , . . . , I n } of entities obeying the synchronization set SS and the trust table tt is the smallest tlts such that the following conditions hold. Firstly, each state in Q represents a n-length vector of process terms modeling the local behavior of each entity I j , 1 ≤ j ≤ n; the initial state q 0 is associated to the vector modeling the initial local state of each entity; the trust predicates in T denote all the possible assignments in the trust table tt and the labeling function P associates a configuration of such a table to each state, by assuming that the initial state of the tlts is labeled by the initialization of tt according to the given trust infrastructure. Secondly, the transitions in R are obtained through the application of the semantic rules for parallel composition and, therefore, the set of labels L is given by the set IAct, ranged over by i, containing internal actions of the form I j .τ and interactions in SS . Therefore, a transition (p, i, q) ∈ R determines, depending on the global state p and the action i, both the vector of local states and the set of trust predicates labeling q.

Example 5. The initial state of the tlts related to our running example is associated to the vector of process terms:

[Req A .Requester , Req 1 .Requestee, Req 2 .Requestee, Req 3 .Requestee]
and is labeled with the trust predicates given by the trust table depicted in Example 3. The transitions departing from this state are three, labeled with Req A .send req i to Req i .rec req 1, 1 ≤ i ≤ 3, respectively.

Model Checking Trust Properties

The formal semantics of a trust system of interacting processes is based on tlts, which is an instance of doubly labeled transition systems [START_REF] Beek | An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications[END_REF], and of Kripke transition systems [START_REF] Chaki | State/Event-Based Software Model Checking[END_REF]. Hence, it is possible to employ temporal logics for such systems in order to define a trust logic for specifying both conditions based on the actions labeling the transitions and requirements based on the trust information labeling the states. We call such a language trust temporal logic (TTL). In particular, TTL embodies features of the classical branching-time state-based Computation Tree Logic [START_REF] Clarke | Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications[END_REF] and of its action-based variant ACTL [START_REF] De Nicola | Actions versus State based Logics for Transition Systems[END_REF].

TTL includes the definition of state formulas, which are applied to states of a tlts, and path formulas, which are applied to sequences of transitions of a tlts. The syntax of TTL is defined as follows:

Φ ::= true | i | v ≥ k | Φ ∧ Φ | ¬Φ | Aπ | Eπ π ::= Φ A1 U Φ | Φ A1 U A2 Φ
where v = tt[I; J], with I and J entity names, k ∈ T, i ∈ IAct, and A 1 , A 2 ⊆ IAct. Inspired by other logics merging action/state-based predicates [START_REF] Aldini | Performability Measure Specification: Combining CSRL and MSL[END_REF], atomic propositions are either actions or trust predicates of the form v ≥ k, where variable v denotes any entry of the trust table and k belongs to the trust domain. State formulas are ranged over by Φ. Intuitively, a state satisfies the atomic proposition i if it enables a transition labeled with i, while it satisfies the atomic proposition v ≥ k if it is labeled with a trust predicate that assigns to v a value greater than (or equal to) k. Composite state formulas are obtained through the classical connectives. The operators A and E denote the universal and existential path quantifiers. A state satisfies Aπ (resp., Eπ) if every path (resp., at least one path) departing from such a state satisfies the path formula π. Path formulas are ranged over by π, while U is the indexed until operator. Intuitively, a path satisfies the until formula Φ A1 U Φ if the path visits a state satisfying Φ , and visits states satisfying Φ while performing only actions in A 1 until that point. Similarly, the until formula Φ A1 U A2 Φ is satisfied by a path if the path visits a state satisfying Φ after performing an action in A 2 , and visits states satisfying Φ while performing only actions in A 1 until that point. We observe that a path satisfying Φ A1 U A2 Φ must include a transition to a state satisfying Φ , while this is not required for Φ A1 U Φ if the initial state of the path satisfies Φ .

Similarly as argued in the previous section, if the states of the tlts include reputation-based information deriving from the recommendation table, we can enrich TTL with reputation-based state predicates. Now, let us define formally some notion about paths with respect to a tlts (Q, q 0 , L, R, T, P ). A path σ is a (possibly infinite) sequence of transitions of the form:

p 0 i0 --→ p 1 . . . p j-1 ij-1 --→ p j . . . where p j-1 ij-1 --→ p j ∈ R for each j > 0.
Every p j in the path is denoted by σ(j). Moreover, let p j A --→ p j+1 if and only if i j ∈ A ⊆ L. We denote with Path(q) the set of paths starting in state q ∈ Q. Then, the formal semantics of TTL is as shown in Table 1.

q |= true holds always q |= v ≥ k iff (v = k ) ∈ P (q) ∧ k ≥ k q |= i iff ∃p : q i --→ p ∈ R q |= Φ ∧ Φ iff q |= Φ and q |= Φ q |= ¬Φ iff q |= Φ q |= Aπ iff ∀σ ∈ Path(q) : σ |= π q |= Eπ iff ∃σ ∈ Path(q) : σ |= π σ |= Φ A 1 U Φ iff ∃k ≥ 0 : σ(k) |= Φ ∧ (for all 0 ≤ i < k : σ(i) |= Φ ∧ σ(i) A 1 --→ σ(i + 1)) σ |= Φ A 1 UA 2 Φ iff ∃k > 0 : σ(k) |= Φ ∧ (for all 0 ≤ i < k -1 : σ(i) |= Φ ∧ σ(i) A 1 --→ σ(i + 1)) ∧ σ(k -1) |= Φ ∧ σ(k -1) A 2 --→ σ(k)
Table 1. Semantics of TTL TTL can be mapped to the logic UCTL [START_REF] Beek | An Action/State-Based Model-Checking Approach for the Analysis of Communication Protocols for Service-Oriented Applications[END_REF], for which an efficient on-thefly model checking algorithm is implemented. The unique non-trivial difference between the two logics is that TTL allows for action-based atomic propositions, while UCTL does not. The atomic proposition i of TTL can be represented through the UCTL until operator as follows. Denoted with false the formula ¬true, then i is expressed by the formula E(false ∅ U {i} true), which establishes that from the current state a transition labeled with i is enabled that leads to a state satisfying the atomic formula true, i.e., given q the current state, it holds that ∃p : q i --→ p ∈ R. Finally, we provide two flavors of classical operators like next (X), eventually (F ), and always (G), depending on the kind of until operator used. To this end, we introduce the following notations:

XΦ = false ∅ U IAct Φ X A1 Φ = false ∅ U A1 Φ EF Φ = E(true IAct U Φ) EF A1 Φ = E(true IAct U A1 Φ) AF Φ = A(true IAct U Φ) AF A1 Φ = A(true IAct U A1 Φ) EGΦ = ¬AF ¬Φ EG A1 = ¬AF IAct-A1 true AGΦ = ¬EF ¬Φ AG A1 = ¬EF IAct-A1 true
For instance, EGΦ holds in p if there exists a path in Path(p) every state of which (including p) satisfies Φ, while EG A1 holds in p if there exists a path in Path(p) every transition of which is labeled with an action in A 1 .

Example 6. With respect to our running example, we focus on the comparison between the two limiting profiles, i.e., risky and cautious, which characterize the behavior of the requestees. After adequate translation of the model, the following properties have been recast and checked both in PRISM [START_REF] Kwiatkowska | PRISM 4.0: Verification of Probabilistic Real-time Systems[END_REF] and in NuSMV [START_REF] Cimatti | NuSMV 2: An OpenSource Tool for Symbolic Model Checking[END_REF].

The first parameter under analysis is the risk factor and the related impact upon the capability of being influenced by recommendations. To this aim, we formulate the following condition to check. Can the risky requestee accept a request without sufficient direct trust towards the requester? The related property is stated formally as follows:

EF (tt[Req 1 ; Req A ] < 2 ∧ Req 1 .send accept 1 to Req A .rec accept 1)
where the state predicate tt[Req 1 ; Req A ] < 2 describes the trust condition and the action predicate Req 1 .send accept 1 to Req A .rec accept 1 represents the behavior to observe, while the formula schema expresses the eventuality of reaching a state satisfying both predicates. The property is satisfied, because by virtue of the assumption ρ = 0.5, positive recommendations provided to the risky requestee can balance (and overcome the effect of) negative direct experiences. The same property can be recast in the case of the cautious requestee: EF (tt[Req 3 ; Req A ] < 5 ∧ Req 3 .send accept 1 to Req A .rec accept 3) which is not satisfied, thus confirming the prudent behavior of this requestee.

An interesting analysis concerns the consequences of a malicious behavior of the requester. The following property: AG( Req A .not pay 3 to Req 3 .not rec pay 1 → AG(¬Req 3 .send accept 1 to Req A .rec accept 3))

is satisfied, thus establishing that after experiencing a cheating behavior of the requester (action Req A .not pay 3 to Req 3 .not rec pay 1) the cautious requestee does not trust the requester anymore (in every future state it holds that the action Req 3 .send accept 1 to Req A .rec accept 3 cannot be enabled). By replacing the cautious requestee with the risky requestee, the corresponding property is violated. Actually, not very surprisingly, even the following property is satisfied:

EF (EG A1 )
where A 1 is the set of actions: This means that a certain point can be reached starting from which the requester can obtain services from the risky requestee infinitely often without paying for any of them. This situation is an immediate consequence of the first property, which demonstrates that the direct mistrust of the risky requestee towards the requester is not sufficient to exclude the cheating behavior. On the other hand, let us now consider a completely honest requester. This variant can be obtained either by eliminating from requester's process terms any action not pay i or, even better, by removing the related actions from the synchronization set SS . In this scenario, we verify whether eventually a point is reached starting from which every issued request is accepted:

{ Req A .
EF (AG IAct-A1 )
where A 1 is the set of actions: { Req 1 .send refuse 1 to Req A .rec refuse 1, Req 2 .send refuse 1 to Req A .rec refuse 2, Req 3 .send refuse 1 to Req A .rec refuse 3 }.

Such a property holds as expected.

Separating functional behavior modeling and trust management specification allows for a clear verification of the impact of trust policies upon specific properties by simply adjusting the trust parameters of certain entities. For instance, let us replace the cautious requestee with a paranoid requestee characterized by strict trust requirements, and then let us consider the capability of such an entity of accepting services. To this aim, we adjust the trust infrastructure only, by tuning ρ, tth, and dispositional trust for entity Req 3 . As an example, with ρ = 0.8, tth(Req 3 ) = 5 (as for the cautious requestee), and dispositional trust less than 4, we obtain that the following property is not satisfied: EF (Req 3 .send accept 1 to Req A .rec accept 3) meaning that the paranoid requestee does not serve any request. The property turns out to hold if the dispositional trust is set to 4, in which case we also observe that, given A 1 = {Req 3 .send accept 1 to Req A .rec accept 3}, the property:

E((tt[Req 1 ; Req A ] < 10 ∧ tt[Req 2 ; Req A ] < 10) IAct U A1 true)
does not hold. More precisely, at least one of the other two requestees must recommend top trust towards the requester in order to allow the paranoid requestee to accept a request.

Finally, let us consider a coalition attack by two requestees against the third one. The condition of interest is formulated as follows. Can malicious requestees provide false feedback to the risky requestee thus avoiding her/him from accepting any request? To this aim, it is sufficient to extend the recommendation table by setting rt[Req 2 ; Req A ; Req 1 ] = rt[Req 3 ; Req A ; Req 1 ] = 0 (while all the other entries are as usual), and then check the TTL formula: ¬EF (Req 1 .send accept 1 to Req A .rec accept 1). This property is satisfied, thus revealing the effectiveness of the attack. By tuning the dispositional trust of the risky requestee, we observe that the attack can be avoided if and only if such a parameter is set to at least 4. On the other hand, if the false feedback is provided by Req 3 only, Req 1 can accept requests (even without altering her/his dispositional trust), but only after a successful interaction between Req 2 and Req A . In this case, we have also verified that extremely positive recommendations by Req 2 (rt[Req 2 ; Req A ; Req 1 ] = top) protect Req 1 from coalition attacks of (up to) 4 malicious requestees.

Related Work and Future Directions

In the literature, formal methods have been used successfully to model trust and trust relationships [START_REF] Nielsen | Towards a formal notion of trust[END_REF][START_REF] Huang | A Calculus of Trust and Its Application to PKI and Identity Management[END_REF][START_REF] Jøsang | Subjective logic book (draft)[END_REF]. However, usually these techniques represent trust without an integration with formal approaches to the modeling and verification of concurrent/distributed systems. Theoretical analysis of cooperation strategies is proposed in formal frameworks like, e.g., game theory [START_REF] Li | Game-Theoretic Analysis of Cooperation Incentives Strategies in Mobile Ad Hoc Networks[END_REF], and the theory of semirings [START_REF] Theodorakopoulos | On Trust Models and Trust Evaluation Metrics for Ad Hoc Networks[END_REF]. The analysis of trust chains is investigated also in a process algebraic setting, either with a specific focus on access control policies [START_REF] Martinelli | Towards an Integrated Formal Analysis for Security and Trust[END_REF], or by employing equivalence checking based analysis [START_REF] Carbone | A Calculus of Trust Management[END_REF]. In this paper we have proposed a process algebraic framework in which trust modeling and system specification are combined and model checking techniques are applied to verify the effects of trust models and related parameters upon cooperation in concurrent and distributed systems.

An extension under development concerns the semantics, which is currently based on nondeterministic labeled transition systems. Without altering the syntax of the language, the idea is to employ quantitative information deriving from the trust infrastructure in order to implement nonfunctional trust-based choice policies at the level of the semantics for interacting processes. For instance, trust can be interpreted as a weight guiding the choice among concurrent trust-based interactions, which thus becomes either probabilistic or prioritized. In the former case, the semantics would be based on probabilistic tlts. Further extensions are concerned with the use of reward structures expressing metrics that can be related to trust. This is the case, e.g., of the service cost, as well as any other parameter related to the quality of experience that may be influenced by (or may affect) trust. As an example, every time an interaction modeling a payment from I to J occurs, a certain reward depending on the trust relation between I and J is cumulated to express the amount paid by I. Then, similarly as done in the setting of quantitative model checking [START_REF] Baier | Performability Assessment by Model Checking of Markov Reward Models[END_REF][START_REF] Aldini | Performability Measure Specification: Combining CSRL and MSL[END_REF][START_REF] Chen | Automatic Verification of Competitive Stochastic Systems[END_REF], we can employ a version of TTL extended with probabilities and rewards to estimate the tradeoff existing between trust and other metrics, which is necessary to evaluate mixed cooperation incentive strategies [START_REF] Aldini | Formal Approach to Design and Automatic Verification of Cooperation-Based Networks[END_REF][START_REF] Aldini | Modeling and Verification of Cooperation Incentive Mechanisms in User-Centric Wireless Communications[END_REF].

  such that tt[I; J] denotes the direct trust of entity I towards entity J as a result of previous interactions between them. Each row tt[I; ] is initialized with the dispositional trust of I, which is the initial willingness of I to trust unknown users. -Recommendation table rt : S × S → T, such that rt[I; J] contains either the trust value recommended by I about J to other entities, or the special symbol δ to specify that I does not provide recommendations about J. -Trust threshold function tth : S → T, such that tth(I) represents the minimum amount of trust (towards other entities) required by I to execute a trusted interaction. -Trust variation function tv : IName → T, such that tv (I.a) is the trust feedback that I associates to the execution of interactions through action a.

P

  , Q ∈ P I.a to J.b ∈ SS P P[P /P, Q /Q] tt[I;J]=update(tt[I;J],tv (I.a)) tt[J;I]=update(tt[J;I],tv (J.b)) tf (I,J)≥tth(I) and: P, Q ∈ P I.a to J.b ∈ SS P I.a - to J.b --→ P[P /P, Q /Q] tt[I;J]=update(tt[I;J],tv (I.a)) tt[J;I]=update(tt[J;I],tv (J.b)) tf (I,J)<tth(I)

  req 1.Wait 1 + . . . + send req n.Wait n

	Wait i	def = rec accept i.Service i + rec refuse i.Requester	1 ≤ i ≤ n
	Service i	def = pay i.Requester + not pay i.Requester	1 ≤ i ≤ n
	while the requestee counterpart is as follows:
	Requestee	def = rec req 1.Decision 1 + . . . + rec req m.Decision m
	Decision i	def = send accept i. τ. Payment i ∓ send refuse i.Requestee 1 ≤ i ≤ m
	Payment i	def = rec pay i.Requestee + not rec pay i.Requestee	1 ≤ i ≤ m

  send req i to Req i .rec req 1 Req i .send accept 1 to Req A .rec accept i Req i .send refuse 1 to Req A .rec refuse i Req A .pay i to Req i .rec pay 1 Req A .not pay i to Req i .not rec pay 1 where 1 ≤ i ≤ 3.

  send req 1 to Req 1 .rec req 1, Req 1 .send accept 1 to Req A .rec accept 1, Req 1 .τ, Req A .not pay 1 to Req 1 .not rec pay 1 }.

Acknowledgment: This work has been partially supported by the MIUR project CINA (Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society).