- Speaker: Mohammad Torabi Dashti
- Title: Super-strings and multi-party contract signing
Problems related to scattered/consecutive super string of a set of
strings are reviewed. A number of these (open) problems have direct
applications in designing and verifying efficient multi-party contract
signing protocols. Some tentative ways to approach these problems are
- Speaker: Chenyi Zhang
- Title: Information Flow in Systems with Schedulers
The focus of work on information flow security has primarily
been on definitions of security in asynchronous systems models. This
work considers systems with schedulers, which require synchronous
variants of these definitions. In particular, it studies the
dependence of these variant definitions of security on implementation
details of the scheduler. Such independence is shown to hold for
synchronous variants of trace-based definitions, but
not for bisimulation-based definitions.
- Speaker: Peter Ryan
- Title: Pret a Voter a la Florentina
- Abstract: Pret a Voter 2006 uses re-encryption mixes and cyclic
shifts of the
candidate order. This is a little fragile in that an adversary has a
systematic way to shift votes. I show how we can introduce the
idea of Florentine squares to enrich the set of permutations that can be
handled and counter the vote shifting attack.
- Speaker: Gerardo and Pim
- Midterm presentation of Master's thesis work
- Speaker: Barbara Kordy
- Title: A Rewrite Approach for Tree Pattern Containment
XPath is a language for navigating an XML tree and selecting a set of
Due to the wide use of XPath, which is embedded into several
languages for querying
and manipulating XML documents, the problem of efficiently answering
has received an increasing attention from the research community. The
for the evaluation of an XPath query depends on its size, thus the
possibility of replacing
a given query by an equivalent one having the smallest size is
essential form the point
of view of complexity. On the other hand, query equivalence is simply
two-way query containment.
In this talk, we focus on a class of purely descendant XPath queries
modeled with tree patterns.
We propose to handle the query containment problem by using a rewrite
We introduce a system of rewrite rules based on the semantics of
and show that for any two queries P and Q, P is contained in Q if and
only if the pattern
representing P can be rewritten to the pattern representing Q using
This provides a new algebraic characterization of the query
Moreover, such a rewrite view gives us a uniform framework to treat
also other problems,
for instance query evaluation.
- Speaker: Ton van Deursen
- Title: Undecidability of checking security protocols
Security protocols are difficult to design and to verify for a variety
of reasons. One of the reasons is that the security problem,
i.e. deciding whether there exists an attack on a protocol, is
undecidable. However, placing restrictions on (the size and structure
of) protocols and protocol analysis may lead to decidable classes of
security protocols, allowing automation of protocol verification. It
is therefore important to find which classes of restrictions lead to
decidability of the security problem.
In this talk, I will present an undecidability result obtained by
Kuesters and Truderung. They adopt the Dolev-Yao model of protocol
execution, and prove that extending it with XOR leads to
undecidability of the security problem. I will conclude by presenting
related work with respect to (un)decidability of security protocols.
- Speaker: Xihui, Xin, and Ying
- Midterm presentation of Master's thesis work
- Speaker: Hugo Jonker
- Title: Nuovo DRM: Introducing Fair Exchange in DRM
- Abstract: We introduce Nuovo DRM, a digital rights management scheme aimed to provide formal and practical security. The scheme is based on a recent DRM scheme, which we formally specify in the mCRL process algebraic language. The original scheme stated the following security requirements: effectiveness, secrecy and resistance of content masquerading. We formalise these security requirements as well as strong fairness and formally check the original scheme against these requirements. This verification step uncovered several security weaknesses, which are addressed by Nuovo DRM. In addition to that, Nuovo DRM introduces several procedural practices to enhance the practical security of the scheme. A finite model of Nuovo DRM is subsequently model checked and shown to satisfy its design requirements, including secrecy, fairness and resistance to content masquerading.
- Speaker: Chenyi Zhang
- Title: How to Work with Honest but Curious Judges?
this talk presents an ongoing work about implementing a majority
with respect to anonymity. The protocol describes how to let 3 judges
cast their vote -- such that the final verdict is guilty if and only
if at least
2 vote for guilty, and in most cases each judge has no knowledge about
the other two's votes.
- Speaker: Sasa Radomirovic
- Title: More on honest, but curious, judges
I will discuss several solutions to the judges problem
introduces last week by Chenyi.
- Speaker: Baptiste Alcalde
- Title: Model-driven Fuzzing
In this talk, I will discuss under which conditions and how to use
common testing techniques in the
context of fuzz security testing.
- Speaker: Hongyang Qu
- Title: MCMAS: A model checker for the verification of multi-agent systems
We present MCMAS, a symbolic model checker specifically tailored for
agent-based specifications and scenarios. MCMAS supports specifications
based on Computational Tree Logic (CTL), epistemic logic (including
operators of common and explicit knowledge), Alternating Time Logic
and deontic modalities for correctness. The model input language
variables and basic types and it implements the semantics of interpreted
systems thereby naturally supporting the modularity present in agent-
systems. MCMAS implements Ordered Binary Decision Diagram (OBDD)-based
algorithms optimised for interpreted systems and supports fairness,
counter-example generation, and interactive execution (both in
symbolic mode). It has been tested in a variety of scenarios including
web-services, diagnosis and security. MCMAS comes with a GUI aimed at
assisting the verification process.
- Speaker: Osman Akcatepe
- Title: Polarization Mode Dispersion and Chromatic Dispersion in Quantum Cryptography
1. A short introduction to Quantum Cryptography
2. Some physical terms, definitions,...etc. relating the presentation.
3. Chromatic Dispersion
4. Polarization Mode Dispersion
5. Comparison of Chromatic Dispersion and Polarization Mode Dispersion
- Speaker: Sasa Radomirovic
- Title: Wallets
This talk is related to a question originally posed by Jan Bergstra.
Consider three persons with a certain number of Euro coins in their
wallets. Suppose they want to exchange some of their coins such that
after the exchange everybody has the same amount of money he or she
had before the exchange, but different coins. Can each such exchange
be achieved through a series of pairwise exchanges? If not, what is
the smallest example of an exchange that requires that all three
persons simultaneously exchange coins?
I will answer one of these questions and pose several open questions
related to this problem.
- Speaker: Pim Vullers
- Title: Secure Ownership and Ownership Transfer in RFID Systems
I will present a verification framework for ownership related
security requirements as well as two ownership transfer protocols
designed with these requirements in mind.
- Speaker: Patrick Schweitzer
- Title: Accelerating Average Consensus - Weight Choosing with the Symprio Algorithm
The talk will be about distributed (e.g. local) algorithms which aim to
reach a consensus in a wireless sensor network. One of the possible aims
of these algorithms is to reach the average of sensor measurements in
all sensors at the same time. The talk will be based upon my diploma
thesis which first surveys state-of-the-art average consensus algorithms
and then improves upon a special type of algorithm: the linear weight
adjustment (LWA) algorithms. These LWA-algorithms will be explained
using the basic Metropolis-Weights algorithm. After that the
acceleration given by the linear weight choosing using Symprio weights
will be explained and numerically shown.
- Speaker: Delphine Longuet
- Title: Testing from Logical Specifications: Proof-guided Test Selection
Testing is one of the most used method for the validation of
software. When the implementation of the system under test is not
known, the test cases to submit to the system can be selected and
generated from a formal specification. Classically, logical
(algebraic) specifications are used to test functional aspects of
programs (data) while transition systems are used to test the dynamic
and reactive behaviour of systems (actions and communications).
I will first introduce the framework for testing from algebraic
specifications, in particular the test case selection method called
axiom unfolding. The principle of this method is to use proof
techniques to guide the selection of test cases, which are built as
derivations of the specification axioms. I will then show how this
framework can be adapted and extended to first-order modal
specifications, in order to provide a logical framework for testing
the dynamic and reactive behavior of systems.
- Speaker: Ben Smyth
- Title: Automated reasoning for election verifiability in electronic voting protocol
I will present the first definition of election verifiability for
electronic voting protocols. The definition is presented in terms of
reachability assertions using the applied pi calculus and is amenable to
automation using ProVerif. The definition allows sufficient voter
capabilities to be established for election verifiability when using
hostile computer systems. More precisely the voter is assumed to vote
using Satan's computer. This paradigm also provides a benchmarking tool
to compare the degree of election verifiability offered by protocols.
The applicability of our methodology is demonstrated by analysing the
protocols due to Fujioka, Okamoto & Ohta and Juels, Catalano &
- Speaker: Tim Muller
- Title: The Expressivity of Kleene star in Process Algebras with the Empty Process
Let BPA*0, PA*0 and ACP*0 be the process algebras Basic Process
Algebra, Process Algebra and Algebra of Communicating Processes
extended with the Kleene star (*) and deadlocking (0). Bergstra,
Bethke and Ponse proved in 1994 that BPA*0 is less expressive than
PA*0, and that PA*0 is less expressive than ACP*0.
We further extend BPA*0, PA*0 and ACP*0 to BPA*0,1, PA*0,1 and
ACP*0,1 by addition of the empty process (1). We will derive that
BPA*0,1 is less expressive than PA*0,1, and that PA*0,1 is less
expressive than ACP*0,1.
- Speaker: Ying Zhang
- Title: Game-Based Verification of Multi-Party Contract Signing Protocols
- Abstract: A multi-party contract signing (MPCS) protocol is used for
a number 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
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 clarify Mauw, Radomirovic and Torabi Dashti's methodology
of designing MRT protocols using minimal message sequences.
We design a number of MRT protocols for 3 and 4 signers
according to the clarified methodology and verify all of them in Mocha.
We detect a flaw against abuse-freeness in MRT protocols
and give a simple fix.
- Speaker: Xihui Chen
- Title: Improving automatic verification of security protocols with XOR
Kusters 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 well in verifying
secrecy for a
large class of protocols, for verification of authentication
properties the class gets smaller and moreover, the verification is
In this thesis, we improve the work by Kusters 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.
- Speaker: An Xin
- Title: Model Checking Round-Based Distributed Algorithms
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 thesis, we present a general idea of
investigating the relations 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 (fully) automatic verification of these algorithms
We apply this idea to several algorithms
(including a new proposed algorithm in the thesis) and
verify the correctness of them by using model checker Spin.
- Speaker: Graham Steel
- Title: Formal Analysis of Security APIs
A security API is the interface between a trusted component, such as a
smartcard or tamper-resistant cryptoprocessor, and an untrusted
component, such as a desktop PC. Such APIs are designed so that no
matter what sequence of commands the untrusted component sends,
certain security properties, such as secrecy of sensitive keys, will
continue to hold. Over the last few years many attacks on such APIs
have been found. Our recent research has involved applying methods for
formal security analysis to security APIs. This talk will
discuss attacks, our analysis approach, the results, and the
- Speaker: Barbara Kordy
- Title: Verifying Security Protocols using Term Rewriting Techniques
The talk will give an introduction to how term rewriting techniques
are used in the verification of security protocols. It is based on a
paper by Jacquemard, Rusinowitch, and Vignerone.
- Speaker: Robert Carter
- Title: Location Aware Multifactor Authentication
Global Navigation Satellites Systems (GNSS) such as GPS are used in
security systems to provide firstly a further authentication factor to
existing and future transaction based systems. Secondly, GNSS is used
for establishing if the place of the transaction matches with the
position of an electronic mobile device associated with the authorised
person at the time of the transaction to enable the secure
authentication of the transaction.
Furthermore a unique identifiable code or device DNA is sequenced from
the device's embedded hardware and communication characteristics and
combined with GNSS data to ensure the integrity of the device.
These systems can be used in various domains but hitherto has been
applied for use in credit card transaction processing. Herein the device
switches a credit card into a ?transaction enabled? mode and during such
state the location of the device can be established and compared to the
location from where the request originates. This, in addition, needs to
correspond with the place where the merchant is entitled to accept such
card as well.
This application a.k.a IPAYMO has won several awards and is currently
part of the ESA Technology Transfer Programme and is incubated in ESA?s
technology centre in Darmstadt (DE). It is partly funded through the
Luxembourg Industrial Incentive Fund (LIIS) and by an industrial
partner. A demonstrator is being built as part of the incubation project
with the assistance of satellite navigation experts from ESOC, the ESA
Space Operation Centre in Darmstadt.
- Speaker: Patrick Schweitzer
- Title: On Attack / Defense Trees
When modeling attacks on systems, the intuitive solution rapidly
becomes infeasible. Hence there is a need for computer support, which
requires a mathematical framework. We present one of the current
approaches: "Attack Trees."
We explain why there is a need for further expansion.
For this expansion, the Attack / Defense Trees, we define a structure,
give semantics, and deduce transformation rules to obtain a unique
normal form. Then we outline the current difficulties in streamlining
- Speaker: Sjouke Mauw
- Title: Secret Santa protocols
Secret Santa is a traditional event which is known in many western
countries under different names (Chris Kindle, Kris Kringle,
Sinterklaassurprises). In this tradition members of a group are
randomly assigned other members to whom they anonymously give a gift.
A short literature study indicates that this problem has not been
studied before in security protocol literature. In my talk I will
propose a definition of the Secret Santa problem and I will sketch
some solution directions. The purpose of the presentation will not be
to answer questions but to initiate a discussion on possible
- Speaker: Gabriele Lenzini
- Title: Trust-Enhanced Security: Applying Trust Management in Systems'
In this talk we discuss, helped by a few examples, how trust
management concepts can be used in the design of systems and of their
security features. After recalling the basic structure of a general
trust management solution, we will discuss an instance of it in the
design of a middleware for a high level of security-assurance in
embedded, component-based, devices. In the same time we recall a few
concepts utilized in measuring software components' trustworthiness
using Subjective Logic. In a second part we discuss an application of
trust management in the design of an infrastructure for context-
awareness. Here, trust measurement is the base of an evaluation of
the belief that the system has in the presence of an identity in a
certain location. This engine brings to the realization of a trust-
based indoor localization system and, potentially, to a location-
aware authentication engine.
Back to SRM presenations.
For questions and comments contact Saša