An ever-increasing number of critical infrastructures rely heavily on the assumption that security protocols satisfy a wealth of requirements. Hence, the importance of certifying e.g., privacy properties using methods that are better at detecting attacks can hardly be overstated. This paper scrutinises the “unlinkability” privacy property using relations equating behaviours that cannot be distinguished by attackers. Starting from the observation that some reasonable design choice can lead to formalisms missing attacks, we draw attention to a classical concurrent semantics accounting for relationship between past events, and show that there are concurrency-aware semantics that can discover attacks on all protocols we consider. More precisely, we focus on protocols where trace equivalence is known to miss attacks that are observable using branching-time equivalences. We consider the impact of three dimensions: design decisions made by the programmer specifying an unlinkability problem (style), semantics respecting choices during execution (branching-time), and semantics sensitive to concurrency (non-interleaving), and discover that reasonable styles miss attacks unless we give attackers enough power to observe choices and concurrency. Our main contribution is to draw attention to how a popular concurrent semantics – history-preserving bisimilarity – when defined for the non-interleaving applied π -calculus, can discover attacks on all protocols we consider, regardless of the choice of style. Furthermore, we can describe all such attacks using a novel modal logic that is hence suitable to formally certify attacks on privacy properties. This study highlights the threats posed by relying exclusively on tools implementing coarser semantics for protocol verification, and justifies in a very precise sense why security practitioners should account for history between past events to build reliable tools.

Software-based memory-erasure protocols are two-party communication protocols where a verifier instructs a computational device to erase its memory and send a proof of erasure. They aim at guaranteeing that low-cost IoT devices are free of malware by putting them back into a safe state without requiring secure hardware or physical manipulation of the device. Several software-based memory-erasure protocols have been introduced and theoretically analysed. Yet, many of them have not been tested for their feasibility, performance and security on real devices, which hinders their industry adoption. This article reports on the first empirical analysis of software-based memory-erasure protocols with respect to their security, erasure guarantees, and performance. The experimental setup consists of 3 modern IoT devices with different computational capabilities, 7 protocols, 6 hash-function implementations, and various performance and security criteria. Our results indicate that existing software-based memory-erasure protocols are feasible, although slow devices may take several seconds to erase their memory and generate a proof of erasure. We found that no protocol dominates across all empirical settings, defined by the computational power and memory size of the device, the network speed, and the required level of security. Interestingly, network speed and hidden constants within the protocol specification played a more prominent role in the performance of these protocols than anticipated based on the related literature. We provide an evaluation framework that, given a desired level of security, determines which protocols offer the best trade-off between performance and erasure guarantees.

Deep neural networks are widely deployed with quantization techniques to reduce memory and computational costs by lowering the numerical precision of their parameters. While quantization alters model parameters and their outputs, existing privacy analyses primarily focus on full-precision models, leaving a gap in understanding how bit-width reduction can affect privacy leakage. We present the first systematic study of the privacy–utility relationship in post-training quantization (PTQ), a versatile family of methods that can be applied to pretrained models without further training. Using membership inference attacks as our evaluation framework, we analyze three popular PTQ algorithms—AdaRound, BRECQ, and OBC—across multiple precision levels (4-bit, 2-bit, and 1.58-bit) on CIFAR-10, CIFAR-100, and TinyImageNet datasets. Our findings consistently show that low-precision PTQs can reduce privacy leakage. In particular, lower-precision models demonstrate up to an order of magnitude reduction in membership inference vulnerability compared to their full-precision counterparts, albeit at the cost of decreased utility. Additional ablation studies on the 1.58-bit quantization level show that quantizing only the last layer at higher precision enables fine-grained control over the privacy-utility trade-off. These results offer actionable insights for practitioners to balance efficiency, utility, and privacy protection in real-world deployments.

Estonia has been deploying electronic voting for its government elections since 2005. The underlying e-voting system and protocol have been continuously improved, aiming to fix the vulnerabilities found over the years and to provide election verifiability, which is now the standard way to ensure election integrity despite corrupt infrastructure or parties. Another goal is receipt-freeness, to ensure privacy even if voters are coerced. However, several recent attacks against its verifiability and privacy show the need of rigorous, realistic formal specifications for the protocol and its security, of new solutions to mitigate attacks, and of automated security proofs to ensure all attacks have been covered. In this paper we propose:

Federated recommendation (FR) is a decentralised approach to training personalised recommender systems, protecting users' privacy by avoiding data collection. Despite its privacy advantages, FR remains vulnerable to poisoning attacks. We focus on untargeted poisoning attacks against FR which degrade the overall performance of recommender services, leading to a detrimental impact on user experience and service quality. In this paper, we propose a general framework to formalise untargeted attacks and identify the vital role played by the interplay between items and user profiles in determining FR's performance. We present an untargeted attack FRecAttack2 which exploits this interplay. Specifically, we develop various methods for sampling user profiles, which approximate user distributions with and without collusion among malicious users. Then we leverage a new measurement to identify items that can disrupt the original interplay with user profiles, based on the change velocity of items' recommendation scores during optimisation. Extensive experiments demonstrate the superiority of our attack, outperforming existing methods by up to 27.56%, and its stealthiness in evading mainstream defences. To counteract untargeted attacks, we present a defence GuardCQ to detect malicious users by quantifying their contribution to boost the right interplay between items and user profiles. Empirical results show that GuardCQ effectively mitigates the attack's impact on FR and enhances the robustness of FR against poisoning attacks.

A Proof of Secure Erasure (PoSE) is a communication protocol where a verifier seeks evidence that a prover has erased the memory on a given device within the time frame of the protocol execution. Designers of PoSE protocols have long been aware that, if a prover can outsource the computation of the memory erasure proof to another device, then their protocols are trivially defeated. As a result, most software-based PoSE protocols in the literature assume that provers are isolated during the protocol execution, that is, provers cannot receive help from a network adversary. Our main contribution is to show that this assumption is not necessary. We introduce formal models for PoSE protocols playing against provers aided by external conspirators and develop two PoSE protocols that we prove secure in this context. We reduce the requirement of isolation to the more realistic requirement that the communication with the external conspirator is relatively slow. Software-based protocols with such relaxed isolation assumptions are especially pertinent for low-end devices, where it is too costly to deploy sophisticated protection methods.

We evaluate a bundle of specifications from the Self-Sovereign Identity (SSI) paradigm to construct an authentication protocol for the Web. We demonstrate how relevant standards such as W3C Verifiable Credentials (VC), W3C Decentralised Identifiers (DIDs), and components of the Hyperledger Aries Framework are to be assembled methodologically into a protocol. We make those assumptions from standard trust models explicit that underlie the derived protocol, and verify security and privacy properties, notably secrecy, authentication, and unlinkability. This enables us to formally justify the additional precision that we urge these specifications to consider, to ensure that implementors of SSI-based systems do not neglect security-critical controls.

The most prevalent smart card-based payment method, EMV, currently offers no privacy to its users. Transaction details and the card number are sent in cleartext, enabling the profiling and tracking of cardholders. Since public awareness of privacy issues is growing and legislation, such as GDPR, is emerging, we believe it is necessary to investigate the possibility of making payments anonymous and unlikable without compromising essential security guarantees and functional properties of EMV. This paper draws attention to trade-offs between functional and privacy requirements in the design of such a protocol. We present the UTX protocol - an enhanced payment protocol satisfying such requirements, and we formally certify key security and privacy properties using techniques based on the applied π-calculus.

Electronic voting is a prominent example of conflicting requirements in security protocols, as the triad of privacy, verifiability and usability is essential for their deployment in practice. Receipt-freeness is a particularly strong notion of privacy, stating that it should be preserved even if voters cooperate with the adversary. While there are impossibility results showing we cannot have receipt-freeness and verifiability at the same time, there are several protocols that aim to achieve both, based on carefully devised trust assumptions. To evaluate their security, we propose a general symbolic definition of election verifiability, extending the state of the art to capture the more complex structure of receipt-free protocols. We apply this definition to analyse, using ProVerif, recent protocols with promising practical features: BeleniosRF and several variants of Selene. Against BeleniosRF, we find several attacks showing that verifiability in Belenios does indeed suffer from the attempt to introduce receipt-freeness. On the other hand, Selene satisfies a weaker notion of receipt-freeness, but we show that it satisfies verifiability in stronger corruption scenarios. We introduce a general frame-work to compare the verifiability of these protocols in various corruption scenarios and conclude with an analysis of SeleneRF, an attempt to get the best of both that we formalise in this paper. In addition to extending the symbolic model, our results point to foundational gaps in current cryptographic models for election verifiability, as they fail to uncover attacks that we do.

Distance-bounding protocols are security protocols with a time measurement phase used to detect relay attacks, whose security is typically measured against mafia-fraud and distance-fraud attacks. A prominent subclass of distance-bounding protocols, known as lookup-based protocols, use simple lookup operations to diminish the impact of the computation time in the distance calculation. Independent results have found theoretical lower bounds 12nn2+1 and 12n, where n is the number of time measurement rounds, on the security of lookup-based protocols against mafia and distance-fraud attacks, respectively. However, it is still an open question whether there exists a protocol achieving both security bounds. This article closes this question in two ways. First, we prove that the two lower bounds are mutually exclusive, meaning that there does not exist a lookup-based protocol that provides optimal protection against both types of attacks. Second, we provide a lookup-based protocol that approximates those bounds by a small constant factor. Our experiments show that, restricted to a memory size that linearly grows with n, our protocol offers strictly better security than previous lookup-based protocols against both types of fraud.

The fair exchange problem has faced for a long time the bottleneck of a required trusted third party. The recent development of blockchains introduces a new type of party to this problem, whose trustworthiness relies on a public ledger and distributed computation. The challenge in this setting is to reconcile the minimalistic and public nature of blockchains with elaborate fair exchange requirements, from functionality to privacy. Zero-knowledge contingent payments (ZKCP) are a class of protocols that are promising in this direction, allowing the fair exchange of data for payment. We propose a new ZKCP protocol that, when compared to others, requires less computation from the blockchain and less interaction between parties. The protocol is based on two-party (weak) adaptor signatures, which we show how to instantiate from state of the art multiparty signing protocols. We improve the symbolic definition of ZKCP security and, for automated verification with Tamarin, we propose a general security reduction from the theory of abelian groups to the theory of exclusive or.

To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point out that active attackers were not previously accounted for in the privacy requirements of this proposal protocol, and demonstrate that an active attacker can compromise unlinkability within a distance of 100cm. Here, we adopt a strong definition of unlinkability that does account for active attackers and propose an enhancement of the protocol proposed by EMVCo. We prove that our protocol does satisfy strong unlinkability, while preserving authentication.

Various modern protocols tailored to emerging wire-less networks, such as body area networks, rely on the proximity and honesty of devices within the network to achieve their security goals. However, there does not exist a security framework that supports the formal analysis of such protocols, leaving the door open to unexpected flaws. In this article we introduce such a security framework, show how it can be implemented in the protocol verification tool Tamarin, and use it to find previously unknown vulnerabilities on two recent key exchange protocols.

Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.

Abstract Active re-identification attacks constitute a serious threat to privacy-preserving social graph publication, because of the ability of active adversaries to leverage fake accounts, a.k.a.sybil nodes, to enforce structural patterns that can be used to re-identify their victims on anonymised graphs. Several formal privacy properties have been enunciated with the purpose of characterising the resistance of a graph against active attacks. However, anonymisation methods devised on the basis of these properties have so far been able to address only restricted special cases, where the adversaries are assumed to leverage a very small number of sybil nodes. In this paper, we present a new probabilistic interpretation of active re-identification attacks on social graphs. Unlike the aforementioned privacy properties, which model the protection from active adversaries as the task of making victim nodes indistinguishable in terms of their fingerprints with respect to all potential attackers, our new formulation introduces a more complete view, where the attack is countered by jointly preventing the attacker from retrieving the set of sybil nodes, and from using these sybil nodes for re-identifying the victims. Under the new formulation, we show thatk-symmetry, a privacy property introduced in the context of passive attacks, provides a sufficient condition for the protection against active re-identification attacks leveraging an arbitrary number of sybil nodes. Moreover, we show that the algorithmK-Match, originally devised for efficiently enforcing the related notion ofk-automorphism, also guaranteesk-symmetry. Empirical results on real-life and synthetic graphs demonstrate that our formulation allows, for the first time, to publish anonymised social graphs (with formal privacy guarantees) that effectively resist the strongest active re-identification attack reported in the literature, even when it leverages a large number of sybil nodes.

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems, for which we capture features and corruption models previously outside the scope of formal verification. Relying on the Tamarin protocol prover for automation, we derive new security proofs and attacks on deployed versions of these protocols, illustrating trade-offs between usability and security.

Abstract This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied $$\pi $$ π -calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so.

We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $\pi$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.

In recent years, smart contracts have suffered major exploits, cost- ing millions of dollars. Unlike traditional programs, smart contracts are deployed on a blockchain. As such, they cannot be modified once deployed. Though various tools have been proposed to detect vulnerable smart contracts, the majority fails to protect vulnera- ble contracts that have already been deployed on the blockchain. Only very few solutions have been proposed so far to tackle the issue of post-deployment. However, these solutions suffer from low precision and are not generic enough to prevent any type of attack. In this work, we introduce ÆGIS, a dynamic analysis tool that protects smart contracts from being exploited during runtime. Its capability of detecting new vulnerabilities can easily be extended through so-called attack patterns. These patterns are written in a domain-specific language that is tailored to the execution model of Ethereum smart contracts. The language enables the description of malicious control and data flows. In addition, we propose a novel mechanism to streamline and speed up the process of managing attack patterns. Patterns are voted upon and stored via a smart contract, thus leveraging the benefits of tamper-resistance and transparency provided by the blockchain. We compare ÆGIS to current state-of-the-art tools and demonstrate that our solution achieves higher precision in detecting attacks. Finally, we perform a large-scale analysis on the first 4.5 million blocks of the Ethereum blockchain, thereby confirming the occurrences of well reported and yet unreported attacks in the wild.

Abstract We present a novel method for publishing differentially private synthetic attributed graphs. Our method allows, for the first time, to publish synthetic graphs simultaneously preserving structural properties, user attributes and the community structure of the original graph. Our proposal relies on CAGM, a new community-preserving generative model for attributed graphs. We equip CAGM with efficient methods for attributed graph sampling and parameter estimation. For the latter, we introduce differentially private computation methods, which allow us to release communitypreserving synthetic attributed social graphs with a strong formal privacy guarantee. Through comprehensive experiments, we show that our new model outperforms its most relevant counterparts in synthesising differentially private attributed social graphs that preserve the community structure of the original graph, as well as degree sequences and clustering coefficients.

Today, there are millions of third-party Android applications. Some of them are buggy or even malicious. To identify such applications, novel frameworks for automated black-box testing and dynamic analysis are being developed by the Android community. Code coverage is one of the most common metrics for evaluating effectiveness of these frameworks. Furthermore, code coverage is used as a fitness function for guiding evolutionary and fuzzy testing techniques. However, there are no reliable tools for measuring fine-grained code coverage in black-box Android app testing. We present the Android Code coVerage Tool, ACVTool for short, that instruments Android apps and measures code coverage in the black-box setting at class, method and instruction granularity. ACVTool has successfully instrumented 96.9% of apps in our experiments. It introduces a negligible instrumentation time overhead, and its runtime overhead is acceptable for automated testing tools. We demonstrate practical value of ACVTool in a large-scale experiment with Sapienz, a state-of-the-art automated testing tool. Using ACVTool on the same cohort of apps, we have compared different coverage granularities applied by Sapienz in terms of the found amount of crashes. Our results show that none of the applied coverage granularities clearly outperforms others in this aspect.

Verification of cryptographic protocols is traditionally built upon the assumption that participants have not revealed their long-term keys. However, in some cases, participants might collude to defeat some security goals, without revealing their long-term secrets.

In order to prevent the disclosure of privacy-sensitive data, such as names and relations between users, social network graphs have to be anonymised before publication. Naive anonymisation of social network graphs often consists in deleting all identifying information of the users, while maintaining the original graph structure. Various types of attacks on naively anonymised graphs have been developed. Active attacks form a special type of such privacy attacks, in which the adversary enrols a number of fake users, often called sybils , to the social network, allowing the adversary to create unique structural patterns later used to re-identify the sybil nodes and other users after anonymisation. Several studies have shown that adding a small amount of noise to the published graph already suffices to mitigate such active attacks. Consequently, active attacks have been dubbed a negligible threat to privacy-preserving social graph publication. In this paper, we argue that these studies unveil shortcomings of specific attacks, rather than inherent problems of active attacks as a general strategy. In order to support this claim, we develop the notion of a robust active attack , which is an active attack that is resilient to small perturbations of the social network graph. We formulate the design of robust active attacks as an optimisation problem and we give definitions of robustness for different stages of the active attack strategy. Moreover, we introduce various heuristics to achieve these notions of robustness and experimentally show that the new robust attacks are considerably more resilient than the original ones, while remaining at the same level of feasibility.

Social network data is typically made available in a graph format, where users and their relations are represented by vertices and edges, respectively. In doing so, social graphs need to be anonymised to resist various privacy attacks. Among these, the so-called active attacks, where an adversary has the ability to enrol sybil accounts in the social network, have proven difficult to counteract. In this article, we provide an anonymisation technique that successfully thwarts active attacks while causing low structural perturbation. We achieve this goal by introducing $$(k, \Gamma _{G,\ell })$$ -adjacency anonymity: a privacy property based on $$(k,\ell )$$ -anonymity that alleviates the computational burden suffered by anonymisation algorithms based on $$(k,\ell )$$ -anonymity and relaxes some of its assumptions on the adversary capabilities. We show that the proposed method is efficient and establish tight bounds on the number of modifications that it performs on the original graph. Experimental results on real-life and randomly generated graphs show that when compared to methods based on $$(k,\ell )$$ -anonymity, the new method continues to provide protection from equally capable active attackers while introducing a much smaller number of changes in the graph structure.

Distance-bounding protocols are cryptographic protocols that securely establish an upper bound on the physical distance between the participants. Existing symbolic verification frameworks for distance-bounding protocols consider timestamps and the location of agents. In this work we introduce a causality-based characterization of secure distance-bounding that discards the notions of time and location. This allows us to verify the correctness of distance-bounding protocols with standard protocol verification tools. That is to say, we provide the first fully automated verification framework for distance-bounding protocols. By using our framework, we confirmed known vulnerabilities in a number of protocols and discovered unreported attacks against two recently published protocols.

Attack trees profile the sub-goals of the proponent of an attack. Attack trees have a variety of semantics depending on the kind of question posed about the attack, where questions are captured by an attribute domain. We observe that one of the most general semantics for attack trees, the multiset semantics, coincides with a semantics expressed using linear logic propositions. The semantics can be used to compare attack trees to determine whether one attack tree is a specialisation of another attack tree. Building on these observations, we propose two new semantics for an extension of attack trees named causal attack trees. Such attack trees are extended with an operator capturing the causal order of sub-goals in an attack. These two semantics extend the multiset semantics to sets of series-parallel graphs closed under certain graph homomorphisms, where each semantics respects a class of attribute domains. We define a sound logical system with respect to each of these semantics, by using a recently introduced extension of linear logic, called MAV, featuring a non-commutative operator. The non-commutative operator models causal dependencies in causal attack trees. Similarly to linear logic for attack trees, implication defines a decidable preorder for specialising causal attack trees that soundly respects a class of attribute domains.

Distance-bounding protocols serve to thwart various types of proximity-based attacks, such as relay attacks. A particular class of distance-bounding protocols measures round trip times of a series of one-bit challenge-response cycles, during which the proving party must have minimal computational overhead. This can be achieved by precomputing the responses to the various possible challenges. In this paper we study this class of precomputation-based distance-bounding protocols. By designing an abstract model for these protocols, we can study their generic properties, such as security lower bounds in relation to space complexity. Further, we develop a novel family of protocols in this class that resists well to mafia fraud attacks.

Attack–defense trees are a novel methodology for graphical security modelling and assessment. They extend the well- known formalism of attack trees by allowing nodes that represent defensive measures to appear at any level of the tree. This enlarges the modelling capabilities of attack trees and makes the new formalism suitable for representing interactions between an attacker and a defender. Our formalization supports different semantical approaches for which we provide usage scenarios. We also formalize how to quantitatively analyse attack and defense scenarios using attributes.

Through real-life experiments, it has been proved that spoofing is a practical threat to applications using the free civil service provided by Global Navigation Satellite Systems (GNSS). In this paper, we demonstrate a prototype that can verify the integrity of GNSS civil signals. By integrity we intuitively mean that civil signals originate from a GNSS satellite without having been artificially interfered with. Our prototype provides interfaces that can incorporate existing spoofing detection methods whose results are then combined into an overall evaluation of the signal's integrity, which we call integrity level. Considering the various security requirements from different applications, integrity levels can be calculated in many ways determined by their users. We also present an application scenario that deploys our prototype and offers a public central service -- localisation assurance certification. Through experiments, we successfully show that our prototype is not only effective but also efficient in practice.

Through real-life experiments, it has been proved, not only in theory but also in practice, that civil signals of Global Navigation Satellite Systems (GNSS) can be spoofed. Consequently, a number of spoofing detection techniques have been proposed to verify the integrity of GNSS signals. In this paper, we develop a novel trust framework based on subjective logic to evaluate the integrity of received GNSS civil signals. We formally define signal integrity for the first time in the framework and use it to precisely characterise different spoofing detection methods. Our framework captures the uncertainty during the inference of signal integrity which has been largely ignored or not explicitly specified in the literature. Our framework also gives rise to several natural ways to combine the outputs of various spoofing detection methods on signal integrity. We validate our framework through experiments using both real and simulated signals and the results show that our framework is effective.

With the prevalence of GNSS technologies, nowadays freely available for everyone, location-based vehicle services such as electronic tolling pricing systems and pay-as-you-drive services are rapidly growing. Because these systems collect and process travel records, if not carefully designed, they can threaten users' location privacy. Finding a secure and privacy-friendlysolution is a challenge for system designers. Besides location privacy, communication and computation overhead should be taken into account as well in order to make such systems widely adopted in practice. In this paper, we propose a new electronic toll pricing system based on group signatures. Our system preserves anonymity of users within groups, in addition to correctness and accountability. It also achieves a balance between privacy and overhead imposed upon user devices.

Wireless sensor networks with hundreds of sensor nodes have emerged in recent years as important platforms for a wide spectrum of monitoring tasks ranging from environmental to military applications. In order to support scalability and increase lifetime of these networks, sensor nodes are preferably grouped into clusters. A large number of clustering protocols have been proposed in the literature with different aims, requirements and efficiency. Previous comparative studies of such protocols were usually based on simulation, which, however, only provides average case results on the limited state space explored. To mend this situation, in this paper, we evaluate and compare four state-of-the-art clustering protocols, i.e., LEACH, GENLEACH, HEED and PANEL, with full state space exploration. Within our analytical framework that consists of a network configuration and an energy consumption model, we aim at analyzing the correctness and performance of the investigated protocols. Our analysis is conducted formally through probabilistic model checking using PRISM and has its focus on the quantitative aspects of the protocols.

Social networking sites have sprung up and become a hot issue of current society. In spite of the fact that these sites provide users with a variety of attractive features, much to users' dismay, however, they are prone to expose users' private information. In this paper, we propose an approach whi ch addresses the problem of collaboratively deciding privacy policies for, but not limited to, shared photos. Our approach utilizes trust relations in social networks and combines them with Condorcet's preferential voting scheme. We study properties of our trust-augmented voting scheme and develop two approximations to improve its efficiency. Our algorithms are compared and justified by experimental results, which support the usability of our trust-augmented voting scheme.

In voting, the notion of receipt-freeness has been proposed to express that a voter cannot gain any information to prove that she has voted in a certain way. Receipt-freeness aims to prevent vote buying, even when a voter chooses to renounce her privacy. In this paper, we distinguish various ways that a voter can communicate with the intruder to reduce her privacy and classify them according to their ability to reduce the privacy of a voter. We develop a formal framework combining knowledge reasoning and trace equivalences to formally model voting protocols and define vote privacy for the voters. Our framework is quantitative, in the sense that it defines a measure for the privacy of a voter. Therefore, the framework can precisely measure the level of privacy for a voter for each of the identified privacy classes. The quantification allows our framework to capture receipts that reduce, but not nullify, the privacy of the voter. This has not been identified and dealt with by other formal approaches.

Multi-party contract signing protocols specify how a number of signers can cooperate in achieving a fully signed contract, even in the presence of dishonest signers. This problem has been studied in different settings, yielding solutions of varying complexity. Here we assume the presence of a trusted third party that will be contacted only in case of a conflict, asynchronous communication, and a total ordering of the protocol steps. Our goal is to develop a lower bound on the number of messages in such a protocol. Using the notion of abort chaining, a specific type of attack on fairness of signing protocols, we derive the lower bound alpha^2 + 1, with alpha being the number of signers involved. We obtain the lower bound by relating the problem of developing fair signing protocols to the open combinatorial problem of finding shortest permutation sequences. This relation also indicates a way to construct signing protocols which are shorter than state-of-the-art protocols. We illustrate our approach by presenting the shortest three-party fair contract signing protocol.

Healthcare requires a new approach with respect to the secure management of information. For this purpose we extend the Role Based Access Control model with exceptions, context awareness, and delegation. By combining this extended model with common notions from the field of Enterprise/Digital Rights Management we obtain a framework for controlling shared information in a distributed environment.

Studies have shown significant benefits of the use of Domain-Specific Languages (DSL) in software engineering. We discuss a software engineering methodology that fully exploits these benefits. The methodology, called the Language-Driven Approach (LDA), is centred around the design of a DSL. It prescribes a staged development of a DSL, which is tailored to the system-under-construction. On the basis of a domain analysis, a formal definition of the problem is obtained. This formal problem definition contains all the relevant ingredients for designing the syntax, the semantics and the pragmatics, which together comprise the DSL. The methodology is illustrated by an elaborate example dealing with the problem of regulating traffic lights at a traffic junction.

Message Sequence Charts are a widely used technique for the visualization of the communications between system components. We present a formal semantics of Basic Message Sequence Charts, exploiting techniques from process algebra. This semantics is based on the semantics of the full language as being proposed for standardization in the International Telecommunication Union.