SRM seminar
Abstracts 2010
- Speaker: Jan Willemson
- Title: Attack Trees. Models and Computation
- Abstract: Structured methods for threat analysis have been used for several decades already. However, there are many scenarios, where mere descriptive approach is insufficient and it is necessary to take economically justified decisions concerning possible defence strategies. In the talk we will cover several recently proposed models for quantitative attack tree analysis and discuss the corresponding computational details.
- Speaker: Martin Caminada
- Title: Attack and Defense in Formal Argumentation
- Abstract: In this talk, we will treat the basics of abstract argumentation theory in order to examine to which extent it is applicable to reasoning about security. In abstract argumentation theory, one assumes a graph in which the nodes correspond with arguments and the arrows correspond with an attack relation. We say that an argument A attacks an argument B iff there exists an arrow from A to B. We say that a set of arguments is admissible ("potentially safe") iff no two arguments in this set attack each other, and for all arguments outside the set that attack an argument in the set, the set contains an argument that "strikes back" (that attacks the attacker). Based on the concept of admissibility, we can then formulate various other principles under which a set of arguments can be accepted. Although this theory was originally developed in the context of formalised argumentation, it is essentially a general theory about how to deal with conflicting entities. That is, how to find "reasonable" or "safe" sets of entities in the presence of conflicts?
- Speaker: Hugo Jonker
- Title: Quantifying voter-controlled privacy
- Abstract: Privacy is a necessary requirement for voting. Without privacy, voters can be forced to vote in specific ways, and the forcing party can check their compliance. But offering privacy does not suffice: if a voter can reduce her privacy, an attacker can force her to do so. We introduce the notion of choice groups as a measure of privacy, and provide formal definitions. We illustrate how this notion can be used to better understand privacy concerns in voting systems, and how the notion of choice groups is formalised to quantify privacy. By combining this with models of various degrees of voter collaboration, we can quantify the privacy under a voter's control.
- Speaker: Georgios Pitsilis
- Title: Trust for recommender systems, Current Achievements and Concepts for Exploration.
- Abstract: This presentation is a mix of survey of previous works in the area of Trust & recommender systems and personal achievements in that area. The latter includes analysis of social networks and evaluation of concepts using the subjective logic as a tool. Trust derivation and the cold-start problem have also been in the focus of the current work. Performance evaluation results are analyzed and compared with baseline techniques. There is also mention to other interesting topics such as the use of trust models in information retrieval. Potential issues and prospective solutions suitable for Recommender Systems and Automatic Annotation of content are briefly presented. Research progress and future directions are also discussed.
- Speaker: Matthijs Melissen
- Title: Games with secure equilibria
- Abstract: (This talk is a review of the paper by Krishnendu Chatterjee, Thomas A. Henzinger and Marcin Jurdzinski.) In 2-player non-zero-sum games, Nash equilibria capture the options for rational behaviour if each player attempts to maximize his payoff. A Nash equilibrium is secure if any rational deviation of player 2 - i.e. a deviation that does not decrease her pay-off - does not damage player 1. It is proven that in graph games with Borel winning conditions, which include the games that arise in verification, there may be several Nash equilibria, but there is always a unique maximal payoff profile of a secure equilibirum.
- Speaker: Baptiste Alcalde
- Title: Trusted Third Parties (TTPs)
- Abstract: In this presentation, we will solve ambiguities around the definition of TTPs, and we will show how to choose TTPs in various settings. This will be done using common sense, formulas, game theory, and your presence at the talk.
- Speaker: Chenyi Zhang
- Title: On Synchronous Notions of Information Flow Security
- Abstract: This talk presents part of the work to appear in FoSSaCS 2010. In the first part of the talk we introduce a number of information flow security properties in a synchronous state-based model, with basic intuitions on confidentiality in such systems --- how information is forbidden to flow from H to L. In the second part we characterize the computational complexities of these notions, with a focus on Nondeducibility on Strategies, which can be regarded as a game between the user H and the system. The lower bound complexity of this property is reduced from Blind-PEEK, a game of incomplete information due to Reif as an extension of the PEEK game of Stockmeyer and Chandra. Such games are universal to different versions of alternating Turing machines.
- Speaker: Cas Cremers
- Title: Modeling and Analyzing Security in the Presence of Compromising Adversaries
- Abstract:
We present a framework for modeling adversaries in security protocol
analysis, in which we define a hierarchy of adversary models. These
models range from a Dolev-Yao style adversary to more powerful
adversaries who can reveal different parts of principals' states during
protocol execution. Our adversary models unify and generalize many
existing security notions from both the computational and symbolic
settings and lead to new, previously unexplored security notions.
We extend an existing symbolic protocol-verification tool with our adversary models. This is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In extensive case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.
Joint work with David Basin
- Speaker: Naipeng Dong
- Title: An Introduction to the Applied Pi Calculus - Part I
- Abstract: In this talk, I am going to introduce the applied pi calculus, a language for describing and analyzing security protocols. I'll present its syntax, operational semantics, and how to model secrete properties, like secrecy and authentication.
- Speaker: Guillaume Aucher
- Title: Privacy policies with dynamic logic
- Abstract: Privacy policies are often defined in terms of permitted messages. Instead, in this talk we derive dynamically the permitted messages from static privacy policies defined in terms of permitted and obligatory knowledge. With this new approach, we do not have to specify the permissions and prohibitions of all message combinations explicitly. To specify and reason about such privacy policies, we extend a multi-modal logic introduced by Cuppens and Demolombe with update operators modeling the dynamics of both knowledge and privacy policies. We show also how to determine the obligatory messages, how to express epistemic norms, and how to check whether a situation is compliant with respect to a privacy policy. We axiomatize and prove the decidability of the modal logic.
- Speaker: Ton van Deursen and Sasa Radomirovic
- Title: Privacy of RFID protocols
- Abstract: This will be a whiteboard presentation on ongoing research. We will describe a series of attacks on the untraceability property of RFID protocols.
- Speaker: Tom Chothia
- Title: A Traceability Attack Against e-Passports
- Abstract: Since 2004 many nations have started issuing ``e-passports''
containing an RFID tag that broadcasts information. It is claimed that
this will make passports more secure and that our data will be
protected from any possible unauthorised attempts to read it. In this
talk we show that there is a flaw in one of the passport's protocols
that makes it possible to trace the movements of a particular
passport, without having to break the passport's cryptographic key.
All an attacker has to do is to record one session between the
passport and a legitimate reader, then by replaying a particular
message, the attacker can distinguish that passport from any other. We
have implemented our attack and tested it successfully against
passports issued by a range of nations.
This was joint work with Vitaliy Smirnov.
- Speaker: Richard Clayton
- Title: What might eCrime research look like in Luxembourg?
- Abstract: This talk discusses the possibilities for academic research in eCrime by researchers at the University of Luxembourg. It explains the problems that can be realistically tackled, the type of infrastructure needed, the sources of data and some of the ethical issues that might arise.
- Speaker: Zhiyuan Liu
- Title: Modeling and analysis of a certified email protocol
- Abstract: Certified email protocols enhance traditional email services with digitally signed receipts of both the senders and receivers. In this work we analyze a certified email protocol with key chains by using finite-state model checker Mocha. Mocha allows for specification of properties in alternating-time temporal logic(ATL), which can be easily used to describe useful properties such as fairness and timeliness. Our analysis detected a few weakness in this protocol. We also show that the protocol can be further simplified, so that the new protocol has fewer communications, without hampering the security properties that hold in the original protocol.
- Speaker: Zhe Xia
- Title: Pret a Voter for the UK elections
- Abstract: Over the past few years, a number of end-to-end verifiable election schemes have been introduced. In these schemes, it can be verified that the election result has been correctly generated, and this will not reveal how a voter has voted, even if this voter wishes to sell her vote. However, most of these schemes are only designed for First-Past-The-Post (FPTP) elections in which voters simply put a "cross" next to his preferred candidate. There are also a number of other election methods which are widely used nowadays. For example, the ordinary UK voters may face FPTP, approval voting, Single Transferable Vote (STV) and supplementary voting in the UK government elections, as well as Instant Run-off Voting (IRV) and Condorcet voting in some other non-political elections. There lacks a generic end-to-end voting solution which handles all these election methods using consistent user interface. In this talk, we introduce such a scheme which ensures that not only the voter experience remains simple and consistent in various election methods, but also the election result will always be generated in the most efficient manner.
- Speaker: Yanjie Sun
- Title: Privacy Enhancement through Collaboration in Social Networks
- Abstract: In the last decade, social networking sites have sprung up and become a hot issue of current society. In spite of the fact that these sites provide users with a variety of attractive features, much to users' dismay however, they are likely to expose users' privacy. In this paper, we propose a collaborative approach which is intended for, but not limited to, address the problem of photo sharing. Simulating this process into voting mechanism, we put forward a voting algorithm which always can generate the only result. In particular, subsequent experiment data shows that this algorithm also tends to produce the best result. Additionally, an inference technique is introduced in order to relieve the users from the burden of manually inputing privacy preference for each picture.
- Speaker: Selwyn Piramuthu
- Title: Input Data with Sequential Bias in Recommender Systems
- Abstract: Recommender systems generally generate recommendations based on past consumer (purchase or consumption) behavior. These systems use either past customer transaction data or online reviews written by customers or both. Current advances in information technology/systems and the concomitant increase in demand from customers for better recommendations necessitate the use of richer input data. Online customer reviews are a rich source for such data. Online customer reviews are also inherently biased due to the sequence in which they are written and perused. We consider sequential bias in online reviews from a recommender system's perspective.
- Speaker: Shishir Nagaraja
- Title: Slaying the snooping dragon: detecting botnets via structured graph analysis
- Abstract: In this talk I shall first highlight the impact of
surveillance botnet attacks and discuss the high level design of such
botnets using a real-world attack as a case study. We will discuss the
reasons behind their spectacular successes despite their centralized
design -- a fundamental weakness that limits their scalability and
robustness. Botnets designed primarily as vehicles for economic crime
reached these limits a while back. As a consequence, they moved to
more decentralized designs based on the use of structured overlay
topologies. While this has allowed them to scale in vast numbers, it
can also be used as a point of detection. In the second part of the
talk, I shall present techniques to localize botnet members based on
the unique communication patterns arising from their overlay
topologies used for command and control.
Experimental results on synthetic topologies embedded within Internet traffic traces from an ISP's backbone network indicate that our techniques (i) can localize the majority of bots with low false positive rate, and (ii) are resilient to the partial visibility arising from partial deployment of monitoring systems, and measurement inaccuracies arising from partial visibility and dynamics of background traffic.
See also:
- http://www.guardian.co.uk/technology/blog/2009/mar/29/dalai-lama-china-malware
- The snooping dragon: http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-746.pdf
- Botgrep: http://www.hatswitch.org/~sn275/papers/botgrep.pdf
- the topology of covert conflict: http://www.hatswitch.org/~sn275/papers/BCS-2006.pdf
- Speaker: Per Hakon Meland
- Title: Threat modelling: A short introduction and stories from end user involvement
- Abstract: This talk will present threat modelling with misuse cases and attack trees in the context of secure software development. Threat modelling can help identify security goals and potential pitfalls of an application at a very early stage, thus reducing the need for bolt-on security and patching. We will look at practical approaches and tools for creating threat models, and take a look at some models that were created and applied during real development projects. Similar applications tend to have similar threats, so one of our research questions has been to see how ordinary developers can benefit from reusable threat models.
- Speaker: Jean-Raymond Abrial
- Title: Development of a Network Topology Discovery Algorithm
- Abstract:
Topology discovery is a distributed algorithm that is at the core of
several routing algorithms, such as link-state routing. It is the
problem of each node in a network discovering and maintening information
on the network topology. The problem is challenging as the network can
change rapidly, indeed more rapidly than the nodes can track and account
for the changes.
The topology discovery algorithm we develop generalizes of the "master and dog" paradigm. Here is the story. A master rides a motorbike while his dog, running behind him, tries to get to him. If the master reduces the speed of the motorbike, then the dog come a bit closer to him. However, if the master accelerates, then the distance between the two increases. But, certainly enough, if the master stops for a sufficiently long period of time then the dog will reach eventually his master.
In our problem, the master is a graph representing the communication structure of a network. A move of the master corresponds to a modification of this graph. What makes our case different from the basic paradigm is that we have many dogs, each of them being a node in the graph. The distance between each dog and the master is represented by the difference between the physical graph and the image of it that each node constructs as soon as it gets some information about the "position" of the master. By definition, we say that a dog-node has reached the master-graph when the local image of the graph in this node corresponds exactly to the real situation of the graph.
In the case of the simple "master and dog" story, the dog reacts to the moves of the master because he can see the master. In our case, the situation is a bit more complicated. Only certain nodes can "see" certain moves of the graph. In other words, the nodes as a community get all information about the moves of the graph, but each individual node has only a partial direct access to these moves. More precisely, a node $n$ gets direct information about the modification of a link $l$ of the physical network if $n$ is the arriving node of link $l$.
Besides the limited information that it can get directly on the graph, each node can acquire more information about the graph from its neighbors (note that these neighbors changes over times as the graph evolves), which themselves either get some direct information on the graph or more information from their neighbors, and so on.
We would like to prove a result analogous to the one we have between the master and the dog, namely that the dog can reach his master if the latter stays still for a while. In our case, we shall prove that, under certain conditions, all dog-nodes can reach the master-graph if the latter stays still long enough.
- Speaker: Ralf Küsters
- Title: Central Security Requirements of E-Voting Systems: Verifiability, Accountability, and Coercion-Resistance
- Abstract:
Systems for electronic voting (e-voting systems), including
systems for voting over the Internet and systems for voting
in a voting booth, are supposed to simplify the process of
carrying out elections and potentially make the voting
process more secure and reliable. These systems are among
the most challenging and complex security-critical systems,
with a rich set of intricate security requirements they
have to fulfill. For example, besides keeping the votes of
individual voters private (privacy of votes), they should
allow voters to check that their votes were counted
correctly (verifiability), since voting machines might have
programming errors or might have been tampered with. By
providing voters with receipts of how they voted, this
problem on its own is easy to solve. However, at the same
time vote buying and voter coercion should be prevented
(coercion-resistance). Moreover, in case a problem occurs,
it should be possible to hold election officials
accountable for their misbehavior (accountability).
In recent work, we have formalized important security requirements for e-voting systems, including coercion-resistance, verifiability, and accountability, both in the symbolic and cryptographic settings. In this talk, I will discuss these requirements informally and sketch our formal definitions. I will also present several state-of-the-art voting systems and discuss their security with respect to our security definitions. The talk does not assume any background on e-voting systems or cryptography.
This talk is based on joint work with Tomasz Truderung and Andreas Vogt (S&P 2009, CSF 2010, and CCS 2010).
- Speaker: Piotr Kordy
- Title: Design and Analysis of Robust Timed Systems
- Abstract:
A timed system is designed within the framework of timed automata. Timed
automata have become a standard modeling and verification formalism for
systems with complex timed constraints. When a timed automaton has been
verified, the results of the verification should be insensitive to small
imprecision in e.g., clock speeds and system parameters. In such a case
the system is said to be robust. Robustness is an important property as
it is a prerequisite for being able to implement a verified design in a
reliable way.
In this presentation we will look at the semantics which models infinitely small clock drifts. If timed automaton is model checked using this "robust" semantics, the result of verification holds for infinitely small clock drifts and infinitely small imprecision on guards.
- Speaker: Shishir Nagaraja
- Title: Playing hide and seek in graphs OR the impact of unlinkability on adversarial community detection
- Abstract: In recent years anonymous communication networks promising unlinkability between users have become increasingly popular. This talk is about some of my work on community hiding and detection using a specific class of inference techniques. We'll use the threat model of a mobile-adversary (resource limited keylogging) who is primarily interested in breaking unlinkability to infer the community membership of users. Using a real-world email communication network, I shall first discuss the amount of link information an adversary is required to gather in order to accurately ascertain community membership information when anonymous channels are *not* in use. It turns out that selective surveillance strategies can improve the adversary's efficiency over random wiretapping. We then consider possible privacy preserving defenses; using anonymous communications helps, but not much. Finally we examine the space of counter-surveillance strategies where users defend against community detection by adding a small number of edges. We show that such defenses can significantly dent the adversary's ability to localize communities even after he/she has compromised the anonymity of a substantial majority of users.
- Speaker: Michael Clarkson
- Title: Hyperproperties.
- Abstract: Security policies on computer systems are usually expressed in terms of confidentiality, integrity, and availability. Unfortunately, no complete technique is known for formalizing and verifying such security policies. This talk proposes expressing security policies in terms of hyperproperties, a new mathematical framework based on sets of sets of traces. Hyperproperties are expressive enough for handling information flow, service guarantees, and a host of other security policies that have been problematic for the frameworks currently in use. Hyperproperties yield insight into the structure of security policies: every hyperproperty is the intersection of a safety hyperproperty and a liveness hyperproperty, where a safety hyperproperty proscribes bad system behaviors, and a liveness hyperproperty prescribes good system behaviors; and safety and liveness correspond to fundamental definitions of structures in mathematical topology. A class of hyperproperties (namely, safety hyperproperties whose bad behaviors can be finitely bounded) enjoys a relatively complete verification technique.
- Speaker: Yanjie Sun
- Title: Privacy in Social Networks ? A Comparative Study and A Scheme on Collaborative Management
- Abstract:
Social networks have sprung up and become a hot issue of current
socitey. In spite of the fact that these networks provide users with a
variety of attarctive 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 incured 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 optimiztion is further developed to improve its efficiency. Considering users might feel boresome in the case of large number of sharing resources, an inference technique is introduced to relieve user from the burden of massive manually input.
- Speaker: Zhiyuan Liu
- Title: Extending a Certified Email Protocol with TTP Transparency and its Formal Verification
- Abstract: 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. After that, 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 which can be naturally interpreted in alternating-time temporal logic (ATL) formulas with game semantics. The verification of properties expressed in ATL formulas corresponds to the computation of winning strategies. Besides, as to how to analyse the property of TTP transparency, another toolset $\mu$CRL is used, since we have to compare traces of getting evidences from different situations. The $\mu$CRL toolset has the ability of generating state spaces which can be visualized and manipulated by the toolbox CADP (Construction and Analysis of Distributed Processes) that acts as a back-end of $\mu$CRL.
- Speaker: Veronique Cortier
- Title: Can I get my security proof for free?
- Abstract: Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed and are used to efficiently detect flaws. In this talk, we will first review results and techniques that allow to analyze and compose security protocols. In a second part, we will present recent results that demonstrate that formal abstract models used for verification are actually sound with respect to much richer models that considers issues of complexity and probability. As a consequence, it is possible to derive strong, clear security guarantees still keeping the simplicity of reasoning in symbolic models. During this talk, we will also discuss the limitations of the current approaches, which are often hidden in the details of the hypotheses.
- Speaker: Sjouke Mauw
- Title: Looking for the needle in a haystack: reverse engineering data dumps
- Abstract:
Once an attacker has managed to decrypt smart card (e.g. for public
transportation), he has access to the stored data, but he still
doesn't know what these bits and bytes mean. In order to, for
instance, read the number of rides left on a card, the attacker must
locate the memory positions where the "number-of-rides-left" counter
is stored. This is the reverse engineering problem of data dumps.
In this talk I will define this problem and introduce some basic solutions. We will assume that the attacker has collected a number of data dumps of different cards and that he can attribute some information to each dump, e.g. how many rides there are still has left.
(joint work with Ton van Deursen and Sasa Radomirovic)
- Speaker: Peter Ryan
- Title: J-PAKE, a password based, authenticated key establishment protocol.
- Abstract:
Password Authenticated Key Establishment protocols are intended to allow parties to set up fresh, authenticated session keys without relying on a PKI. Instead we assume that Anne and Bob initially share a low entropy secret, e.g. a password. Such protocols must ensure that Yves, the attacker, passive or active, cannot launch offline dictionary attacks against the password, i.e. cannot garner enough material to be able to confirm guesses at the password. In other words, the goal is to bootstrap from a low entropy shared secret to high entropy secrets.
In this talk I will present a novel such protocol and discuss its design and analysis.
Joint work with Feng Hao, James Heather, Dalia Khader, Steve Schneider,.....
- Speaker: Melanie Volkamer
- Title: Electronic voting - past and future research at CASED
- Abstract: The past approach to create trust in electronic voting is based on the evaluation and certification of voting systems. In future, evaluated and certified systems will be even more trustworthy by providing E2E verifiability. This means that the voter can verify that his vote has been correctly included in the tallying. In addition everyone can verify that the tallying is correct. In my talk, I will first focus on our research results in the context of evaluation and certification of electronic voting systems. Afterwards, I will give a short introduction to E2E verifiable systems and point out the challenges in the context of usability in particular in the context of the Helios system.
- Speaker: Hugo Jonker
- Title: Anonymity and Verifiability in Voting: Understanding (Un)Linkability
- Abstract: Anonymity and verifiability are crucial security requirements for voting. Still, they seem to be contradictory, and confusion exists about their precise meanings and compatibility. In this presentation, we investigate and resolve the confusion by showing that both can be expressed in terms of (un)linkability: while anonymity requires unlinkability of voter and vote, verifiability requires linkability of voters and election result. By combining this with an adversary model that describes an adversary's abilities to establish links, we arrive at a comprehensive model for describing, analyzing and understanding privacy and verifiability in voting.
- Speaker: Sasa Radomirovic
- Title: Towards a model for security and privacy in the IoT
- Abstract: I will present first ideas towards building a security and privacy model for the Internet of Things (IoT). This will be a classic SRM talk in that the audience is invited to kick around ideas during the talk.
- Speaker: Georgios Pitsilis
- Title: Clustering Recommenders in Collaborative Filtering using Explicit Trust information
- Abstract: Clustering has been explored in information sciences as a solution to mitigate the information overload problem. In this work we explore the benefits of clustering in Recommender Systems. We demonstrate the performance advantages of classic clustering algorithms like k-means and we explore the use of new ones like Affinity Propagation (AP). Contrary to what has been used before, we investigate possible ways that the social oriented information like explicit trust could be exploited with AP for forming clusters of high quality. We conducted a series of evaluation tests using data from a real Recommender system Epinions.com from which we derived conclusions about the usefulness of trust information in forming clusters of Recommenders. Moreover, from our results we conclude that the potential advantages in using clustering can be enlarged by making use of the information that Social Networks can provide.
- Speaker: Matthijs Melissen
- Title: Doubtful Deviations and Farsighted Play - Anticipation in game theory
- Abstract: Nash equilibrium is based on the idea that a strategy profile is stable if no player can benefit from a unilateral deviation. We observe that some locally rational deviations in an strategic form game may not be profitable anymore if one takes into account the possibility of further deviations by the other players. As a solution, we propose the concept of farsighted pre-equilibrium, which takes into account only deviations that do not lead to a decrease of the player's outcome even if some other deviations follow. While Nash equilibria are taken to include plays that are certainly rational, our pre-equilibrium is supposed to rule out plays that are certainly irrational. We study this issue on several examples, including generalized Prisoner's dilemma.
- Speaker: Ben Smyth
- Title: Attacking ballot secrecy in Helios
- Abstract: Helios 2.0 is an open-source web-based end-to-end verifiable electronic voting system, suitable for use in low-coercion environments. The scheme is particularly significant due to its implementation and deployment for use in real-world elections: the Catholic University of Louvain adopted the system to elect the university president, and Princeton University used Helios to elect the student vice president; in addition, the International Association of Cryptologtic Research trialled the scheme in a non-binding poll. In this talk, we analyse ballot secrecy and discover a vulnerability which allows an adversary to compromise voters' privacy. This vulnerability has been successfully exploited to break privacy in a small election using the current Helios implementation. Moreover, the feasibility of an attack is considered in the context of French legislative elections and, based upon our findings, we believe it constitutes a threat to ballot secrecy in real-world elections. Finally, a fix is proposed.
- Speaker: Ben Smyth
- Title: Automated verification of selected equivalences with barriers
- Abstract: A procedure for the automated analysis of observational equivalence is delivered in the context of the applied pi calculus. In addition, the notion of barrier synchronisation is characterised for processes. The study of barrier synchronisation in relation to equivalence is particularly interesting because certain equivalence properties can only be realised under specific synchronisation assumptions. In particular, privacy preserving protocols -- including electronic voting schemes, vehicular ad-hoc networking protocols and anonymity networks -- make such assumptions. The results have been implemented in the tool ProSwapper, an extension to ProVerif, and the applicability of the tool is demonstrated by analysing vote privacy in electronic voting protocols and privacy in vehicular ad-hoc networks.
- Speaker: Barbara Kordy
- Title: On propositional Attack-Defense Trees
- Abstract:
Attack trees (ATrees) are a well-known methodology to describe the possible security weaknesses of a system.
Attack-defense trees (ADTrees) extend attack trees with defense nodes, and therefore allow us to represent
and analyze more complex attack-defense scenarios.
When using the propositional semantics, ATrees and ADTrees can be seen as representation languages for Boolean functions. In this presentation, we will take a look at these two languages and try to answer the following questions:
- Is the ATrees language complete?
- Is the ADTrees language complete?
- How hard is query evaluation on ADTrees compared to query evaluation on ATrees?
- Do we need new algorithms to process ADTrees?
- Are there any queries that can be (efficiently) solved on ATrees but not on ADTrees?