SRM seminar

Abstracts 2013

Speaker: Samir Ouchani
Title: A Security Verification Framework for SysML Activity Diagrams
Abstract:
UML and SysML play a central role in modern software and systems engineering. They are considered as the de facto standard for modeling software and systems. Today's systems are created from a myriad of interacting parts that are combined to produce visible behaviors. The main difficulty arises from the different ways in modeling each component and the way they interact with each other. Moreover, nowadays secure software has become an essential part in industrial development. One challenge in academia as well as in industry is to produce a secure product. Another challenge is to prove its correctness especially when the software environment is imprecise and uncertain.

The aim of this talk is to provide a practical and formal framework that enables security risk assessment and security requirements verification on a system modeled as a composition of UML/SysML behavioral diagrams. Our main contribution is a novel approach to automatically verify security of systems on their design models based on security requirements, probabilistic adversarial interactions between potential attackers and the system's models. These structures are shaped to provide an elegant way to define the combination between different kinds of diagrams. We rely on stochastic security templates to specify security properties and a standard catalogue of attack patterns to build a library of attacks design templates. The result of the interaction between selected attack scenarios and the composed diagrams with the instantiated security properties are used to quantify security risk by applying probabilistic model-checker. To handle the verification process scalability, our approach allows the verification of large system efficiently by optimizing and avoiding the global model construction. To demonstrate the effectiveness of our approach, we apply our methodology on academia as well as industrial benchmarks.

Speaker: Jeroen van de Graaf
Title: Improved Non-Interactive Dining Cryptographers
Abstract:
Dining Cryptographers is a well-known cryptographic protocol for anonymous broadcast, proposed by Chaum. In the original model it is assumed that all participants are on-line, which allows correcting problems that may occur, such as collisions (two participants happening to choose the same slot) or disrupters (dishonest participants who deviate from the protocol).

In 2006, the author proposed an off-line variant in which, after a preliminary phase in which random strings are exchanged, the participants only publish one long message. In this talk we will discuss this protocol and present some new results to improve efficiency.

This is joint research with Pablo García and Germán Montejano.

Speaker: Jean Krivine
Title: Rule-based modeling of protein-protein interaction networks: deriving pathways from facts.
Abstract:
Signaling pathways of the cell are causal cascades of protein-protein interactions (that involve complex formation and post-transcriptional modifications) that are triggered in response to the reception of some (protein) signal at the surface of the cell. Such pathways are generally classified according to their phenotypic outcome, such as cell growth, death or motion.

In this talk, which requires no deep knowledge about computer science nor biology, I will introduce Kappa, a rule-based formalism designed to model protein-protein interaction networks in a scalable fashion. Kappa is equipped with a stochastic simulator (KaSim) that may output time trajectories of particular protein complexes. We will see that by tracking the causal interplay between Kappa rule applications, it becomes possible to "explain" the appearance of particular observables (for instance a gene activation) during a simulation. We will argue that such "explanations" are good candidates for being "formal signaling pathways". It is noteworthy that standard causal semantics that are considered in computer science fail to give satisfactory "formal pathways". As a consequence the "formal pathways" that I will introduce in this talk require a notion of "non local causality". This new concept, albeit non standard in computer science, seems to match the intuitive notion of causality in signaling pathways. We will conclude about the general interest of "non local causality" for the computer science community.

Speaker: Vincenzo Iovino
Title: On the achievability of simulation-based security for functional encryption
Abstract:
Functional encryption is a generalization of public-key encryption that enables selective and fine-grained control over encrypted data. Though functional encryption is becoming very popular in real world applications and cloud computing, general and meaningful security definitions for this primitive are either insufficient or subject to impossibility results.

In this seminar I will survey the research in this area as well as I will present new perspectives. The first part of the talk will concern my paper published in CRYPTO 2013, and in the last part I will present my new results aimed to improve the state of the art.

Speaker: Gabriele Lenzini
Title: Applying the Socio-Technical Approach in Security
Abstract: Despite the enormous success of applied cryptography, how to achieve effective security still is an open question. This should not surprise since a system's security depends not only on its technical robustness but also on its social robustness, and therefore on how the system integrates with the environment and with the people it ultimately interacts. Consequently, one the greatest challenges facing computer security today are to discover what weaknesses lay in those "social layers. In this talk I will present some preliminary research on defining and using a framework for studying a system's security socio- technically. Such a framework consists of a reference model and some toolkits/methodologies. As proof of concept we apply the framework to study socio-technical security of two particular ceremonies: validating self-signed TLS certificates and selecting of WiFi access points.

Speaker: Diana Marosin
Title: Assessing Risks and Opportunities in Enterprise Architecture using an extended ADT Approach
Abstract: At every step in creating an enterprise design, architects encounter risks and opportunities. In most cases, risk assessment and treatment is done using the company's internal methodology or based on some best-practices known by the architect. We propose a method that can combine both qualitative and quantitative risk analysis and also incorporate risk mitigation solutions. In IT security, attack-defence trees (ADT) were used successfully to represent attacks and counter-measures. The goal of this talk is to present a methodology that leverages the ADT approach in order to assess risks and opportunities in enterprise architecture. We have elaborate a framework to identify the best ways to mitigate risks and increase enterprise's profitability based on architectural principles. We use a case study from the insurance sector in order to exemplify the capabilities of the framework.

Speaker: Liqun Chen
Title: Trusted Computing: Trusted Platform Modules and the Cryptographic Algorithms Supported by Them
Abstract: This talk is about trusted computing, the next generation of trusted platform modules (TPM2) and the cryptographic algorithms that are supported by them. After briefly describing the background of trusted computing and trusted platforms, we will discuss TPM2 and the cryptographic algorithms that it supports. The design target for TPM2 was high performance in hardware and we illustrate the design process used to achieve this by considering the development of the TPM2 digital signature primitive. This is a simple elliptic curve signature scheme and can be used to generate different types of signatures. Two known applications of this primitive are direct anonymous attestation (DAA) and U-Prove.

Speaker: Steve Kremer
Title: Automated verification of equivalence properties in symbolic models
Abstract:
Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks, which can be conveniently modeled using process equivalences. Currently, we are in the strange situation where nearly all security properties (with the notable exception of authentication) are modeled using such equivalences, while most tools are only able to verify trace properties.

We will discuss the few tools that have the ability to verify such equivalences and there limitations. Then we will present our approach which is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. The procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effectively tested on examples. Several of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol.

Speaker: Jose Miguel Perez Urquidi
Title: Attribute Based Signatures
Abstract:
Digital signatures are schemes for demonstrating the authenticity of a digital message or document. A valid standard signature gives reason to believe that the message was created by a known sender, who cannot deny having sent it. Under more strict anonymity requirements, one can sign using group signatures, ring signatures or attribute based signatures. The latter is the focus of our talk.

In Attribute Based Signatures (ABS), messages are signed under an attribute predicate, and users are anonymous under the group of all possible users that posses enough attributes to satisfy that predicate. In other words, attribute-based signatures demonstrate that a message was created by someone that owns enough attributes.

In this talk we introduce the basics notions of digital signatures, and present the advantages and shortcomings of the previous signing schemes. We will motivate and describe in detail the concept of attribute-based signatures.

Speaker: Christian W. Probst
Title: From System Models to Attack Trees
Abstract: In this work we aim at combining two techniques for identifying system vulnerabilities, attack trees and system models. Attack trees state the goal of an attack, and then represent different approaches to reach that goal. They are usually created by structured brain storming, and then can be analysed for quantitative and qualitative properties by tools such as the ADTool. System models, on the other hand, represent the structure of a system and interesting properties. They can be analysed for inherent vulnerabilities using formal methods. Obviously, system models and attack trees are closely related - in principle, the latter can be generated from the former, thereby coupling the system model to the quantitative and qualitative properties identified for attack trees. In this presentation we will present our work in the TREsPASS project.

Speaker: Stephen Clark
Title: Linguistic Steganography: Information Hiding in Text
Abstract:
Linguistic Steganography is concerned with hiding information in a natural language text, for the purposes of sending secret messages. A related area is natural language watermarking, in which information is added to a text in order to identify it, for example for the purposes of copyright. Linguistic Steganography algorithms hide information by manipulating properties of the text, for example by replacing some words with their synonyms. Unlike image-based steganography, linguistic steganography is in its infancy with little existing work. In this talk I will motivate the problem, in particular as an interesting application for natural language processing (NLP). Linguistic steganography is a difficult NLP problem because any change to the cover text must retain the meaning and style of the original, in order to prevent detection by an adversary.

I will describe a number of linguistic transformations that we have investigated, including synonym substitution and adjective deletion. For the adjective deletion I will describe a novel secret sharing scheme in which many people receive a copy of the original text, but with different adjectives deleted; only when the various texts are combined together can the secret message be revealed.

Joint work with Ching-Yun (Frannie) Chang.

Speaker: Jeroen van de Graaf
Title: Fast key distribution with security from quantum-optical noise
Abstract: The quantum-mechanical description of coherent light, as produced by lasers, gives rise to an intrinsic noise, known as quantum noise, optical noise or shot noise. Several protocols have been proposed to exploit this physical phenomenon to obtain secure data encryption and key distribution, including AlphaEta. Here we focus on the cryptographic aspects of a variant presented by Barbosa [PRA 2003] and propose an improvement, which is inspired on the concept of a pool of randomness as used by random bit generators in operating systems. This research in progress is a colaboration with Gabriel Almeida and Geraldo A. Barbosa.

Speaker: Philip Stark
Title: Mini-Minimax Uncertainty of Emulators
Abstract: In applications such as modeling climate, chemical reactions, automobile crashes, and aircraft, it is common to approximate the output of expensive "black-box" numerical simulators or of actual experiments with high-dimensional parameters using an "emulator," which is essentially an inexpensive interpolation based on a small number of simulations at different design points. Often, high-consequence decisions are based on the emulator output . How trustworthy are emulators? We formalize this problem as a pointwise minimax problem for estimating a function from a limited number of noise-free observations, subject to the constraint that the unknown function is no less regular than the observed data require it to be. Since the function is almost certainly rougher than any finite set of observations would reveal, this is a lower bound on the uncertainty. We solve the resulting optimization problem using ideas from Information Based Complexity. Applying the techniques to the Community Atmosphere Model (a popular climate model), we find that the uncertainty in a global flux estimate based on a particular set of 1154 observations is no smaller than the uncertainty a single well-placed observation would give. We also find lower confidence bounds for quantiles of the uncertainty and the mean of the uncertainty over the domain of the function. For the Community Atmosphere Model, these lower confidence bounds are an appreciable fraction of the maximum uncertainty. We conclude that emulators may not provide a trustworthy basis for decisions in many problems; it seems more promising to focus attention on particular scientific questions rather than on pointwise estimates.

Speaker: Sjouke Mauw
Title: Fair Parallel Multi-party Contract Signing Protocols
Abstract: Multi-party contract signing (MPCS) protocols allow a group of signers to exchange signatures on a predefined contract. A fair such protocol guarantees that either every honest signer receives the signatures of all other signers or no signer receives an honest signer's signature. Previous approaches considered either completely linear protocols or fully parallel broadcasting protocols. We introduce the new class of parallel MPCS protocols which combines parallel and linear execution and allows for parallelism even within a signer role.

Speaker: Walter Belgers
Title: Social Engineering
Abstract: Technical people look at security mostly from a technical standpoint. Are systems fully patched? Have SQL-injection problems been eliminated? Truth is, the technical aspect of security is just a small part of the problem. People are probably the biggest security problem to fix. Social engineering is conning people into giving you information or access to systems or buildings. It is, in most cases, far more easy than breaking in electronically. In this talk, we will look at what makes social engineering work, how to come up with working scenario's and how to try to avoid these problems. The lecture includes examples from actual social engineering assignments and some hilarious clips from the internet. After the talk, the attendees will hopefully understand the importance of security awareness within their organizations, being more alert to attacks at the same time.

Speaker: Xihui Chen
Title: A Trust Framework for Evaluating GNSS Signal Integrity
Abstract: Through real-life experiments, it has been proved, not only in theory but also in practice, that civil signals of Global Navigation Satellite Systems (GNSS) can be spoofed. Consequently, a number of spoofing detection techniques have been proposed to verify the integrity of GNSS signals. In this talk, we present a novel trust framework based on subjective logic to evaluate the integrity of received GNSS civil signals. We formally define signal integrity for the first time in the framework and use it to precisely characterise different spoofing detection methods. Our framework captures the uncertainty during the inference of signal integrity which has been largely ignored or not explicitly specified in the literature. Our framework also gives rise to several natural ways to combine the outputs of various spoofing detection methods on signal integrity. We validate our framework through experiments using both real and simulated signals and the results show that our framework is effective.

Speaker: Barbara Kordy
Title: Probabilistic framework for attack-defense trees
Abstract: In this talk, we present a novel methodology for probabilistic assessment of attack-defense scenarios. Our approach combines the security model of attack-defense trees with the probabilistic framework of Bayesian networks. This allows us to perform probabilistic computations in the presence of dependent actions. In our design, the Bayesian network does not replace the information represented by the structure of an attack-defense tree, but complements it with additional probabilistic dependencies between attack steps. The security model and the probability model are kept separate and can thus be created and maintained by different experts.

Speaker: Rui Joaquim
Title: Voter Verifiable Complex Ballots Encryption
Abstract:
This talk describes how to apply the MarkPledge voter (human) verifiable vote encryption technique to complex ballots, e.g. ballots with a large number of candidates and preferential voting ballots.

The presentation will be divided in two parts. The first part will focus on a new partial vote receipt approach that aims to minimize the usability issues of a direct MarkPledge approach to complex ballots. The second part of the presentation will focus on a new way to implement MarkPledge that is more flexible and efficient, thus better suited for complex ballots.

Speaker: Michele Orru
Title: I got your browser: say hello to BeEF
Abstract:
Nowadays web applications and browser security are hot topics. Many believe a simple Cross Site Scripting vulnerability might be more dangerous than a local privilege escalation. In this seminar we'll focus on XSS post exploitation, and generally hooking victim browsers with Social Engineering techniques to do a variety of nasty exploitation techniques.

In order to achieve this we'll use BeEF, the Browser Exploitation Framework, covering various modules and extensions that help to achieve persistence, trick victims to do unwanted actions, and launch exploits and additional attacks, sometimes to fully patched browsers.

Between the many, we'll cover Social Engineering attacks, Man in The Browser, Tunneling Proxy, together with various exploitation scenarios on the Intranet of the hooked browser.

Speaker: Tim Muller
Title: Beta Models with Trust Chains
Abstract: For some interactions over the Internet, it's useful to model agents (targets) as having a certain integrity. This (unknown) integrity determines the probability that the interaction succeeds or fails at the expense of the other agent (the subject). The subject constructs an estimate of the integrity of the target, called a trust opinion. If the only source of information is personal observations, then the Beta Model perfectly models the construction of trust opinions. We extend the Beta Model with recommendations. There is not a unique resulting model, but a family of models; the family of Beta Models with trust chains. We prove general properties for all models in the family of Beta Models with trust chains.

Speaker: Li Li
Title: Symbolic Analysis of an Electric Vehicle Charging Protocol
Abstract:
Electric vehicles are promising and futuristic automobiles which use electric batteries for clean energy. Because energy storage devices nowadays cannot meet the requirement for long-term driving, the electric vehicles need to visit charging stations frequently for energy supplying. As a result, the location privacy disclosed along with the charging process has drawn particular attention.

In the talk, we will describe a state-of-the-art protocol for this purpose and we will also present our ongoing work on formal verification of the protocol. This protocol has four sub-routines which are registration, charging, topup and statement. In each sub-routine, separate protocol and zero-knowledge proof have been used. Due to its high complexity, we decide to treat the zero-knowledge proofs as black boxes in the first place and reasoning each sub-routine symbolically. After that, we shall verify the zero-knowledge proofs on a computational level and give a complete proof to whole system. So far, the symbolic models have been built and formally verified. The verification on computational level is partially finished.

Speaker: Joost-Pieter Katoen
Title: Analyzing Probabilistic Programs: Pushing the Limits of Automation
Abstract:
Probabilistic programs are pivotal for cryptography, privacy and quantum programs, are typically a few number of lines, but hard to understand and analyse. The main challenge for their automated analysis is the in finite domain of the program variables combined with the occurrence of parameters. Here, parameters can range over concrete probabilities but can also encompass various aspects of the program, such as number of participants, size of certain variables etc.

McIver and Morgan have extended the seminal proof method of Floyd and Hoare for sequential programs to probabilistic programs by making the program annotations real- rather than Boolean-valued expressions in the program variables. As in traditional program analysis, the crucial annotations are the loop invariants. The problem to synthesize loop invariants is very challenging for probabilistic programs where real-valued, quantitative invariants are needed.

In this talk, we present a novel approach to synthesize loop invariants for the class of linear probabilistic programs. In order to provide an operational interpretation to the quantitative annotations, we give a connection between McIver and Morgan's wp-semantics of probabilistic programs and parameterized Markov decision processes.

Speaker: Yang Zhang
Title: A New Access Control Scheme for Facebook-style Social Networks
Abstract: The popularity of online social networks makes the protection of users' private information an important but scientifically challenging problem. In the literature, relationship-based access control schemes have been proposed to address this problem. However, with the dynamic developments of social networks, we identify new access control requirements which cannot be fully captured by the current schemes. In this talk, we focus on public information in social networks and treat it as a new dimension which users can use to regulate access to their resources. We define a new social network model containing users and their relationships as well as public information. Based on the model, we introduce a variant of hybrid logic for formulating access control policies. In addition, we exploit a type of category relations among public information to further improve our logic for its usage in practice.

Speaker: Jean Lancrenon
Title: Three-Party, Password-Authenticated Key Exchange with Server Private Keys
Abstract: This talk will describe ongoing work in three-party, password-authenticated key exchange (3-PAKE). In a 3-PAKE protocol, Alice and Bob share their own passwords with a trusted third party T that aids them in computing a shared, secret session key. The usual security requirements for password-based schemes are required to hold, namely the scheme should resist various flavors of password dictionary attacks. We make the case for considering 3-PAKEs that require T to have strong secret keying material in addition to holding user passwords. We will show how a simple trick commonly used in two-party, password-authenticated key exchange allows us to retain user-friendliness, lower protocol design complexity, and achieve additional security properties that ordinary 3-PAKEs cannot satisfy. Several protocols will be presented to illustrate our study.

Speaker: Marielle Stoelinga
Title: Time-Dependent Analysis of Attacks
Abstract:
The success of a security attack crucially depends on time: the more time available to the attacker, the higher the probability of a successful attack; when given enough time, any system can be compromised. Insight in time-dependent behaviors of attacks and the evolution of the attacker's success as time progresses is therefore a key for effective countermeasures in securing systems.

In this talk we present an efficient technique to analyze attack times for an extension of the prominent formalism of attack trees. If each basic attack step, i.e., each leaf in an attack tree, is annotated with a probability distribution of the time needed for this step to be successful, we show how this information can be propagated to an analysis of the entire tree. In this way, we obtain the probability distribution for the entire system to be attacked successfully as time progresses. For our approach to be effective, we take great care to always work with the best possible compression of the representations of the probability distributions arising. This is achieved by an elegant calculus of acyclic phase type distributions, together with an effective compositional compression technique.

Speaker: David Williams
Title: Model Checking under Refinement Closed Notions of Fairness
Abstract: Motivated by Murray's work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP's theory of refinement, enabling subsequent step-wise refinement of the CSP model.

Speaker: Mirosław Kurkowski
Title: Fast Verification of Security Protocols
Abstract:
Security protocols use cryptographic techniques to achieve some important goals in computer networks. These goals are for example authentication (identity confirmation of communicating sides), distribution of new session keys, or ensuring confidentiality of messages. For many years verification methods have been intensively studied, including verification of security properties in protocols.

In this talk, we will present a new concept of mathematical modeling and formal verification of security protocols. We will start with basic mathematical definitions of our mathematical model for protocol executions. Next we define correct sequences of protocol executions. Then, using the simple idea of chains of states, we will express the basic concepts, including knowledge of users and dependencies between steps of the protocol and other simultaneous executions. In particular, the feasible executions of the protocol will be modeled as a subtree of the tree of all executions of the protocol. Finally, we will show how to search the tree to find a possible attack or to prove correctness of the protocol. Suitable restrictions on the structure of the tree, ensure very short time of verification in all the examples considered and verified so far.

We will use the NSPK Protocol as a working example on which we explain the model and the algorithm. We will also give a glimpse of our experimental results for several protocols, and compare them with results obtained by the leading verification tools.

Speaker: Gerben Broenink
Title: Security in smart grids
Abstract:
Our energy infrastructure in changing. The amount of green energy is increasing, and consumers become prosumers. The classic infrastructure with one power plant which provides power to all consumers, is slowly transforming into a grid of consumers, prosumers, distributed energy suppliers, and power plants. The original hierarchical structure is being changed into an distributed structure. All these changes have an impact on the infrastructure, the traditional grid changes into a so called 'smart grid'. This means that more ICT is used to measure and control the energy infrastructure.

These changes to the energy infrastructure have the potential to increase the efficiency of the infrastructure, and enable the use of more green energy. However, they also introduce new risks. In my presentation, I'll clarify the changes made in the infrastructure, and I'll discuss some of the arising security questions.

Speaker: Christian Franck
Title: Anonymous communication and e-voting based on the Dining Cryptographers protocol
Abstract: In the dining cryptographers protocol, a malicious participant can disrupt communication by providing a wrong output. Existing techniques only allow to limit the damage to some extent. This is a major obstacle to the practical usage of the protocol. The objective of this thesis is to provide a better response to this problem. Our starting point are the ideas presented by Golle and Juels, where outputs of algebraic structure are generated based on the Diffie-Hellman key exchange, and where non-interactive zero-knowledge proof techniques allow to prove the correctness of these outputs. We present verifiable superposed sending, a computationally secure technique which allows participants to generate verifiable outputs. We use a reservation phase which provides participants with a digital pseudonym of the sender. They use this digital pseudonym to generate an output of algebraic structure by directly establishing a shared secret with the sender. A honest participant can prove that his output is correct with respect to the reservation. The dining cryptographers protocol becomes a practicable alternative to mixnets, especially when strong anonymity is required, and it has the advantage that it can transfer messages with lower latency. We present possible applications in the fields of electronic voting, low latency anonymous communication and secure multiparty computation.

Speaker: Paulo Verissimo
Title: Beyond the glamour of Byzantine Fault Tolerance: OR why resisting intrusions means more than BFT
Abstract: Byzantine Fault Tolerance (BFT) has become a reference paradigm for dealing with faults and intrusions, achieving security (and dependability) in an automatic way, much along the lines of classical fault tolerance. However, BFT is a means to an end--- intrusion tolerance and resilience--- and recent results which we review point to the fact that there is more to designing resilient systems than BFT and that, surprisingly or not, not all BFT algorithms lead to resilient designs. Although recent practical algorithmic or systems fixes have partially improved the situation, we show that the problems have a formal root: exhaustion failure and the susceptibility of current BFT systems to it. We discuss the theoretical underpinnings and then give several practical examples of the phenomenon. Then, we review recent research results that address a complete approach to designing resilient BFT systems, especially in dynamic and long-lived environments. Concepts like consensus, state machine replication, proactive/reactive recovery/resilience, diversity, distributed systems hybridization, exhaustion safety, are put in context in a coherent whole.

Speaker: Jannik Dreier
Title: Verifiability in e-Auction Protocols & Brandt's Protocol Revisited
Abstract:
An electronic auction protocol will only be used by those who trust that it operates correctly. Therefore, e-auction protocols must be verifiable: seller, buyer and losing bidders must all be able to determine that the result was correct. We pose that the importance of verifiability for e-auctions necessitates a formal analysis. Consequently, in the first part of the talk, we identify notions of verifiability for each stakeholder. We formalize these and then use the developed framework to study the verifiability of several examples. We provide an analysis of the protocol by Sako in the applied pi-calculus with help of ProVerif, finding it to be correct. Additionally we identify issues with the protocols due to Curtis et al. and Brandt.

In the second part, we will analyze the protocol by Brandt in more detail. We show first that this protocol - when using malleable interactive zero-knowledge proofs - is vulnerable to attacks by dishonest bidders. Such bidders can manipulate the publicly available data in a way that allows the seller to deduce all participants' bids. Additionally we discuss attacks on non-repudiation, fairness and the privacy of individual bidders exploiting authentication problems.

Speaker: Joel Ouaknine
Title: Decision Problems for Discrete Linear Dynamical Systems
Abstract:
Discrete linear dynamical systems permeate a vast number of areas of mathematics and computer science, and also have many applications in other fields such as economics and theoretical biology. In the context of computer science, discrete linear dynamical systems arise among others in connection with automated verification (termination of linear programs, probabilistic systems, stochastic logics), quantum computing, formal language theory, etc.

In this talk I will introduce discrete linear dynamical systems (absolutely no prior knowledge will be assumed) and present some fundamental decision problems, such as reachability and positivity.

This is joint work with James Worrell and Matt Daws.

Speaker: Muhammed Ali Bingol
Title: RFID security and privacy protocols for practical usage
Abstract:
The recent advent of ubiquitous technologies has raised an important concern for citizens: the need to protect their privacy. So far, this wish was not heard of industrials, but national and international regulation authorities, as the European Commission recently published some guidelines to enforce customers' privacy in RFID systems: "Privacy by design" is the way to be followed as stated in EC Recommendation. Research on privacy is an active domain but there is still a wide gap between theory and everyday life's applications. Filling this gap will require academia to design protocols and algorithms that fit the real life constraints. These requirements are 'sine qua non' conditions for deploying privacy-friendly authentication protocols in real-life applications. It is a popular challenge to design authentication protocols that are both privacy-friendly and usable in real-life. A significant portion of the literature in RFID is dedicated to that goal, and many inventive mechanisms were proposed to achieve it.

In this presentation, firstly, I will reintroduce security and privacy aspects of RFID applications and the trade-off between security and scalability. I will present our implementation of a scalable and forward-private authentication protocol, using a variant by Avoine et. al. that accommodates it to time-memory trade-offs. Then I will summarize some of our publications about RFID protocols and distance bounding protocols with their application scenarios.

Back to SRM presenations.

Contact

For questions and comments contact Barbara Kordy or Jean Lancrenon.