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
- open, save, import, and export PBN models;
- generate a PBN model complying with a provided specification;
- simulate a PBN;
- perform the computation of steady-state probability for a specified set of states with available methods;
- visualise the PBN structure;
- compute the long-term influence of a specified gene on a given target gene.
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 JonkerDuration: 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.
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.
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
SpyDroid
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.
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.
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.
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.
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.
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.
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.
Keywords:.
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.
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.
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.
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.
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.
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.
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.
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.
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.