We develop a comprehensive threat model for the automotive domain. It is accomplished by means of a novel, multilevel research methodology that leverages Human-Artificial Intelligence (HAI). Given the inherent complexity of threat modelling and the challenges in ensuring its completeness, the methodology combines the complementary strengths of human analysis with large language models over four phases. Each phase is structured as a sequence of two or three refinement levels so that each level iteratively enhances prior results through either human or artificial intelligence. The first phase focuses on modelling the system under analysis to establish a clear and structured baseline. The second phase addresses the elicitation of assets and associated threats, followed by a third phase in which mitigation strategies are designed. The fourth and final phase ensures that mitigation is augmented to explicitly incorporate Zero Trust, Pseudonymisation, and Data Minimisation within the context of the automotive domain. The methodology maintains its multilevel HAI structure across all phases, thereby fostering a dynamic validation loop between expert knowledge and machine-driven inference, ultimately enhancing both accuracy and coverage of the resulting threat model.

The importance of cybersecurity is widely acknowledged as paramount for virtually every computerized application domain. Not only is it concerned with the protection of digital assets and resources from illegitimate use, but it is also essential to people’s privacy, for example for shielding their personal data, and even to their safety, for example for safeguarding the functioning of devices that may potentially harm humans. This article investigates the extent to which cybersecurity is properly ensured of IoT devices (also commonly termed smart devices ) which are modern, that is, trendy at present, then also inexpensive, hence useful to evaluate a price-cybersecurity ratio, and, finally, commonly used. While it is clear that innumerable such devices exist, the findings reported below focus on the case of the Tapo ecosystem by TP-Link, which features cheap Amazon best sellers at present. Our findings suggest that effective Vulnerability Assessment and Penetration Testing sessions can be carried out on such devices by following the PETIoT kill chain. Findings also demonstrate that as many as six devices of the TAPO ecosystem suffer four previously unknown (so called zero-day ) vulnerabilities, which we filed as four CVEs on MITRE’s public database. Following Responsible Disclosure with TP-Link, vulnerabilities were publicly disclosed only after the vendor released appropriate fixes. All vulnerabilities were found using freeware, requiring over 600 lines of exploitation code.

The current digital landscape demands robust security requirements and, for doing so, the institutions enact complex security directives to protect the citizens and the infrastructures, particularly in the European Union. These directives aim to safeguard data and harmonise security across the European region, and institutions must navigate this evolving legal landscape in order to implement and keep up-to-date the prescribed security measures. However, understanding and implementing these directives towards full compliance can be difficult and expensive. Ontological representation can be employed to represent and operationalise such security directives, ultimately contributing to the effectiveness and efficiency of the compliance process. Ontologies in fact promote a structured approach to represent knowledge, making the applicable directives more simply understandable by humans and more readily processable by machines. This article introduces SecOnto, a novel methodology for representing security directives as ontologies. SecOnto breaks down the process of transforming the juridical language of modern security directives into full-fledged ontologies by means of five semi-automated steps: Preprocessing, Interpretation, Structuring, Representation and Verification. Each step is described and validated by means of operational examples based upon Directive 2022/2555 of the European Parliament and of the Council of the European Union on security of network and information systems, better known as NIS 2.

Security compliance constitutes a significant source of concern for many corporate decision-makers due to its complexity and cost. These may be due, first and foremost, to the style of juridical language, which is often challenging to translate into concrete operational procedures. To facilitate such a translation and ultimately optimise the compliance effort, this article presents “NIS2Onto”, an Web Ontology Language (OWL) ontology designed to translate the Network and Information Security Directive version 2 (NIS 2) into an ontological format aimed to favour unambiguous understanding and security operations of cybersecurity professionals, legal experts, and all organisational stakeholders. Through the semantic representation of the NIS 2 entities, relationships, and security measures, NIS2Onto enables automated compliance verification, streamlined risk assessments, and effective policy implementation. Our evaluation employs both metrical and qualitative analysis through a real case study to witness the robustness and practical applicability of NIS2Onto. The ontology not only supports the accurate interpretation of complex legal texts but also aids in systematically enforcing cybersecurity measures. Furthermore, the extensibility of NIS2Onto allows for integration with other regulatory frameworks, thereby fostering a comprehensive and unified approach to cybersecurity governance.

Within the dynamic realm of Intelligent Transportation Systems (ITS), the Internet of Vehicles (IoV) marks a significant paradigm shift. IoV is an interconnected network of vehicles, infrastructures, and the Internet, driven by wireless communication technologies. This paper dissects the privacy landscapes of ITS and IoV, exploring gaps and redundancies in standards and academic literature. We do so by leveraging European Telecommunications Standards Institute (ETSI) ITS G5 standards and IoV analyses from literature, and building two relational models to depict said privacy landscapes. A macroscopic analysis reveals structural and thematic differences: ITS, governed by established standards, has a robust structure, while IoV, in its nascent stage, lacks formalisation. A detailed analysis highlights challenges in data collection, sharing, and privacy policies. As ITS transitions to IoV, increasing data volume demands enhanced privacy safeguards. Addressing these challenges requires collaborative efforts to develop comprehensive privacy policies, prioritise user awareness, and integrate privacy-by-design principles. This paper offers insights into navigating the evolving landscape of transportation technologies, laying the groundwork for privacy-preserving ITS and IoV ecosystems.

Despite their apparent simplicity, devices like smart light bulbs and electrical plugs are often perceived as exempt from rigorous security measures. However, this paper challenges this misconception, uncovering how vulnerabilities in these seemingly innocuous devices can expose users to significant risks. This paper extends the findings outlined in previous work, introducing a novel attack scenario. This new attack allows malicious actors to obtain sensitive credentials, including the victim's Tapo account email and password, as well as the SSID and password of her local network. Furthermore, we demonstrate how these findings can be replicated, either partially or fully, across other smart devices within the same IoT ecosystem, specifically those manufactured by Tp-Link. Our investigation focused on the Tp-Link Tapo range, encompassing smart bulbs (Tapo L530E, Tapo L510E V2, and Tapo L630), a smart plug (Tapo P100), and a smart camera (Tapo C200). Utilizing similar communication protocols, or slight variants thereof, we found that the Tapo L530E, Tapo L510E V2, and Tapo L630 are susceptible to complete exploitation of all attack scenarios, including the newly identified one. Conversely, the Tapo P100 and Tapo C200 exhibit vulnerabilities to only a subset of attack scenarios. In conclusion, by highlighting these vulnerabilities and their potential impact, we aim to raise awareness and encourage proactive steps towards mitigating security risks in smart device deployment.

Legal language can be understood as the language typically used by those engaged in the legal profession and, as such, it may come both in spoken or written form. Recent legislation on cybersecurity obviously uses legal language in writing, thus inheriting all its interpretative complications due to the typical abundance of cases and sub-cases as well as to the general richness in detail. This paper faces the challenge of the essential interpretation of the legal language of cybersecurity, namely of the extraction of the essential Parts of Speech (POS) from the legal documents concerning cybersecurity.

Self-issued voice commands leverage the voice-controllable device’s internal speaker to issue malicious voice commands to the device itself. These attacks are a class of voice spoofing attacks particularly challenging to protect from, as it is very hard for a countermeasure solution to infer whether the command comes from an external entity or from the device itself. In this paper, we propose a countermeasure against self-issued voice commands by training a Twin Neural Network to recognise the differences between what is being played and what is being recorded by the voice-controllable device. In fact, these audios are very similar in case of voice command self-issue attacks and different in case of legitimate commands. We start with a security and usability trade-off analysis of countermeasures against voice spoofing attacks, by describing different classes of synthesised voice commands that need to be blocked or allowed, depending on the necessities of the user. Then, we present our solution to protect voice-controllable devices from self-issued commands and show that it correctly classifies commands in the benign (real-user) and malign (self-issued) categories 97% of the times on average. We compare this result with state-of-the-art anomaly detection techniques as a baseline and show that our solution outperforms them. Furthermore, we instantiate our countermeasure on three different classes of devices to measure its performance, and we find that the additional overhead is negligible. Finally, we measure the usability impact of our solution when users interact with the tested device under different conditions, showing that our solution is resistant to environmental changes and regardless of the identity of the user issuing the commands.

Contains fulltext : 290606.pdf (Publisher’s version ) (Open Access)

The IoT is getting more and more pervasive. Even the simplest devices, such as a light bulb or an electrical plug, are made "smart" and controllable by our smartphone. This paper describes the findings obtained by applying the PETIoT kill chain to conduct a Vulnerability Assessment and Penetration Testing session on a smart bulb, the Tapo L530E by Tp-Link, currently best seller on Amazon Italy. We found that four vulnerabilities affect the bulb, two of High severity and two of Medium severity according to the CVSS v3.1 scoring system. In short, authentication is not well accounted for and confidentiality is insufficiently achieved by the implemented cryptographic measures. In consequence, an attacker who is nearby the bulb can operate at will not just the bulb but all devices of the Tapo family that the user may have on her Tapo account. Moreover, the attacker can learn the victim's Wi-Fi password, thereby escalating his malicious potential considerably. The paper terminates with an outline of possible fixes.

This paper questions how to approach threat modelling in the automotive domain at both an abstract level that features no domain-specific entities such as the CAN bus and, separately, at a detailed level. It addresses such questions by contributing a systematic method that is currently affected by the analyst's subjectivity because most of its inner operations are only defined informally. However, this potential limitation is overcome when candidate threats are identified and left to everyone's scrutiny. The systematic method is demonstrated on the established LINDDUN threat modelling methodology with respect to 4 pivotal works on privacy threat modelling in automotive. As a result, 8 threats that the authors deem not representable in LINDDUN are identified and suggested as possible candidate extensions to LINDDUN. Also, 56 threats are identified providing a detailed, automotive-specific model of threats.

We present ALEXA VERSUS ALEXA (AvA), a novel attack that leverages audio files containing voice commands and audio reproduction methods in an offensive fashion, to gain control of Amazon Echo devices for a prolonged amount of time. AvA leverages the fact that Alexa running on an Echo device correctly interprets voice commands originated from audio files even when they are played by the device itself -- i.e., it leverages a command self-issue vulnerability. Hence, AvA removes the necessity of having a rogue speaker in proximity of the victim's Echo, a constraint that many attacks share. With AvA, an attacker can self-issue any permissible command to Echo, controlling it on behalf of the legitimate user. We have verified that, via AvA, attackers can control smart appliances within the household, buy unwanted items, tamper linked calendars and eavesdrop on the user. We also discovered two additional Echo vulnerabilities, which we call Full Volume and Break Tag Chain. The Full Volume increases the self-issue command recognition rate, by doubling it on average, hence allowing attackers to perform additional self-issue commands. Break Tag Chain increases the time a skill can run without user interaction, from eight seconds to more than one hour, hence enabling attackers to setup realistic social engineering scenarios. By exploiting these vulnerabilities, the adversary can self-issue commands that are correctly executed 99% of the times and can keep control of the device for a prolonged amount of time. We reported these vulnerabilities to Amazon via their vulnerability research program, who rated them with a Medium severity score. In addition, we discuss the results of a set of tests performed on three voluntary Echo-equipped households to verify the feasibility of AvA in real scenarios, finding that the attack remains undetected and operative in most cases. Finally, to assess limitations of AvA on a larger scale, we provide the results of a survey performed on a study group of 18 users, and we show that most of the limitations against AvA are hardly used in practice.

Electronic Control Units (ECUs) communicate with each other to accomplish the functionalities of modern vehicles. ECUs form an in-vehicle network that is precisely regulated and must be adequately protected from malicious activity, which has had several outbreaks in recent years. Therefore, we present CINNAMON, an AUTOSAR-based Basic Software Module that aims at confidentiality, integrity and authentication, all at the same time, for the traffic exchanged over the bus protocols that AUTOSAR supports. CINNAMON in fact stands for Confidential, INtegral aNd Authentic onboard coMmunicatiON. This article introduces the requirements and specification of CINNAMON in a differential fashion with respect to the existing Secure Onboard Communication Basic Software Module, which does not include confidentiality. As a result, CINNAMON exceeds SecOC at least against information gathering attacks. The article then defines three security profiles, regulating also the freshness attribute appropriately. Most importantly, CINNAMON is not a simple academic exercise because it is implemented in a laboratory environment on commercial ECUs, thus reaching the level of TRL 4, “Component and/or breadboard validation in laboratory environment”. The runtimes obtained on inexpensive devices are reassuring, paving the way for a possible large-scale application.

Abstract Fuzzing has become one of the best-established methods to uncover software bugs. Meanwhile, the market of embedded systems, which binds the software execution tightly to the very hardware architecture, has grown at a steady pace, and that pace is anticipated to become yet more sustained in the near future. Embedded systems also benefit from fuzzing, but the innumerable existing architectures and hardware peripherals complicate the development of general and usable approaches, hence a plethora of tools have recently appeared. Here comes a stringent need for a systematic review in the area of fuzzing approaches for embedded systems, which we term “embedded fuzzing” for brevity. The inclusion criteria chosen in this article are semi-objective in their coverage of the most relevant publication venues as well as of our personal judgement. The review rests on a formal definition we develop to represent the realm of embedded fuzzing. It continues by discussing the approaches that satisfy the inclusion criteria, then defines the relevant elements of comparison and groups the approaches according to how the execution environment is served to the system under test. The resulting review produces a table with 42 entries, which in turn supports discussion suggesting vast room for future research due to the limitations noted.

Socio-Technical Systems (STSs) combine the operations of technical systems with the choices and intervention of humans, namely the users of the technical systems. Designing such systems is far from trivial due to the interaction of heterogeneous components, including hardware components and software applications, physical elements such as tickets, user interfaces, such as touchscreens and displays, and notably, humans. While the possible security issues about the technical components are well known yet continuously investigated, the focus of this article is on the various levels of threat that human actors may pose, namely, the focus is on security ceremonies. The approach is to formally model human threats systematically and to formally verify whether they can break the security properties of a few running examples: two currently deployed Deposit-Return Systems (DRSs) and a variant that we designed to strengthen them. The two real-world DRSs are found to support security properties differently, and some relevant properties fail, yet our variant is verified to meet all the properties. Our human threat model is distributed and interacting: it formalises all humans as potential threatening users because they can execute rules that encode specific threats in addition to being honest, that is, to follow the prescribed rules of interaction with the technical system; additionally, humans may exchange information or objects directly, hence practically favour each other although no specific form of collusion is prescribed. We start by introducing four different human threat models, and some security properties are found to succumb against the strongest model, the addition of the four. The question then arises on what meaningful combinations of the four would not break the properties. This leads to the definition of a lattice of human threat models and to a general methodology to traverse it by verifying each node against the properties. The methodology is executed on our running example for the sake of demonstration. Our approach thus is modular and extensible to include additional threats, potentially even borrowed from existing works, and, consequently, to the growth of the corresponding lattice. STSs can easily become very complex, hence we deem modularity and extensibility of the human threat model as key factors. The current computer-assisted tool support is put to test but proves to be sufficient.

This paper presents SixPack, a cyber attack to VANET communications that is able to go undetected by the current state-of-the-art anomaly detectors. The SixPack attack is a dynamic attack conducted by an insider attacker who modifies the content of the Basic Safety Messages to pretend a sudden activation of the braking system with the consequent activation of the Anti-lock Braking System, and create a fake representation of the vehicle. The attacker then rejoins the fake representation of the vehicle with the real one, avoiding the current state-of-the-art anomaly detectors. We experimentally evaluated the evasion capabilities of the SixPack attack using the F2MD test framework on the LuST and LuSTMini city scenarios, demonstrating the ability of the attacker to generate a high percentage of false positives that prevent the attack from being detected consistently.

Modern vehicles embed a lot of software that turns them into Cyper-Physical Systems (CPS). Electronic Control Units (ECUs) communicate through the CAN bus protocol, which was not designed to be secure. This paper presents a proof-of-concept of TOUCAN, a new security protocol designed to secure CAN bus communications following the AUTOSAR standard. The presentation introduces design, implementation and performance of TOUCAN on a test-bed composed by two inexpensive boards that can be demonstrated to exchange secure TOUCAN frames.

Modern vehicles abound with Electronic Control Units (ECUs) that need to speak with each other. They adopt a binary language and form an in-vehicle network that must be precisely regulated. This was the aim for the inception of "Controller Area Network" protocol, also known as CAN bus [1] and is widespread today. It is standardised in ISO 11898-1:2015 [4] as a simple protocol based on two bus lines. However, it is not meant to be secure.

Mobile users have got used to getting useful information while they are literally on the move. An implication of this habit is that certain live information, such as that for navigation, for dating and for handling emergencies, should be tailored to the user's current location. While this is technically feasible with the current technology, it raises concerns on the user's location privacy. To address the delicate tradeoff between user's location privacy and appropriateness of the information for that location, this paper discusses three information delivery protocols. One is the widely adopted Android's protocol, the other two are the authors' novel ones, termed AL protocol and LBPP protocol respectively. The former conceals the user's location within a geographical area, the latter employs secure two-party computation. Privacy of all protocols is analysed, motivating the choice to implement the LBPP protocol. It is made available as the "Getmewhere" service for the reader to download.

The authentication of a web server is a crucial procedure in the security of web browsing. It relies on certificate validation, a process that may require the participation of the user. Thus, the security of certificate validation is socio-technical as it depends on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. This manuscript analyzes extensively the socio-technical security of certificate validation as carried out through today’s most popular browsers. First, we model processes, protocols and ceremonies that browsers run with servers and users as UML activity diagrams. We consider both classic and private browsing modes and focus on the certificate validation. We then translate each UML activity diagram to a CSP# model. The model is expanded with the LTL formalization of five socio-technical properties pivoted on user involvement with certificate validation. We automatically check whether the CSP# models are socio-technically secure against Man-in-the-Middle attacks using the PAT model checker. The findings turn out to be far from straightforward. From them, we state best-practice recommendations to browser vendors.

The security and privacy of the data that users transmit, more or less deliberately, to modern services is an open problem. It is not solely limited to the actual Internet traversal, a sub-problem vastly tackled by consolidated research in security protocol design and analysis. By contrast, it enta ils much broader dimensions pertaining to how users approach technology and understand the risks for the data they enter. For example, users may express cautious or distracted personas depending on the service and the point in time; further, pre-established paths of practice may lead them to neglect the intrusive privacy policy offered by a service, or the outdated protections adopted by another. The approach that sees the service security and privacy problem as a socio-technical one needs consolidation. With this motivation, the article makes a threefold contribution. It reviews the existing literature on service security and privacy, especially from the socio-technical standpoint. Further, it outlines a general research methodology aimed at layering the problem appropriately, at suggesting how to position existing findings, and ultimately at indicating where a transdisciplinary task force may fit in. The article concludes with the description of the three challenge domains of services whose security and privacy we deem open socio-technical problems, not only due to their inherent facets but also to their huge number of users.

An exam is a practise for assessing the knowledge of a candidate from an examination she takes. Exams are used in various contexts, such as in university tests and public competitions. We begin by identifying various security and privacy requirements that modern exams should meet, especially in the prospect of them being supported by information and communication technologies. These requirements extend well beyond ensuring authenticating the candidate and preventing her from cheating. Cheating is routinely enforced by invigilation by trusted parties, whereas we discuss that an exam should meet its security and privacy requirements against stronger threat models, including malicious exam authorities. Thus exams must be designed with the care normally devoted to security protocols, and in such a mindset we present WATA IV, a new protocol that meets our security and privacy requirements even when an exam manager is malicious.

Abstract The Inductive Method is among the most established tools to analyse security protocols formally. It has successfully coped with large, deployed protocols, and its findings are widely published. However, perhaps due to its embedding in a theorem prover or to the lack of tutorial publications, it is at times criticised to require super-specialised skills and hence to be rather impractical. This paper aims at showing that criticism to be stereotypical. It pursues its aim by presenting the first tutorial-style paper to using the Inductive Method. This paper cannot cover every aspect of the method. It focuses on a key one, that is how the Inductive Method treats one of the main goals of security protocols: confidentiality against a threat model. The treatment of that goal, which may seem elegant in the Inductive Method, in fact forms a key aspect of all protocol analysis tools, hence the paper motivation rises still. With only standard skills as a requirement, the reader is guided step by step towards design and proof of significant confidentiality theorems. These are developed against two threat models, the standard Dolev–Yao and a more up-to-date one, the General Attacker, the latter turning out particularly useful also for didactic purposes.

Electronic exam systems are pieces of software employed in online educations to assess performances of students. However, both the security of the protocols they reply upon and a general understanding of the possible threats is still to be met. This manuscript outlines a Ph.D. research work wherein we attempt to shed some light in the area. We identify the phases composing a typical exam system, we comments on relevant security properties that should be preserved in the various phases, and we advances an informal though structured definitions of them.

Authenticating a web server is crucial to the security of web browsing. It relies on TLS certificate validation, a property whose enforcement may require getting the user involved. Thus, certificate validation is a socio-technical property - it relies on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. Hence the need for an appropriate methodology to study certificate validation from a socio-technical perspective. Certificate validation as carried out through today's most popular browsers - Chrome, Internet Explorer, Firefox and Opera Mini - is first represented by means of UML activity diagrams. It is then translated into CSP#, and expanded with the LTL formalization of four socio-technical properties pivoted on user involvement with certificate validation. The properties are then checked automatically using the PAT model checker. The findings turn out to be far from straightforward and, most importantly, allowed for prototyping a basic methodology for the sociotechnical formal analysis of security properties.

Security protocols are often analysed in isolation as academic challenges. However, the real world can require various combinations of them, such as a certified email protocol executed over a resilient channel, or the key registration protocol to precede the purchase protocols of Secure Electronic Transactions (SET). We develop what appears to be the first scalable approach to specifying and analysing mix protocols. It expands on the Inductive Method by exploiting the simplicity with which inductive definitions can refer to each other. This lets the human analyst study each protocol separately first, and then derive holistic properties about the mix. The approach, which is demonstrated on the sequential composition of a certification protocol with an authentication one, is not limited by the features of the protocols, which can, for example, share message components such as cryptographic keys and nonces. It bears potential for the analysis of complex protocols constructed by general composition of others.

Amazon is the world's largest e-shopping site, with its market capitalization having just passed $100 billion [1]. Internet users interaction with its web site is an example of a widespread security ceremony - a ceremony focuses on security- related human interaction with technology, including security protocols and on-line service consumption [2]. This paper focuses on how Amazon's ceremony manages the users' security and privacy through the digital identities they may create with the popular web site. It leverages on the cognitive walkthrough method [3] to distill tasks, steps and walkthroughs of the ceremony, and then to pinpoint four risks affecting the users' security and privacy. It formulates four corresponding recommendations for technical web site updates that would resolve the noted risks. In particular, the recommendations address common contexts such as users accessing Amazon from their smartphones. A possible explanation of the coexistence of such risks with the late capitalization achievements is that users are more driven by familiarity and confidence than by trust. These findings are meant to be complemented with a homologous assessment from Amazon's standpoint.

The use of small portables and mobile devices has made MANETs (mobile ad hoc networks) very popular. A MANET is a network composed by a group of mobile nodes without any fixed device or a central coordination. They work in an open net and their collaboration is the sole means to allow communications and the survival of the MANET itself. A critical issue is to assess the behaviour of the nodes that participate in the network, possibly identifying selfish conduct that can compromise the functioning of the system. This paper shows a method to evaluate the behaviour of all nodes by establishing a reputation value that represents the trustworthiness of each node. A protocol is presented to calculate the reputation of a node by locally observing the node from another one, and then tuning this intermediate value with additional observations from other participants. When the reputation value of a node is available, it is circulated and distributed uniformly over the network. This reputation protocol is viable. Each node can efficiently calculate the reputation values of its neighbours and then of all network nodes. A variety of simulations conducted using the network simulator NS-2 strongly support these claims.

A recent privacy protocol for secure e-polls aims at ensuring the submitting individuals that the pollster will preserve the privacy of their submitted preferences. Otherwise the individuals can indict the pollster, provided that the pollster participates actively in this phase. The analysis of the protocol in a realistic threat model denounces that a malicious pollster that abuses the private preferences by disclosure will arguably not help out during its own indictment. Therefore, the protocol ensures insufficient fairness among their participants because it gives the pollster some advantage over the individuals. Two variant protocols are introduced and analysed in the same threat model - one is found to move the advantage over the individuals, the other is found to achieve a satisfactory level of fairness.

Classical security protocols aim to achieve authentication and confidentiality under the assumption that the peers behave honestly. Some recent protocols are required to achieve their goals even if the peer misbehaves. Accountability is a protocol design strategy that may help. It delivers to peers sufficient evidence of each other's participation in the protocol. Accountability underlies the nonrepudiation protocol of Zhou and Gollmann and the certified email protocol of Abadi et al. This paper provides a comparative, formal analysis of the two protocols, and confirms that they reach their goals under realistic conditions. The treatment, which is conducted with mechanized support from the proof assistant Isabelle, requires various extensions to the existing analysis method. A byproduct is an account of the concept of higher-level protocol .

The importance of Information Security to virtually every level and aspect of modern society is widely accepted.The field is one of the most dynamic in computer science and a growing number of research symposia are devoted to this discipline every year.Business, government, transport, critical infrastructures etc. routinely have to face security issues.News items highlighting security concerns appear in the media with increasing frequency.The 19th ACM Symposium on Applied Computing was held 14-17 March 2004 in Nicosia, Cyprus.Its Security Track, the third in the series, hosted twelve talks, based on the respective papers included in the conference proceedings, in diverse areas of information security.The Track was organized as a research conference itself, drawing on the expertise of the ten eminent representatives of both Industry and Academia forming its program committee.Their efforts resulted in each of the forty submitted papers getting at least three reviews.This special issue of the Journal of Computer Security presents the four best papers among those presented at the conference.Originally, eight had been selected.Each of the eight was then upgraded by the authors so as to guarantee at least 30% new material with respect to the conference version.Each upgraded paper was additionally reviewed by at least two leading experts in Computer Security, and the four best papers could be selected accordingly.The best papers reflect the wide diversity of the workshop and provide, we believe, valuable contributions to the field.The first, by Bistarelli et al., uses the framework of soft constraints to model the problem of vulnerabilities cascading through a network.The second, by Collberg and Sahoo, presents an analysis of the robustness of the SHKQ software watermarking algorithm.The third, by Nenadić et al., presents a pair of related protocols for certified e-mail with fair non-repudiation of origin and receipt.The final paper, by Siaterlis and Maglaris, presents a novel data fusion based approach to the detection of distributed denial of service attacks.

In recent years, research in computer security has become part of all fields in computer science.The proliferation of network computing and mobile computation, and especially the ubiquity of the Internet, has made security one of the key areas in modern computing.Security is a multidisciplinary topic related to almost every aspect of computer science.From information assurance to mobile computation, from artificial intelligence to wireless communication, it is difficult to find a computer science field in which security is not a concern directly or indirectly.Security threats are a constant hassle to system administrators worldwide, as well as to the average home computer user.Such 'popularity' makes security the prime concern to computer industries today.The selected papers for this special issue demonstrate the multidisciplinary aspect of the field.The main focus is on the practical (applied) aspects of computer security so as to fit well with the general objectives of the symposium.These objectives are also well in line with the objectives of this journal.The requirement to be 'applied' is not a restriction to computer security researchers, since most of the research in this field is applied by nature.The papers in this special issue consist of expanded versions of the best papers presented at the Computer Security Track of the 2003 ACM Symposium on Applied Computing held in Melbourne, Florida, 9-12 March 2003.These four articles were fully reviewed and chosen from an original pool of 28 papers from 19 different countries.The papers were extensively reviewed in a process that involved 57 reviewers in total and re-reviewed after the extended versions were submitted so as to ensure journal quality.The four papers represent the wide spectrum of the computer security field.Atallah and Lonardi describe a variation for the LZ-77 algorithm that warranties the authenticity of the data.Gassend et al. propose the use of delays associated with integrated circuits as an authentication mechanism that is shown to be a better alternative to the use of digital information embedded in the circuit (keys).Raman et al. tackle the problem of discovering services in pervasive networks by describing a scalable, access-controlled architecture based on an intentional naming system.Finally, Shin et al. propose the Role Administration (RA) system to help establish a set of roles and role hierarchies; the RA system can be used to build role-based authorization infrastructures.

Security protocols stipulate how the remote principals of a computer network should interact in order to obtain specific security goals. The crucial goals of confidentiality and authentication may be achieved in various forms, each of different strength. Using soft (rather than crisp) constraints, we develop a uniform formal notion for the two goals. They are no longer formalised as mere yes/no properties as in the existing literature, but gain an extra parameter, the security level. For example, different messages can enjoy different levels of confidentiality, or a principal can achieve different levels of authentication with different principals. The goals are formalised within a general framework for protocol analysis that is amenable to mechanisation by model checking. Following the application of the framework to analysing the asymmetric Needham-Schroeder protocol (Bella and Bistarelli 2001; Bella and Bistarelli 2002), we have recently discovered a new attack on that protocol as a form of retaliation by principals who have been attacked previously. Having commented on that attack, we then demonstrate the framework on a bigger, largely deployed protocol consisting of three phases, Kerberos.

An existing approach based on induction and theorem proving is tailored to the verification of security protocols that make use of smart cards. Smart cards are modelled operationally, hence only their functionalities, rather than their implementative technicalities, are of interest. The spy can steal certain smart cards, and clone others while learning their stored secrets. In terms of generality, the approach scales up to protocols that assume secure or insecure means between agents and smart cards, as well as to smart cards being PIN-operated or PIN-less. In terms of extensibility, new, application-dependent smart card functionalities can be easily included. The approach is demonstrated on the key distribution protocol designed by Shoup and Rubin [30], and the assumptions are studied that are necessary on the smart cards for the protocol goals to be met. It is found that, if the data buses of the smart cards are unreliable as to produce outputs in an unspecified order, then the protocol does not confirm to the peers its goals of confidentiality, authentication, and key distribution because of lack of explicitness. A simple fix is introduced and proved.

Secure electronic transaction (SET) is an immense e-commerce protocol designed to improve the security of credit card purchases. In this paper, we focus on the initial bootstrapping phases of SET, whose objective is the registration of cardholders and merchants with a SET certificate authority. The aim of registration is twofold: getting the approval of the cardholder's or merchant's bank and replacing traditional credit card numbers with electronic credentials that cardholders can present to the merchant so that their privacy is protected. These registration subprotocols present a number of challenges to current formal verification methods. First, they do not assume that each agent knows the public keys of the other agents. Key distribution is one of the protocols' tasks. Second, SET uses complex encryption primitives (digital envelopes) which introduce dependency chains: the loss of one secret key can lead to potentially unlimited losses. Building upon our previous work, we have been able to model and formally verify SETs registration with the inductive method in Isabelle/HOL (T. Nipkow et al., 2002). We have solved its challenges with very general techniques.

The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a purchase, the SET dual signature guarantees authenticity while keeping the customer's account details secret from the merchant and his choice of goods secret from the bank.This paper reports the first verification results for the complete purchase phase of SET. Using Isabelle and the inductive method, we showed that the credit card details do remain confidential and customer, merchant and bank can confirm most details of a transaction even when some of those details are kept from them. The complex protocol construction makes proofs more difficult but still feasible.Though enough goals can be proved to give confidence in SET, a lack of explicitness in the dual signature makes some agreement properties fail: it is impossible to prove that the customer meant to sent his credit card details to the payment gateway that receives them.