Search

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., ProFuN, UPMARC

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.

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., ProFuN, UPMARC

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., ProFuN, WISENET

WISENET

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., ProFun, WISENET

WISENET

WISENET

WISENET

In the LEAP framework for wireless sensor networks a set of keys is used to secure communication. LEAP distinguishes between unicast (pairwise) communication, group (cluster) communication and global (broadcast) communication. The keys used in pairwise communication are derived from an initial key KI that nodes are equipped with prior to deployment and that is deleted after link setup. Further keys are distributed encrypted with these pairwise keys. If the initial key is ever disclosed, the whole network is compromised. To lower the threat of KI disclosure, we present a novel KI -less scheme for key predistribution. Our scheme is based on random key redistribution, and proves to perform better in medium sized networks than previous proposals. It is resilient against node capture attacks and allows node to node authentication. Attacks against overlying protocols in the network are more difficult with this scheme. We have conducted computations to show the feasibility of our scheme for networks up to a size of 1000 nodes. By introducing a key reuse system we are able to increase the probability of a successful link setup. We have included a security analysis that discusses our scheme’s resistance against commonly known attacks., WISENET

We present a protocol for query authentication in a sensor network where there is multi-hop communication and the queries are broadcasted by the base station into the network. Authenticating the queries is important so attackers cannot modify existing queries because this would lead to wrong readings; or insert new ones into the network because this would lead to waste of energy. We propose a layered query authentication protocol that ensures that, in the presence of less than n captured nodes, unauthorized queries are stopped after a small number of hops. When more than n nodes are captured, the unauthorized queries will only spread in one direction with a limited angle. Message authentication codes (MACs) are used to protect the authenticity and integrity of the query. n MACs are attached to the query message at the base station and the nodes replace MACs from this message in an interleaved manner., WISENET