Finished Student Projects

Graphical User Interface for ASSA-PBN

Student: Gary CORNELIUS
Level: Master
Supervisor: Dr. Andrzej Mizera
Duration: February — July 2015

Description: Comprehensive understanding of cellular mechanisms requires the development of efficient methods and techniques for formal modelling and analysis of real-life biological systems. In this project we concentrate on the steady-state analysis of Gene Regulatory Networks (GRNs) cast into the framework of Probabilistic Boolean Networks (PBNs). PBNs is a probabilistic generalization of the standard framework of Boolean Networks: it incorporates rule-based dependencies between genes, permits systematic study of global network dynamics, allows to cope with uncertainty, both in data and the model selection, and permits the quantification of the relative influences and sensitivities of genes in their interactions with other genes.

The dynamics of PBNs is governed by discrete-time Markov chains (DTMCs). Specifically, the dynamics of a variant of PBNs, i.e., PBNs with perturbations, is governed by an ergodic DTMC. Characterisation of the long-run behaviour of a PBN and quantification of the influences of genes on other genes are both based on the steady-state distribution of the associated DTMC. Therefore, efficient computation of steady-state probabilities is of utter importance. It is well studied how to compute the steady-state distribution of small PBNs with numerical methods. However, due to their high computational cost and memory requirements, these methods are not scalable. In the literature, a few statistical methods such as Monte Carlo methods, are proposed to deal with large PBNs.

The aim of this project is further development of ASSA-PBN, a tool for approximate steady-state analysis of large PBNs. ASSA-PBN implements numerical methods for exact analysis of small PBNs and statistical methods for approximate analysis of large PBNs. The current version supports three different statistical methods, i.e., the perfect simulation algorithm, the two-state Markov chain approach, and the Skart method. Within this project ASSA-PBN is being provided with a GUI. In particular the GUI will allow to

Keywords: Gene Regulatory Networks, Probabilistic Boolean Networks, software tool, GUI

Distance bounding protocols based on random graphs

Student: Simon BANDELLA
Level: Bachelor
Supervisors: Prof. Dr. Sjouke Mauw and Dr. Rolando Trujillo Rasúa
Duration: 17/01/2015-31/05/2015

Description: We have analysed the state-of-the art on graph based distance bounding protocols. The performed analysis shows that the fixed graph structure used by this type of protocols provides an advantage to the adversary that could be overcome by using random graphs instead. Therefore, we propose the notion of distance bounding protocols based on random graphs. The proposed protocols have been evaluated by means of a simulation tool that compare our protocol with other distance bounding protocols. The empirical results confirm the advantages of the new design.

Result: successful defense

Inferring Friendship from Check-in Data of Location-Based Social Networks

Student: Ran Cheng
Level: Master
Supervisors: Dr. Jun Pang and Yang Zhang
Duration: From February 2014 to October 2014.

Description: In recent years, the relation between human mobility and social connection attracts a lot of attention from both industry and academia. In the past, obtaining people's mobility information is considered to be an obstacle for related studies. Nowadays, however, with the ubiquity of GPS-enabled mobile devices and location-based social networking services, gaining people's spatial-temporal location information becomes easier. These spatial-temporal location information brings us opportunities to investigate on some valuable information of a particular individual, such as his interests, his visiting pattern and his real-life social connections. Particularly, this project focuses on predicting whether there exists friendship between two individuals according to their mobility information. As friends tend to visit same places, we consider the number of co-occurrences and the number of locations that two people co-occurred to be indicators of friendship. Besides, the visiting time interval between two users also has an effect on friendship prediction. By conducting machine learning technique on all the information above, we construct two friendship prediction models. The first model refers to predicting friendship of two people with only one of their co-occurred places' information. It aims at achieving an effective prediction model under the situation that only limited resources are provided. The second model proposes solution for predicting friendship of two people where all the information of their every particular co-occurred place is essential. The result shows that both models outperform the state-of-art models for location-based friendship prediction.
Keywords: Social relations, spatio-temporal data, location-based services, machine learning

Fighting Fingerprinting for Privacy

Student: Christof FERREIRA TORRES
Level: Bachelor
Supervisor: Dr. Ir. Hugo Jonker
Duration: February — May 2014

Description: Fingerprinting is a way to identify users that does not depend on client-side storage (unlike cookies, Flash cookies, etc.). Fingerprinting is used by both anti-fraud companies and advertising companies to identify users. Fingerprinting can be done passively, only based on the interaction between the client and server, or actively, using client-side scripting to uncover more information about the client. In either case, a user who browses the Internet will be open to fingerprinting by each site (s)he visits. More particularly, any site that incorporates content from another site -- such as a "share this" button -- allows the user to be tracked by this second site. The goal of this project is firstly to analyse how fingerprints are, how they work, and how they are currently used. Based on that, this project will develop a FireFox plugin that will improve privacy on the Internet.
Keywords: online privacy, FireFox, fingerprinting, tracking.

Deblurring blurred text

Student: François LANGE
Level: Bachelor
Supervisor: Dr. Ir. Hugo Jonker
Duration: February — May 2014

Description: Sensitive text (account numbers, personally identifying information, etc.) is often blurred before being published in newspapers, websites etc. In this project, we investigate to what extent such hidden information is recoverable. The project first surveys possible approaches to deblurring from literature. In addition, more "thinking out-of-the-box" approaches will be considered. Based on this survey, one approach is selected and implemented as a GIMP plugin.
Keywords: deblurring, GIMP

Evaluating Security Protocols for Enforcing Topology-based Access Control

Student: Nida Khan
Level: Master
Supervisors: Dr. Jun Pang and Yang Zhang
Duration: From November 2013 to February 2014.

Description: Large quantity of data in online social networks (OSNs), such Facebook and Google+, give rises to privacy concerns for their users. Access control is one of the most straightforward ways to address this challenge. Relationship-based access control schemes have been proposed in recent years to protect users' privacy in social networks. In such schemes, whether a user can view another one's information depends on the relationship between them. Recently, we have proposed cryptographic protocols to enforce three fine-grained relationship-based access control polices which are topology-based, including k-common friends, k-depth and celebrity in decentralised social networks. These protocols are mainly built on paring-based cryptosystems. Their efficiency and security have been analysed under honest but curious as well as malicious adversary models. In this project, we focus on the performance of our proposed protocols and evaluate their computational and communication overheads through simulations on real social network topologies.
Keywords: Social networks, security protocols, access control.

DRM for Privacy

Supervisor: Dr. Ir. Hugo Jonker
Duration: From February 2013 to May 2013.

Description: Smart phones make taking and sharing photos easy. However, not all photos should be treated publicly. A photo of a wild night in a disco should be treated differently from a photo taken in broad daylight in front of a touristic sight. The goal of this project is to develop an app that enables users to share photos, while ensuring that the shared photos can only be viewed in circumstances sufficiently similar to the ones in which the picture was taken (context privacy).
Keywords: DRM, context-aware privacy, Android.

User similarity and privacy based on mobility profiles

Student: Ruipeng Lu
Level: Master
Supervisors: Dr. Jun Pang and Xihui Chen
Duration: From February 2013 to October 2013.

Description: Social networks has become an essential part of many people's everyday lives. A lot of social networks have deployed location-based services with which friends can share favorite places or outdoor activities by virtue of the increasingly ubiquitous devices that are able to acquire locations accurately. Location-based services leads social networks to a new approach of user recommendation based on the similarity of users' mobility profiles which are their frequent movement behavior extracted from their movement history. This can be done by measuring the extent of proximity between users' movement trajectories, or semantically by measuring the extent of closeness between the functionalities of places often visited by users. In this project, we propose principles that user similarity measures based on mobility profiles should follow, and identify the defects of the existing user similarity measures in the literature. We further propose three novel similarity measures, one without semantics and the other two with semantics. The experimental results on real datasets corroborate that our new similarity measures outperform the existing ones. We also develop the MinUS software tool that coalesces the mobility profile construction process and the comparison of user similarity using the existing or our new similarity measures.
Keywords: Data mining, mobility profiles, spatio-temporal trajectories, user similarity, location-based services

Multiple Antivius Engine Scanners

Student: Catalin Anton
Level: Master
Supervisor(s): Matthijs Melissen and Patrick Schweitzer
Duration: From July 2012 to January 2013.

Description: The Multiple Antivirus Engine Scanners project aims at providing a user-friendly and fast solution to the problem of diagnosing if a given file is susceptible to contain a particular malware code. The proposed system is intended as a local scanning tool. This feature will avoid the further dissemination of the targeted attack malware code, which may be possible if an online scanning tool is used. It is also presumable that if an on-line tool is used, the initiators of the attack may become aware that a targeted malware code is suspected. This will give them an opportunity to change their course of action to alternative attacks.
Keywords: Privacy, anti-virus scanners, malware.

Carving proprietary communication protocols

Students: Ana GAGGERO and Loïc GAMMAITONI
Level: Master
Supervisors: Prof. Dr. Sjouke Mauw and Dr. Ir. Hugo Jonker
Duration: From September 2012 to January 2013.

Description: The main topic of this project is the reverse-engineering of proprietary protocols. The envisioned approach will be to select a protocol for which a closed-source application is distributed to its users. An example of such protocols is the Skype protocol. By varying the input to the application and recording the traffic, traces of the system can be created. The next step is to extend current methods for analyzing these traces, in order to recover the underlying protocol. The final step is to implement these methods in an (existing) prototype.
Keywords: carving, reverse-engineering, skype, black box analysis


Student: Filipe FERREIRA
Level: Bachelor
Supervisor: Dr. Ir. Hugo Jonker
Duration: From September 2012 to December 2012.

Description: Recently, researchers found a way to leverage an iPhone's accelerometers to infer keystrokes. By leaving a phone running a special measuring app close to the keyboard, the app is able to make reasonable guesses at what the typed word is.
The goal of this project is to develop a proof-of-concept: implement this technique for an Android phone, and set up a working demonstration.
Keywords: Android, password, signal-processing.

Constructing and comparing user mobility profiles in LBS

Student: Ran Xue
Supervisor(s): Dr. Jun Pang and Xihui Chen
Level: Master
Duration: From February 2012 to October 2012.

Description: Along with the increasing availability of location-acquisition technologies such as GPS and GSM networks among others, we have better access to the collection of large spatio-temporal datasets. This brings us new opportunities in location-based services. First, using that large amount of information of spatio-temporal data, we can discover useful knowledge about users' movement behavior. Second, using the location-acquisition technologies, users can record their location histories. Such real-world location histories allow for the discovery of users' points of interests in places over time. This helps us to understand the relationships between users based on their location data. As a requirement for recommendation systems, we need to calculate a similarity score between each two users to recommend each user a list of potential friends. This project will study new methods to generate users' mobility profiles and calculate users' similarity between each other.
Keywords: Privacy, location-based services, data mining, mobility profiles, spatial trajectories.

Reverse engineering communication protocols

Student: Bianca Miniberger
Supervisor(s): Prof. Dr. Sjouke Mauw and Dr. Sasa Radomirovic
Level: Master
Duration: From October 2011 to March 2012.

Description: A notorious problem in digital forensics is the recovery of hidden, deleted, or partially destroyed data. In order to solve this problem, it is essential to know the structure, such as a file format or a protocol specification, of the data that is being reconstructed. If the structure is unknown it needs to first be reverse-engineered.
This project concerns the reverse-engineering of a protocol specification from observations of messages exchanged during the execution of a communication protocol. Its starting point is a recent paper on this topic by van Deursen, Mauw, and Radomirovic. The paper is available here.
Keywords: Digital Forensics, carving, reverse-engineering.

Implementation and validation of security checks for GNSS location assurance

Student: Daniel Marnach
Supervisor(s): Prof. Dr. Sjouke Mauw
Level: Master
Duration: From August 2011 to February 2012.

Description: Global Navigation Satellite Systems (GNSS) offer no authentication of their satellites towards their civilian users. As a consequence, two types of attacks, namely meaconing and GNSS signal spoofing, may be performed in order to falsify the computed locations.
The LASP project aims to compensate the missing authentication by introducing the Location Assurance Provider (LAP), a Trusted Third Party whose purpose it is to estimate the probability that a claimed location is correct. To do so, it runs a number of so called security checks. Each of these algorithms gets as input data sent to the LAP by one or more users, checks whether a particular condition holds, and returns its opinion on whether the analysed data is authentic.
In this project, we introduce a new security check that is based on the clock bias of receivers towards the GPS reference time. The design of this check entailed an extensive reverse engineering of the employed equipment's behaviour. The clock bias security check has been tested under laboratory conditions and looks very promising. It was possible to detect simulated meaconing attacks without having too many false positives.
Keywords: location assurance, GNSS, subjective logic, PKI.

Anonymity and privacy in electronic toll collection systems

Student: David Kamdoum
Supervisor(s): Dr. Jun Pang and Xihui Chen
Level: Master
Duration: From February 2011 to December 2011.

Description: The popularity and cheap access of localisation chips of Global Navigation Satellite Systems offers chances to upgrade Electronic Toll Pricing (ETP) Systems. Vehicles' locations are collected by the toll server automatically and used to compute drivers' tolls at the end a toll session. This brings a number of benefits to clients, providers and environment as well. However, it also causes a lot of concern of people's location privacy.
A few privacy preserving mechanisms have been proposed in last few years. We find that the attacker (adversarial server) can still learn more about users' locations with the data available in the proposed systems, for example, through statistical analysis. In this project, we want to analyse the effects of statistical analysis from the attacker's view, and analyse whether public information, e.g., home address, driving habits can be used to breach users' location privacy as well.
Keywords: location privacy, anonymity, ETP systems, metrics.

Identifying users by typing cadence

Student: Yiwen Meng
Supervisor(s): Dr. Sasa Radomirovic
Level: Master
Duration: From February 2011 to October 2011.

Description: It is well-known that most people have a unique typing rhythm. The aim of this project is to deduce, in a first step, as much information as possible about an individual from his or her typing rhythm. In a second step, given a variety of side-channel information, the aim is to deduce as much as possible about the content typed by an individual.
Keywords: Privacy, keystroke dynamics.

Evaluation of attributes on attack-defense trees

Student: Jean-Paul Weber
Supervisor(s): Dr. Barbara Kordy and Patrick Schweitzer
Level: Master
Duration: From February 2011 to October 2011.

Description: Evaluation of attributes on attack-defense trees.
Keywords: attack trees, attack-defense trees, security assessment, attributes.

Mafia attacks on RFID and NFC devices

Student: Cheng Xing
Supervisor(s): Dr. Sasa Radomirovic and Ton van Deursen
Level: Master
Duration: From February 2011 to October 2011.

Description: In this project, relay attacks on NFC smart phones are implemented. The viability of these attacks on typical NFC payment applications is studied in practice and in a formal model. Finally, countermeasures are proposed and proved correct in the formal model.

Security and reliability analysis of clustering protocols

Student: Qian Li
Supervisor(s): Dr. Jun Pang and Dr. Peter Schaffer
Level: Master
Duration: From February 2011 to October 2011.

Description: With the advances in sensor development technologies, wireless sensor networks (WSNs) are growing popular for a wide range of applications in the military and civil domains. WSNs usually comprise a mass of small, energy constrained sensor nodes with limited processing and wireless communication capabilities. Sensor nodes are often grouped into clusters which are mostly disjoint and consist of a leader, referred to as the cluster head, and member nodes. The cluster heads are usually elected in the network through local or global mechanisms. The cluster head controls the operation of its cluster.
The security and reliability aspects of clustering, or, in other words, resilience against attacks have gained modest attention so far. An attacker can have various goals ranging from reducing the efficiency of data collection performed by the sensor network to the complete disruption of operation. These attacks can be mounted by preventing the termination of the algorithm, confusing the nodes with regard to their responsibilities in the network, retracing the network structure and launching targeted attacks, etc. Such sophisticated attacks can have a larger impact than attacks against randomly chosen nodes. The goal of this project is to find, formally define and explore the key properties the fulfillment of which provides resistance against attacks of any kind.
Keywords: Security, reliability, clustering protocols, formal methods.
Note: This is a project with SnT.

Probabilistic modelling and analysis of the PDGF signalling pathway

Student: Qixia Yuan
Supervisor(s): Dr. Jun Pang
Level: Master
Duration: From February 2011 to October 2011.

One paper based on this work has been published in the proceedings of CompMod'11.
Description: Due to the similarity between biological systems and complex distributed/reactive systems studied in computer science, modeling and analysing techniques developed in the field of formal methods can be applied to biological systems as well. In this project, we apply the probabilistic model checker PRISM to the analysis of a biological system -- the Platelet-Derived Growth Factor (PDGF) signaling pathway, demonstrating in detail how this pathway can be analysed in PRISM.
Keywords: Probabilistic model checking, biological pathways, biological modelling, verification.

Extending a certified email protocol with transparent TTP and its formal verification

Student: Zhiyuan Liu
Supervisor(s): Dr. Jun Pang and Dr. Chenyi Zhang
Level: Master
Duration: From February 2010 to October 2010.

One paper based on this work has been published in the proceedings of TrustCom'10.
Another paper paper based on this work has been accepted for publication in the proceedings of TTSS'10.

Description: Cederquist et al. proposed an optimistic certified email protocol, which employs key chains to reduce the storage requirement of the trusted third party. We extend their protocol to satisfy one more property of TTP (trusted third party) transparency, using an existing verifiably encrypted signature scheme based on bilinear pairings. We are able to show, by a detailed comparison, that our extended protocol is one of the most efficient certified email protocols satisfying strong fairness, timeliness, effectiveness and TTP transparency.
We analyse the extended protocol using the technique of automatic formal verification. The finite-state model checker Mocha is adopted to verify the properties of fairness, timeliness and effectiveness. The toolset mCRL is used to verify the property of TTP transparency.
Keywords: Certified email protocols, TTP transparency, fairness, formal verification.

Privacy in social networking sites: A comparative study and a scheme on collaborative management

Student: Yanjie Sun
Supervisor(s): Dr. Jun Pang
Level: Master
Duration: From February 2010 to October 2010.

A paper based on this work has been accepted to be published in the proceedings of STM'10.

Description: Social networks have sprung up and become a hot issue of current society. In spite of the fact that these networks provide users with a variety of attractive features, much to users' dismay, however, they are likely to expose uses' private information.
In this thesis, we conduct a full-fledged privacy exploration on six typical social networking sites. Our study mainly revolves around the life cycle of users' private data, which pertains to collection, procession, retention and deletion. An exhaustive comparative analysis has been undertaken to reveal a wide range of privacy risks.
To address the privacy problem incurred by resource sharing, we propose an approach which adopts collaborative management to obtain a joint decision reflecting the "general will". Our proposed algorithm utilizes trust relations in social networks and combines it with the Condorcet preferential voting scheme. An optimization is further developed to improve its efficiency. Considering users might feel bored in the case of large number of sharing resources, an inference technique is introduced to relieve user from the burden of massive manual input.
Keywords: Privacy, Condorcet voting, social networking.

Game-based verification of multi-party contract signing protocols

Student: Ying Zhang
Supervisor(s): Dr. Jun Pang and Dr. Chenyi Zhang
Level: Master
Duration: From February 2009 to October 2009.

A paper based on this work has been published in the proceedings of FAST'09.

Description: A multi-party contract signing (MPCS) protocol is used for a group of signers to sign a digital contract over a network. We analyse the protocols of Mukhamedov and Ryan (MR), and of Mauw, Radomirovic and Torabi Dashti (MRT), using the finite-state model checker Mocha. Mocha allows for the specification of properties in alternating-time temporal logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives us an intuitive interpretation of the verification problem of crucial properties of MPCS protocols. We analyse the MR protocol with up to 5 signers and our analysis does not reveal any flaws. MRT protocols can be generated from minimal message sequences, depending on the number of signers. We discover an attack in a published MRT protocol with 3 signers, and present a solution for it. We also design a number of MRT protocols using minimal message sequences for 3 and 4 signers, all of which have been model checked in Mocha.
Keywords: Model checking, contract signing protocols, fairness, Mocha.

Improving automatic verification of security protocols with XOR

Student: Xihui Chen
Supervisor(s): Dr. Jun Pang and Ton van Deursen
Level: Master
Duration: From February 2009 to October 2009.

A paper based on this work has been published in the proceedings of ICFEM'09.

Description: Küsters and Truderung recently proposed an automatic verification method for security protocols with exclusive or (XOR). Their method reduces protocols with XOR to their XOR-free equivalents, enabling efficient verification by tools such as ProVerif. Although the proposed method works efficiently for verifying secrecy, verification of authentication properties is inefficient and sometimes impossible.
In this paper, we improve the work by Küsters and Truderung in two ways. First, we extend their method for authentication verification to a richer class of XOR-protocols by automatically introducing bounded verification. Second, we improve the efficiency of their approach by developing a number of dedicated optimizations. We show the applicability of our work by implementing a prototype and applying it to both existing benchmarks and RFID protocols. The experiments show promising results and uncover a flaw in a recently proposed RFID protocol.
Keywords: Formal verification, security protocols, exclusive or, ProVerif.

Model checking round-based distributed algorithms

Student: Xin An
Supervisor(s): Dr. Jun Pang
Level: Master
Duration: From February 2009 to October 2009.

A paper based on this work has been published in the proceedings of ICECCS'10.

Description: In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking.
In this paper, we present a general idea of investigating the bounded distance of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make automatic verification of these algorithms possible. We apply this idea to several algorithms and present their verification results in the model checker Spin.
Keywords: Model checking, distributed algorithms, model transformation, Spin.

Secure ownership and ownership transfer in RFID systems

Student: Pim Vullers
Supervisor(s): Dr. Sasa Radomirovic and Ton van Deursen
Level: Master
Duration: From January 2009 to July 2009.

A paper based on this work has been accepted and published in the proceedings of ESORICS'09.

Description: We present a formal model for stateful security protocols. This model is used to define ownership and ownership transfer as concepts as well as security properties. These definitions are based on an intuitive notion of ownership related to physical ownership. They are aimed at RFID systems, but should be applicable to any scenario sharing the same intuition of ownership. We discuss the connection between ownership and the notion of desynchronization resistance and give the first formal definition of the latter. We apply our definitions to existing RFID protocols, exhibiting attacks on desynchronization resistance, secure ownership, and secure ownership transfer.
Keywords: RFID protocols, ownership, desynchronization resistance, ownership transfer, formal verification.

Design of an attack-tree creation tool

Student: Carlo Wampach
Level: Bachelor
Duration: From March 2008 to June 2008.

Compositionality of security protocols

Student: Pieter Ceelen
Level: Master
Duration: From April 2007 to July 2007.

A paper based on this work has been accepted and published in the proceedings of STM'07.