Logo: to the web site of Uppsala University

Psi-calculi is a parametric framework for extensions of the pi-calculus with arbitrary data and logic. All instances of the framework inherit machine-checked proofs of the metatheory such as compositionality and bisimulation congruence. We present a generic analysis tool for psi-calculus instances, enabling symbolic execution and (bi)simulation checking for both unicast and broadcast communication. The tool also provides a library for implementing new psi-calculus instances. We provide examples from traditional communication protocols and wireless sensor networks. We also describe the theoretical foundations of the tool, including an improved symbolic operational semantics, with additional support for scoped broadcast communication.

High-level formalisms for concurrency are often defined as extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms. Psi-calculi is a parametric framework that can accommodate a wide spectrum of such calculi. It allows the definition of process calculi that extend the pi-calculus with arbitrary data, logic and logical assertions. All such psi calculi inherit machine-checked proofs of the meta-theory such as compositionality and bisimulation congruence.

We present a generic tool for analysing processes from any psi calculus instance, and for implementing new instances with the help of a supporting library. The tool implements symbolic execution and bisimulation algorithms for both unicast and wireless broadcast communication. We illustrate the tool by examples from pi-calculus and the area of wireless sensor networks.

We explore two applications of negative premises to increase the expressive power of psi-calculi: reliable broadcasts and priorities. Together, these can be used to model discrete time, which we illustrate with an example from automotive applications. The negative premises can be encoded by a two-level structural operational semantics without negative premises; we use this fact to prove the standard congruence and structural laws of bisimulation with Nominal Isabelle.

Participatory sensing applications typically bind sensor data to locations. Location privacy preserving mechanisms protecting the location of users introduce therefore an uncertainty in the collected data distributions. We consider two strategies to reconstruct a data distribution after k-anonymity has been applied to the users' location information. We investigate how different parameters for the location privacy preserving mechanism influence both the quality of information and the location privacy of the users. Our results show that the cloak area resulted from applying k-anonymity has a higher impact on both the quality of information and the location privacy than the number of users, k, that are cloaked together.

A wireless sensor network is a collection of numerous sensors distributed on an area of interest to collect and process data from the environment. One particular threat in wireless sensor networks is node compromise attacks, that is, attacks where the adversary gets physical access to a node and to the programs and keying material stored on it.

Only authorized queries should be allowed in the network and the integrity and confidentiality of the data that is being collected should be protected. We propose a layered key distribution scheme together with two protocols for query authentication and confidential data aggregation. The layered key distribution is more robust to node and communication failures than a predefined tree structure. The protocols are secure under the assumption that less than n sensor nodes are compromised. n is a design parameter that allows us to trade off security for overhead. When more than n sensor nodes are compromised, our simulations show that the attacker can only introduce unauthorized queries into a limited part of the network and can only get access to a small part of the data that is aggregated in the network. Considering the data collection protocol we also contribute with strategies to reduce the energy consumption of an integrity preserving in-network aggregation scheme to a level below the energy consumption of a non-aggregation scheme. Our improvements reduce node congestion by a factor of three and the total communication load by 30%.

Location privacy of the users carrying mobile devices is another aspect considered in this thesis. Considering a mobile sink that collects data from the network, we propose a strategy for data collection that requires no information about the location and movement pattern of the sink. We show that it is possible to provide data collection services, while protecting the location privacy of the sink. When mobile phones with built-in sensors are used as sensor nodes, location information about where the data has been sensed can be used to trace users and infer other personal information about them, like state of health or personal preferences. Therefore, location privacy preserving mechanisms have been proposed to provide location privacy to the users. We investigate how a location privacy preserving mechanism influences the quality of the collected data and consider strategies to reconstruct the data distribution without compromising location privacy.

We propose two strategies to reduce energy consumption for secure data aggregation in wireless sensor networks. While the purpose of data aggregation is to reduce energy consumption, secure data aggregation introduces an overhead making the total energy consumption comparable to naive secure non-aggregation. Another aspect is that the secure data aggregation has higher node congestion than non-aggregation schemes for networks of sizes up to about 100 nodes. Considering a secure data aggregation protocol, our strategies are to reduce the height of the aggregation tree and limit its node degree. The former results in fewer verification messages and a lower total communication load, and the latter reduces node congestion. The most heavily burdened node sends a third of the messages required in the original protocol, which for small networks is lower than with non-aggregation, and the total communication load is lowered compared to non-aggregation.