SRM seminar

Abstracts 2012

Speaker: Jason Crampton
Title: On the Parameterized Complexity of the Workflow Satisfiability Problem
Abstract: A workflow specification defines a set of steps and the order in which those steps must be executed. Security requirements may impose constraints on which groups of users are permitted to perform subsets of those steps. A workflow specification is said to be satisfiable if there exists an assignment of users to workflow steps that satisfies all the constraints. An algorithm for determining whether such an assignment exists is important, both as a static analysis tool for workflow specifications, and for the construction of run-time reference monitors for workflow management systems. Finding such an assignment is a hard problem in general, but work by Wang and Li in 2010 using the theory of parameterized complexity suggests that efficient algorithms exist under reasonable assumptions about workflow specifications. We improve the complexity bounds for the workflow satisfiability problem. We also generalize and extend the types of constraints that may be defined in a workflow specification and prove that the satisfiability problem remains fixed-parameter tractable for such constraints.

Speaker: Luca Viganò
Title: Formal Methods for the Security of the Internet of Services
Abstract:
In the Internet of Services (IoS), systems and applications are no longer the result of programming components in the traditional meaning but are built by composing services that are distributed over the network and reconfigured and consumed dynamically in a demand-driven, flexible way. However, composing services leads to new, subtle and dangerous, vulnerabilities due to interference between component services and policies, the shared communication layer, and application functionality.

In this seminar, I will briefly present the AVANTSSAR Platform and the SPaCIoS Tool, two integrated toolsets for the formal specification and automated validation of trust and security of applications in the IoS at design time and run time, respectively. (Both have been developed in the context of FP7 projects that I have been coordinating.) To highlight some of my contributions to AVANTSSAR and SPaCIoS, I will focus on two particular results.

First, I will discuss a compositionality result that formalizes conditions for vertical composition of security protocols, i.e., when an application protocol (e.g., a banking service) runs over a channel established by another protocol (e.g., a secure channel provided by TLS). This is interesting and useful as protocol composition can lead to attacks even when the individual protocols are all secure in isolation.

Second, I will briefly discuss how although computer security typically revolves around threats, attacks and defenses, the sub-field of security protocol analysis has so far focused almost exclusively on the notion of attack. I will motivate that there is room for a fruitful notion of defense for vulnerable protocols and that the conceptual bridge lies in the notion of multiple non-collaborating attackers and interference between simultaneous attack procedures.

Speaker: Jeff Yan
Title: The design of image recognition CAPTCHAs: challenges and solutions
Abstract: CAPTCHA has already become a standard security mechanism, but it's hard to get its design right. Most text CAPTCHAs were broken, and there is a growing interest in the research communities exploring an alternative: image recognition CAPTCHAs (IRCs), which require interdisciplinary expertises including computer vision and image processing, HCI, machine learning and security. In this talk, I discuss the design of IRCs for large-scale real-life applications such as Gmail and Hotmail, where millions of CAPTCHAs are required on a daily basis. Some design challenges will be highlighted, e.g. security, usability and scalability. I will show how representative IRCs were broken due to novel attacks, and define a simple but novel framework for guiding the design of robust IRCs. Then, I will present Cortcha, a novel design that relies on Context-based Object Recognition to Tell Computers and Humans Apart. Cortcha meets all the key design criteria, and arguably represents the state-of-the-art design of IRCs. This is joint work with Dr Bin Zhu's team at Microsoft Research Asia, Beijing.

Speaker: Alexandre Dulaunoy
Title: The Attackers' Principles
Abstract: An introduction to the mindset of the attackers based on an empirical analysis of the incidents received by the CERT community in Luxembourg and abroad. The idea is to discover the mindset of the attackers by the techniques they are using. Can we generalize some rules? Can we use those principles to better protect our infrastructures? Can the prototyping of offensive technologies help us?

Speaker: Hongyang Qu
Title: Incremental Quantitative Verification for Markov Decision Processes
Abstract: Quantitative verification techniques provide an effective means of computing performance and reliability properties for a wide range of systems. However, the computation required can be expensive, particularly if it has to be performed multiple times, for example to determine optimal system parameters. We present efficient incremental techniques for quantitative verification of Markov decision processes, which are able to re-use results from previous verification runs, based on a decomposition of the model into its strongly connected components (SCCs). We also show how this SCC-based approach can be further optimised to improve verification speed and how it can be combined with symbolic data structures to offer better scalability. We illustrate the effectiveness of the approach on a selection of large case studies.

Speaker: Devrim Ünal
Title: The Formal Policy Framework for Mobility: Formal Specification, Verification and Enforcement of Location and Mobility Related Security Policies
Abstract:
In this seminar, a novel security policy specification and verification framework named FPFM (Formal Policy Framework for Mobility) will be presented. The proposed framework presents novel findings in the areas of location and mobility based security, multi-domain security and formal verification of security models and security policies, including information flow analysis, model checking of security policies based on process calculus and inductive theorem proving of security policies. A formal role-based access control model named FPM-RBAC is proposed for the specification of security policies. The security policy model represents novelty regarding location and mobility constraints, mapping of role hierarchies, specification of multi-domain security policies and separation of duty constraints. An XML-based security policy language named XFPM-RBAC implements the FPM-RBAC security policy model and supports automatic generation of formal security policy specifications.

Formal verification of security policies are supported through model checking and theorem proving. A spatio-temporal model checking algorithm based on Ambient Logic has been proposed, for the formal verification of Ambient Calculus based specifications for mobile systems. The proposed algorithm is capable of spatio-temporal model checking of mobile network configurations with respect to location and mobility constraints. Information flow analysis, based on allowed flows by a security policy, is also possible by using the same approach. Theorem prover specifications have been developed for the purpose of verification of role based access control policies by use of the Coq theorem prover.

The presentation will mainly focus on two of the components of FPFM: the FPM-RBAC model and the spatio-temporal model checking algorithm. Possible extensions and improvements to the FPFM framework, such as partial order reduction, stochastic model checking, attack modeling and privacy enhanced access control will be discussed.

Speaker: Sasa Radomirovic
Title: Constructing Short Sequences Containing All Permutations of a Set as Subsequences
Abstract:
A sequence over a fixed finite set is said to be complete, if it contains all permutations of the set as (not necessarily consecutive) subsequences. Determining the length of shortest complete sequences is an open problem. The problem arises naturally when considering fairness of optimistic multi-party protocols in asynchronous communication networks with an offline trusted third party. Examples of such protocols are reconstruction of a shared secret and contract signing.

I will present new upper bounds for the length of shortest complete sequences and discuss a variety of approaches to construct such sequences.

Speaker: Tejeddine Mouelhi
Title: PPTree: An Attack-Defense Tree Driven Creation of Protection Profile
Abstract: This talk will present the work done in the DG-Trac project, an ESA funded project, in which SnT is in charge of security requirements definition. This talk will present the approach based on attack-defense trees that aims at defining the DG-Trac protection profile, based on common criteria ISO/IEC 15446. The context of the DG-Trac project will be presented. Then, a description of the concept of protection profiles and the common criteria methodology will be presented. Afterwards, the way attack-defense trees are used to assist creating protection profiles will be described. The talk will end with a discussion, a return-of-experience on attack-defense trees, the drawbacks, the challenges and some open questions regarding the limitations of the proposed approach.

Speaker: Florian Kerschbaum
Title: An Optimizing Compiler for Secure Computations
Abstract: Secure multi-party computations have many applications in privacy and data security. They can solve cross-organizational problems in supply chain management or privacy-enhanced data analysis, such that the protection needs of the parties are respected. Nevertheless, the development of protocols for multi-party computation is extremely complex. Domain-specific languages can help the programmer to implement more efficiently and effectively. However, compilers currently produce worse results than manually generated protocols. Program analysis and automated optimization can remedy this problem. Based on two practical examples we show a general technique for optimizing secure computations which can be automatically implemented in a compiler.

Speaker: Andreas Albers
Title: Towards Privacy as a Competitive Edge for Online Business
Abstract:
Online businesses increasingly rely on personal data in order to provide value for their users and to differentiate from competition. At the same time users become more and more concerned about privacy threats resulting from their online activities. Today, it is (still) difficult for users to control the collection and use of their personal data when interacting with online businesses. Therefore, privacy research so far has been focusing mainly on the development of means to support users in protecting their privacy. However, from an online business perspective, existing or upcoming means of privacy protection (e.g. tracking protection tools) could also hamper current online business models. Consequently, privacy research should also consider and address the need of online businesses for personal data in their research agenda.

The first half of the talk will outline a vision on how privacy can become a competitive edge for online businesses. This can provide an incentive for online businesses to excel at protecting the privacy of their users. At the same time, it lays the foundation for a fair trade-off between user privacy and value provision by online businesses. As a starting point for this endeavor, we propose a paradigm shift in which online businesses offer users the ability to maintain their digital identity instead of solely enabling them to review their personal data and setup privacy policies. The second half of the talk will provide an overview of selected research projects at Goethe University in the area of mobile marketing, mobile sensing and privacy aspects of online communities, which contribute to this vision.

Speaker: André Deuker
Title: All Friends Are Equal - Some Even More: An Investigation of Privacy Protection Among Facebook Users
Abstract: Social Networking Sites (SNS) such as Facebook are a great chance for social scientists to observe human interaction and social phenomena. Information system (IS) researchers, a sub-group of social scientists, analyse the effect which SNS properties have on human behaviour. As such, IS research aims to build bridges between social science and information technology in order to support users and providers of SNS. Given this research domain, part 1 of this talk will present a qualitative IS study on information overload and privacy protection on SNS. The objective of this study is to provide answers to questions such as "What makes SNS newsfeed content interesting from an individual user's perspective?" or "Based on which criteria do users decide who is allowed to see things they share on SNS?". The results of our study reveal a set of "contextual factors", which determine information consumption and sharing behavior of users. Then, part 2 of this talk presents our endeavor to transfer these gained insights into a privacy advisor concept in order to support SNS users in their daily sharing activities.

Speaker: Rolando Trujillo Rasúa
Title: : Privacy-preserving publication of spatio-temporal data
Abstract: Today's pervasiveness of location-aware devices like mobile phones and GPS receivers helps companies and governments to easily collect huge amount of information about the movements of people. Analyzing and mining this type of information, also known as trajectories or spatio-temporal data, might reveal new trends and previously unknown knowledge to be used in traffic, sustainable mobility management, urban planning, supply chain management, etc. By doing so, resources can be optimized and business and government decisions can be solid and well-founded. As a result, it is considered that both companies and citizens profit directly from the publication and analysis of spatio-temporal databases. However, the privacy of individuals is obviously downgraded if their trajectories are published in a way which allows re-identification of the individual behind a trajectory. Those privacy threats, together with the most important solutions and challenges on trajectory anonymization, will be introduced in this talk.

Speaker: James Heather
Title: Cryptography with Everyday Objects
Abstract: Most security protocols appearing in the literature make use of cryptographic primitives that assume that the participants have access to some sort of computational device. However, there are times when there is need for a security mechanism to evaluate some result without leaking sensitive information, but computational devices are unavailable. We discuss here various protocols for solving cryptographic problems using everyday objects: coins, dice, cards, and envelopes.

Speaker: Vaishnavi Rajendran
Title: Attribute Based Searching of Encrypted Data
Abstract: Cloud Computing is an emerging platform in recent times. The basic concept of Cloud computing involves delivering data or a form of service (Eg. Storage, Software etc.) over the internet in a on-demand basis. In a cloud when say a file is uploaded onto the server, the sender might not know who on the other end is going to access his file from the cloud. This calls for a security concern. Attribute Based Encryption is an encryption scheme that allows a user to decrypt a ciphertext if he/she had the right set of attributes. The attributes are required to satisfy a security policy. If attribute based encryption is applied to a cloud computing platform, it would allow only a certain set of users who held the right attributes to access a file uploaded by the sender. Another feature that can be added to the cloud computing platform is the ability for the user to search for the particular file(s) she requires instead of downloading a large bulk of data at one instant. Public Key Encryption with Keyword Search introduces searchable encryption of ciphertexts. It allows users to set up a gateway at the server that can search for required messages without gaining any knowledge of the contents of the message. We bring together the techniques behind both Attribute Based Encryption and Public Key Encryption Search with Keyword search to form a new proposal towards a cloud computing platform.

Speaker: Josep Domingo-Ferrer
Title: Co-utility: rational self-enforcement of privacy, security and functionality
Abstract:
A major problem in the global information society is the lack of a worldwide legal framework accepted by all countries. This raises the issue of how to protect the legitimate interests of the various players in information transactions. Protocols for information technology transactions should be designed so that the best interest of any protocol participant leads her to act in such a way that she serves the best interest of the other protocol participants. This will allow effortlessly achieving a fair operation of the information society as the result of rational co-operation rather than as an expensive legal requirement.

We introduce the novel concept of co-utility or co-operative utility, which can be defined in game-theoretic terms: a protocol offers co-utility or is co-utile if the best option for a player to maximize her utility is to co-operate with one or more other players to maximize their utility. Reasonable components of utility in the information society are security, privacy and functionality. The privacy component of co-utility corresponds to the co-privacy property that we have recently introduced.

The co-utility property makes an individual's utility maximization a goal that rationally interests other individuals: it is a matter of helping oneself by helping someone else. Co-utility is a groundbreaking concept because it opens the way to a joint and coordinated treatment of privacy, security and functionality. We formally define co-utility in terms of game equilibria and we illustrate its use in several practical applications: i) controlled content distribution, data liberation and digital content oblivion; ii) anonymous keyword search; iii) communication in vehicular ad hoc networks (VANETs), and iv) social networks.

Speaker: Michèle Feltz
Title: Beyond eCK: Security against Stronger Adversaries
Abstract:
We show that it is possible to achieve perfect forward secrecy in two-message or one-round key exchange (KE) protocols that satisfy even stronger security properties than provided by the extended Canetti-Krawczyk (eCK) security model. In particular, we consider perfect forward secrecy in the presence of adversaries that can reveal ephemeral secret keys and the long-term secret keys of the actor of a session.

We propose two new security models for KE protocols. First, we formalize a slightly stronger variant of the eCK security model that we call eCKw. Second, we integrate perfect forward secrecy into eCKw, which gives rise to the even stronger eCK-PFS model. We propose a security-strengthening transformation (i.e. a compiler) between our new models. Given a two-message Diffie-Hellman type protocol secure in eCKw, our transformation yields a two-message protocol that is secure in eCK-PFS. We demonstrate how to generalize this result to other KE security models and argue why the MAC transformation does not achieve eCK-PFS security.

Speaker: Tim Muller
Title: Composite Trust; a formal derivation of conjunction and disjunction of trust opinions
Abstract: Trust appears in asymmetric interactions, where a user is dependent on the willingness of another party to successfully cooperate. To avoid initiating interactions with parties that will likely fail to cooperate, users establish trust opinions about other parties. The Beta Model is a popular, formal model that deals with such trust opinions. The Beta Model is not very expressive, as the assumptions required for the formal model are restrictive. In the literature, several models are extensions of the Beta Model. These models are not usually derived from a set of assumptions, but rather based on the intuitions of the authors. In this presentation, we want to formally derive conjunction and disjunction of trust opinions. We will introduce a set of assumptions for the Beta Model, and add some assumptions about conjunction and disjunction. From this extended set of assumptions, we will derive a general way of computing (composite) trust opinions. Furthermore, we will compare our results with the literature, and look at the implications.

Speaker: Assaad Moawad
Title: Social dimension in security systems
Abstract: Access control policies are often defined on the basis of the least privilege principle. According to this principle, users should only be able to access the minimum amount of information necessary to accomplish their duties. Such policies, however, are often perceived as too restrictive, and users do not have the rights necessary to perform assigned duties or collaborate with other users. As a consequence, access control mechanisms are perceived as a barrier and thus bypassed, making the system insecure. In this talk, we are going to discuss the social dimension in security systems. We will present conviviality concept which is a social science concept for ambient intelligent systems to highlight soft qualitative requirements like user friendliness. We will show how to use conviviality as a way to integrate human needs for socialness and collaboration in order to design better and more secure systems where users feel less tempted to cheat and less tempted to bypass the access control policy. We illustrate our presentation with use cases from the Ville de Luxembourg.

Speaker: Naipeng Dong
Title: Formal Analysis of Privacy in an eHealth Protocol
Abstract: Given the nature of health data, privacy of eHealth systems is of prime importance. An eHealth system must enforce that users remain private, even if they are bribed or coerced to reveal themselves or others. Consider e.g. a pharmaceutical company that bribes a pharmacist to reveal information which breaks a doctor's privacy. In this talk, we identify and formalise several new but important privacy notions on enforcing doctor privacy. Then we analyse privacy of a complicated and practical eHealth protocol. Our analysis shows to what extent these properties as well as properties such as anonymity and untraceability are satisfied by the protocol. Finally, we address the found ambiguities resulting in privacy flaws, and propose suggestions for fixing them.

Speaker: Cas Cremers
Title: Distance Hijacking attacks on Distance Bounding Protocols
Abstract: After several years of theoretical research on distance bounding protocols, the first implementations of such protocols have recently started to appear. These protocols are typically analyzed with respect to three types of attacks, which are historically known as Distance Fraud, Mafia Fraud, and Terrorist Fraud. We define and analyze a fourth main type of attack on distance bounding protocols, called Distance Hijacking. This type of attack poses a serious threat in many practical scenarios. We show that many proposed distance bounding protocols are vulnerable to Distance Hijacking, and we propose solutions to make these protocols resilient to this type of attack. We show that verifying distance bounding protocols using existing informal and formal frameworks does not guarantee the absence of Distance Hijacking attacks. We extend a formal framework for reasoning about distance bounding protocols to include overshadowing attacks. We use the resulting framework to prove the absence of all of the found attacks for protocols to which our countermeasures have been applied.

Speaker: Cas Cremers
Title: Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Abstract: We present a general approach for the symbolic analysis of security protocols that use Diffie-Hellman exponentiation to achieve advanced security properties. We model protocols as multiset rewriting systems and security properties as first-order formulas. We analyze them using a novel constraint-solving algorithm that supports both falsification and verification, even in the presence of an unbounded number of protocol sessions. The algorithm exploits the finite variant property and builds on ideas from strand spaces and proof normal forms. We demonstrate the scope and the effectiveness of our algorithm on non-trivial case studies. For example, the algorithm successfully verifies the NAXOS protocol with respect to a symbolic version of the eCK security model.

Speaker: Rui Joaquim
Title: A highly sound and efficient voter verifiable vote encryption technique (MarkPledge 3) and its use in the EVIV Internet voting system
Abstract:
The MarkPledge 3 (MP3) technique is a highly sound voter verifiable encryption technique that follows the working principle of the MarkPledge technique (Neff, 2004). Due to its simple mathematical structure, MP3 presents significant theoretical and practical improvements over the previous two MarkPledge technique specifications (MP1 and MP2) and it is specially adapted to run on computational constrained devices, e.g. smart cards.

EVIV is a highly sound End-to-end Verifiable Internet Voting system whose integrity is guaranteed by the participation of one honest trustee in a random number generation protocol at the beginning of the election day. The EVIV vote protocol integrates the MarkPledge and the code voting techniques to create a vote protocol which, in addition to the strong integrity properties, offers full voter's mobility and preserves the voter's privacy from the vote casting PC, even if the voter votes from a public PC, such as a PC at a cybercafé or at a public library.

The MP3 is specially relevant to EVIV since, to give full voter's mobility and to protect the voter's privacy from the vote casting PC, the vote encryption is created by a voter security token, e.g. a smart card, which is a computational constrained device.

Speaker: Weili Fu
Title: Labeling Extensions of General Tableaux with Many Truth Values
Abstract: Truth values of statements in reasoning problems are true and false typically. In our work a statement is associated with a value in a linear ordered set which is used in the applications about degrees of trust, access rights, levels of granularity. To know whether a consequence is inferred by a set of statements labelled with such values, instead of reasoning for every set of statements, we compute a value in the linear ordered set so called maximal truth value for this consequence. To compute this value, we extend general tableaux to create a general approach. Since termination is not preserved by the extension of general tableaux, priority strategy on the order of rule applications is defined and a constraint on the inputs is designed. The extension with these settings can be applied to the tableaux for ALC in description logics. We additionally explore another termination technology--blocking. To imply tableaux in description logics, tree tableaux was defined which generate tree-like structures. We define a normal form for tree tableaux such that generation of tree structures by rule applications is fit for defining blocking. A transformation procedure for normal form is also defined. Blocking condition for termination is defined for tree tableaux and then extended for the extension of tree tableaux. Tree tableaux with blocking are again applied to most tableaux in description logics.

Speaker: Iuliia Tkachenko
Title: Universal Steganalysis without source-cover mismatch
Abstract: Recently a large number of algorithms for hiding information in digital files (images, mp3 files, texts, etc.) appeared. In this presentation we will talk about detection of the presence of hidden information in JPEG-images. The main purpose is to detect presence of hidden information even in the case of novelty (other steganography algorithms than those used during the learning). Firstly we will talk about the steganalysis scenario that we call "universal steganalysis". Then we will consider several methods of machine learning (One-class and Multi-class classification) for detection the presence of hidden information in JPEG-images. In the end we will suggest using the fusion of classification results of two classifiers in order to increase the probability of detection of steganographic images.

Speaker: Xihui Chen
Title: Post-hoc User Traceability Analysis in Electronic Toll Pricing Systems
Abstract: Electronic Toll Pricing (ETP), a location-based vehicular service, allows users to pay tolls without stopping or even slowing down their cars. User location records are collected so as to calculate their payments. However, users have privacy concerns as locations are considered as private information. In this talk, we focus on user traceability in ETP systems where anonymous location records are stored by the service providers. Based on user toll payment information, we propose a post-hoc analysis of user traceability, which aims at computing a user's all possible traces. Moreover, we propose several methods to improve the effectiveness of the analysis by combining other contextual information and propose a number of optimizations to improve its efficiency as well. We develop a prototype and evaluate the effectiveness of the analysis by conducting extensive experiments on a number of simulated datasets.

Speaker: Patrick Schweitzer
Title: Specifying quantitative questions on Attack-Defense Trees
Abstract: Attack-defense trees are a novel methodology for graphical security modeling and assessment. The methodology includes a visual-intuitive and a formal model. Both, the intuitive and the formal components of the approach can be used for quantitative analysis of attack-defense scenarios. This talk details how to bridge the gap between the intuitive and the formal way of quantitatively assessing attack-defense scenarios. We discuss how to properly specify an intuitive quantitative question. Given a well specified question, we then show how to derive an appropriate domain which constitutes the corresponding formal model.

Speaker: Jason Crampton
Title: Cryptographic enforcement of interval-based access control policies
Abstract: The enforcement of authorization policies using cryptography has received considerable attention in recent years. Enforcement mechanisms vary in the amount of storage and the number of key derivation steps that are required in the worst case. These parameters correspond, respectively, to the number of edges and the diameter of the graph that is used to represent the authorization policy. In this talk we will consider a particular class of access control policies and the associated graphs. We then present a number of techniques for constructing a new graph that has a smaller diameter than the original graph but enforces the same authorization policy.

Speaker: Christoph Bösch
Title: Selective Document Retrieval from Encrypted Database
Abstract: We propose the concept of selective document retrieval (SDR) from an encrypted database which allows a client to store encrypted data on a third-party server and perform efficient search remotely. We propose a new SDR scheme based on the recent advances in fully homomorphic encryption schemes. The proposed scheme is secure in our security model and can be adapted to support many useful search features, including aggregating search results, supporting conjunctive keyword search queries, advanced keyword search, search with keyword occurrence frequency, and search based on inner product. To evaluate the performance, we implement the search algorithm of our scheme in C. The experiment results show that a search query takes only 47 seconds in an encrypted database with 1000 documents on a Linux server, and it demonstrates that our scheme is much more efficient, i.e., around 1250 times faster, than a solution based on the SSW scheme with similar security guarantees.

Speaker: Selwyn Piramuthu
Title: PUF-based Authentication Protocol to Address Ticket-Switching of RFID-tagged Items
Abstract: Ticket-switching incidents where customers switch the price tag or bar code in order to pay a lower amount for their 'purchased item' is not uncommon in retail stores. Since the item still has to pass through a check-out counter before it's out of the store, it has a (even if miniscule) positive probability of being identified. However, when item level RFID tags are used in an automated check-out environment, the probability of such incidents coming to light is estimated to be almost zero. We propose an authentication protocol for this scenario using a pair of item-level RFID tags, one of which is PUF-enabled to resist cloning attacks.

Speaker: Ran Xue
Title: User Mobility Profiles and Their Usage in Location-Based Services
Abstract: The increasing availability of location-acquisition technologies (GPS, GSM networks, etc.) enables people to log their location histories with spatio-temporal data. Such real-world location histories give us two major opportunities: to discover useable knowledge about users' mobility profiles and to understand the correlation between users and their visited locations. In this project we propose a method to construct users' mobility profiles and compute the similarity between users based on the distance function we define on profiles. Moreover, such individual's mobility profile can be matched to an anonymous routine, which leads us to the privacy attack/protection field in location based-services. We can also develop a system to recommend friends and locations to users according to the similarity matrix we compute.

Speaker: Barbara Kordy
Title: On optimistic multi-party contract signing protocols
Abstract:
Multi-party contract signing (MPCS) protocols specify how a number of signers can cooperate in achieving a fully signed contract, even in the presence of dishonest signers. Here we consider optimistic MPCS protocols, where we assume presence of a trusted third party which is contacted only in case of a conflict.

The presentation discusses a connection between optimistic MPCS protocols and the combinatorial problem of constructing sequences which contain all permutations of a set as subsequences. We provide an explicit and general construction for MPCS protocols which converts a sequence over a finite set of signers into a protocol specification for the signers. Furthermore, we give tight conditions under which the resulting protocols satisfy fairness and timeliness.

Speaker: Yang Liu
Title: Pervasive Model Checking
Abstract: Model checking is emerging as an effective software verification method with wide applications. However, still there are a lot research challenges in model checking techniques and in applying model checking techniques. To address these challenges, this talk presents our research contributions in the system modeling, efficient model checking algorithms development and effective reduction techniques. More important, we introduce a process analysis toolkit (PAT, www.patroot.com), which is a self-contained verification framework for specification, simulation and verification of concurrent, real-time and probabilistic systems. PAT architecture provides extensibility in many possible aspects: modeling languages, model checking algorithms, reduction techniques and so on. Various model checkers have been developed under this new architecture in short time. Since PAT is released 5 years ago, it has attracted 2000+ registered users world wide. Our vision is to achieve pervasive model checking so as to build a framework for realizing different verification techniques, and making model checking as planning, problem-solving, scheduling/services.

Speaker: Zhenchang Xing
Title: Feature Location: How it is and How it Should be Supported
Abstract: Feature location links program elements to features described in natural language. It is an important and recurring activity for efficient software maintenance, reengineering and validation. In this talk, I will first discuss an empirical study of the effectiveness of Information Retrieval (IR) based feature location techniques. This study suggests that IR techniques have to be customized for software data. I will then briefly summarize three on-going projects that exploit unique characteristics of software data to improve the effectiveness of IR-based feature location. Next, I will discuss a developercentered study that investigates how developers actually perform feature location tasks. This study proposes a conceptual framework for understanding feature location process. This framework reveals that feature location engages multiple levels of information and it is a multi-faceted interactive search process. The lessons learned from this developer-centered study motivate my ongoing research on an intelligent, interactive, on-the-fly wizard that can provide context-sensitive and personalized support for feature location tasks.

Speaker: Harm van Beek
Title: Digital Forensics, what's that about?
Abstract: The Netherlands Forensic Institute (NFI) provides a large variety of forensic services to clients within the criminal justice chain, such as the Public Prosecution Service and the police. It uses the newest technologies and scientific insights. In this talk, I give an overview of the daily work and forensic research that takes place at the NFI's Digital Technology group. This work focuses on securing evidence from a crime scene, making digital data available to examiners from this evidence and doing detailed analysis of this data. The NFI developes tools and technology to support all three stages.

Speaker: Dominique Cansell
Title: Formal and Incremental Construction of the Distributed Reference Counting Algorithm
Abstract: The development of distributed algorithms and, more generally, distributed systems, is a complex, delicate and challenging process. Refinement techniques of (system) models improve the process by using proof assistant and by applying a design methodology aiming at starting from the most abstract model and leading to the most concrete model in an incremental way, for producing a distributed solution. In this talk we present a complete and proved development of a distributed reference counting algorithm. This algorithm is used to share and remove resources in a distributed way and also in distributed garbage collection. A resource is created by a site (the owner) and can be used by other sites. The owner of a resource can remove it only when it is sure that this resource is not used by another site. L. Moreau and J. Duprat have developed such an algorithm and proved it using the proof assistant Coq. The first contribution of our work is the incremental construction starting from a simple abstraction without any distribution through to a distributed and concrete algorithm which looks like that of Moreau and Duprat. This incremental construction allows us to validate step by step the real algorithm and to prove it more easily. We show how models are produced in an elegant and progressive way, thanks to the refinement and how the final distributed algorithm is built starting from these models. The development is carried out within the framework of the event B method and models are validated with a tool (Rodin). We give also an explanation on the termination of this algorithm using specific constraints (limited messages like Moreau and Duprat). It is a joint work with Dominique Mery.

Speaker: Jan Willemson
Title: Internet voting in Estonia - risk analysis and vote verification
Abstract:
In Estonia, legally binding voting over Internet has been possible since 2005. During the parliamentary elections of 2011, almost 25% of the votes were cast over Internet. Unfortunately, this also means that Internet voting is an attractive target for variously motivated attackers. Hence, it is necessary to analyze the current risk situation and design the appropriate measures against the emerging threats.

This talk consists of two parts. First, we will give an overview of the attack-tree based risk model of Estonian (electronic) voting system, and in the second part we will propose basic principles of vote verifiability to be used during the next Estonian elections. This is a joint research together with Sven Heiberg.

Speaker: Denise Demirel
Title: A publicly-verifiable mix-net with everlasting privacy towards observers
Abstract:
Mix-nets are of interest for several applications where privacy plays an important role like, for instance, eVoting and electronic mail services. Important for their use in application with high requirements regarding integrity, is that the whole process can be verified by any third party. Therefore, all recent variations of mix-nets publish additional information to allow verification of its correct functioning by any observer. This information is encrypted using some public key algorithm (often ElGamal or Paillier) based on number theoretic problems which are assumed to be computationally hard. However, attacks like brute-force that consists of simply checking all possible solution would still be successful (although a computational limited attacker needs decades).

In this talk I present a novel, publicly verifiable mixing scheme which has everlasting privacy towards observers: all the information published on the bulletin board by the mixes (audit information etc.) reveals no information about the identity of any of the messages published. The correctness of the mixing process is statistical: even if all authorities conspire, they cannot change the contents of any message without being detected with overwhelming probability.

Speaker: Matthijs Melissen
Title: Virtual Multi-Protocol Attacks in Non-Repudiation Protocols
Abstract: We give a formal definition of the security property of non-repudiation, and study which conditions this definition must contain. It is well-known that agents need to restrict the use of their key material to a limited set of protocols if multiple security protocols are executed in parallel. We identify an additional requirement, which states that agents should also know about other agents which keys are used for which protocols. When this requirement is not satisfied, a new class of attacks, called virtual multi-protocol attacks, arises. In such attacks, the adversary executes a protocol honestly, and afterwards falsely denies that he has been executing this protocol, abusing the lack of knowledge of the attacked agent. Virtual multi-protocol attacks can be prevented by having the public key infrastructure not only link keys to agents, but also to the protocol for which the key is used.

Speaker: Olivier Roux
Title: Hybrid Modelling of biological systems for the accurate analysis of their timing features
Abstract:
We want to study complex dynamical biological systems but the knowledge we can have of these systems is weak, and it mainly relies upon observations of their behaviours. For this purpose, models are built according to various approaches, and they are accompanied with many parameters that have to be introduced in order to stand for a priori unknown values. We are mostly involved in the logical modelling approach (a la René Thomas) where we want to bring in the temporal dimension. This leads to a hybrid representation which is much intricate. As a matter of fact, we have to face the problem of dealing with models with a lot of parameters and frequently a rather huge or even sometimes unmanageable number of states. For this reason, we introduce a new approach that avoids the computation of the whole states space.

It applies naturally on Gene Regulatory Networks (GRN) which is one of these biological systems we want to study and we shortly introduce their dynamics, at first. Then, we present a new stochastic π-calculus framework, namely the Process Hitting. From this framework, we start a sequence of consistent analyses which deal with both stochastic and temporal aspects and reveal important features of the studied biological system.

The first result is that it makes it possible to check structural properties such as the set of stable states, discrete parameters identification, specification of cooperative actions of associated genes for their coordinated interaction, and so on... As a matter of fact, it appears that very large GRNs can now be studied since such a method avoids building the actual states graph. We show that we are able to take into account a regulatory network of at least twenty genes, which means a graph of 2^66 states!

The second stage of our approach consists in benefiting from the ability of using the stochastic π-calculus in order to execute simulations with stochastic rates. We recall that these rates stand for the time delays for an interaction to take place. This allows us to tune stochastic and temporal parameters so that we can implement temporal properties. We are able to perform these simulations using SPIM, which is an implementation of the stochastic π-calculus. Furthermore, since the translation of the aforementioned Process Hitting in the language of the probabilistic model-checker PRISM is also very easy, we are able to achieve formal verification of the temporal properties that have emerged from the previous phase of the temporal parameters tuning.

Along the talk, we sketch some elements of our method through a tiny toy example.

Speaker: Mohammad Hassan Habibi
Title: RFID Systems: Introduction, Authentication, and Privacy Issues
Abstract: The development of RFID systems in sensitive applications such as e-passport, e-health, credit cards, and personal devices, makes it necessary to consider the related security and privacy issues in great detail. In this presentation, we have an introduction to RFID systems and review their components, standards, communication characteristics, and applications. Then, we investigate RFID authentication protocols and their primitives, security requirements, and vulnerabilities. Next, we focus on formal privacy analysis of RFID authentication protocols and explain an RFID privacy model and its notions. A recently proposed RFID authentication protocol is also analyzed in this model and its security and privacy flaws are shown. Finally, some suggestions to improve the analyzed protocol are presented.

Speaker: Alexandre Bartel
Title: About ByteCode Static Analysis and Manipulation for Android Security
Abstract: Android based devices are becoming widespread. As a result and since those devices contain personal and con?dential data, the security model of the Android has been analyzed extensively. We present how bytecode static analysis and manipulation can help secure Android applications. First, we present the permission model of the Android system as well as the permission gap problem, i.e., when an Android application declares more permissions than required. Second, we show that it's feasible, in a reasonable amount of time, to apply static analysis approaches directly on Android smartphones. Finally, we explain how what we have learned could be used to develop new approaches, working directly on the smartphone, for instance to detect malwares.

Speaker: Stephan Neumann
Title: Civitas and the Real World: Problems and Solutions from a Practical Point of View
Abstract: In the past, researchers have proposed many cryptographic voting schemes that satisfy a wide range of security properties. These schemes often rely on strong trust assumptions and do not consider the voter sufficiently, which currently renders them inappropriate for use in real-world elections. Correspondingly, the voting schemes in use - such as in Estonia - are not based on scientific proposals, but rather rely on own proposals that are usable and easy to understand, but provide less security. In order to ensure democracy while relying on electronic voting schemes, it is important to close the gap between theory and practice. As a prime example, in this talk we focus on the cryptographic voting scheme Civitas, which features provably strong security properties, such as end-to-end verifiability and coercion-resistance. We identify strong trust assumptions and usability weaknesses of the scheme, which currently prevent its usage in real-world elections. Based on these results, we show how most of these strong trust assumptions can be implemented. In addition to other techniques, we propose the use of smart cards in order to overcome Civitas' most critical usability problem, namely credential handling. Together with a voter-process description and the corresponding user-interface, we pave the way for the use of Civitas in real-world elections.

Speaker: Kostas Chatzikokolakis
Title: Differential Privacy vs Quantitative Information Flow
Abstract:
Differential privacy is a notion that has emerged in the community of statistical databases, as a response to the problem of protecting the privacy of the database's participants when performing statistical queries. The idea is that a randomized query satisfies differential privacy if the likelihood of obtaining a certain answer for a database x is not too different from the likelihood of obtaining the same answer on adjacent databases, i.e. databases which differ from x for only one individual.

Information flow is an area of security concerned with the problem of controlling the leakage of confidential information in programs and protocols. Nowadays, one of the most established approaches to quantify and reason about leakage is based on the Renyi min entropy version of information theory.

In this talk, I will analyze the notion of differential privacy in light of the conceptual framework provided by the Renyi min-entropy. I show that there is a close relation between differential privacy and leakage, due to the graph symmetries induced by the adjacency relation. Furthermore, I will discuss the utility of the randomized answer, which measures its expected degree of accuracy, and in particular certain kinds of utility functions called "binary", which have a close correspondence with the Renyi min mutual information. Again, it turns out that there can be a tight correspondence between differential privacy and utility, depending on the symmetries induced by the adjacency relation and by the query. I will discuss how, depending on these symmetries, we can build an optimal-utility randomization mechanism while preserving the required level of differential privacy.

Speaker: Andrea Huszti
Title: Secure Electronic Applications
Abstract:
Nowadays more and more people use computer to manage their everyday life. There are several electronic systems that require people to fill out a simple or sometimes rather complex questioner and later all the answers are evaluated. These assessment systems bring up serious security issues. Security requirements for different assessment systems are sometimes similar. We propose a universal protocol that possesses all necessary security requirements, such that eligibility, secrecy, anonymity, individual and global verifiability and can be applied for e-exam, e-pollster, e-auction, e-tender and e-vote, as well. Our solution employs blind signature and secret sharing schemes, digital envelope technique and provides receipt on a bulletin board.

In case of micropayment schemes all costs that appear during functioning should be minimized. This also includes the cost of disputes and charge backs that result in penalty for the vendor. We extend PayWord micropayment scheme with payment approval to minimize disputes, charge backs or to avoid attacks that ruin reputation of the vendor. We achieve payment approval with employing a MAC function per a purchase that does not increase time complexity significantly. We give also a formal evaluation in applied pi calculus and prove that our scheme fulfills secure payment authorization, payment approval and secrecy of payment information.

Speaker: André van Cleeff
Title: Physical and Digital Security: Comparison, Combinations & Properties
Abstract:
Automation projects are not always successful. One particular reason for failure is that digital systems have serious security problems that were less apparent in the original physical systems. For example, electronic voting security has proven to be very challenging, and so has digital rights management.

In this thesis we examine the security-relevant differences of physical and digital systems by my means of case studies on voting, rights management, access control and server virtualization. We investigate the strength of combinations of physical and digital security mechanisms and attempt to generalize our results.

Speaker: Jean Lancrenon
Title: Password-Authenticated Key Exchange
Abstract: Password-authenticated key exchange made its initial appearance in 1992, with the encrypted key exchange protocol of Bellovin and Merritt. Since then, the problem has received considerable attention. As an introduction to the topic, I'll present some of the original early approaches to tackling this problem, as they reveal interesting subtleties in designing such a primitive.

Speaker: Wojtek Jamroga
Title: Castelfranchi's View on Trust
Abstract: Cristiano Castelfranchi is a well known social scientist working on the conceptual structure of trust. I am going to present his view on the issue. In particular, Castelfranchi argues that trust is (contrary to the way it is often modeled) not just a subjective probability of "trustworthiness" of the party we may or may not trust. According to him, trust combines beliefs about the party's willingness and ability to help, a decision to entrust, and, finally, the very action of trusting.

Speaker: Pim Vullers
Title: Attribute-based Credentials on Smart Cards
Abstract:
Smart cards have become ubiquitous in our lives. However, most of them are not really smart and just store an unique identifier. Even the smarter ones still rely heavily on unique identifiers. This results in simple traceability of such cards which can lead to detailed files of the users actions and behaviour, interfering with the user's privacy.

To prevent such privacy issues we propose to use attribute-based credentials instead of identity-based solutions. This is possible since most systems only rely on certain attributes instead of the user's identity. For example, when you want to board a train, the system only needs to verify whether you're allowed to or not, based on a ticket or year pass.

In this talk we will have a look at the available technologies which implement an attribute-based credential system: Microsoft's U-Prove, IBM's Idemix, and our own self-blindable credentials. More specific we will discuss our results on the smart card implementations of these technologies. Finally I'll give an demonstration to show how such credentials can be used in practice.

Speaker: Jérôme Dossogne
Title: Linking coercion-freeness and verifiability in Internet Voting schemes
Abstract: Much effort is currently invested in combining coercion-freeness and verifiability in Internet Voting schemes. Under the hypothesis of the continuous presence of an over-the-shoulder attacker, the talk will introduce notions such as Multi-Party Designated Verifier Signature and Mental Booth. Additionally, we will present an interactive proof of correct encryption and a special encryption scheme that offers additive homomorphism on both messages and keys. Using those four components, we propose an Internet Voting scheme that supports both properties.

Speaker: Rosario Giustolisi
Title: WATA4.0: Enhancing WATA anonymous marking system with usability and individual verifiability
Abstract: In public competitions or university exams, candidates have to trust the examiner to mark fairly. The same requirement also applies when the competition adopts the known double envelope method. To rebalance that trust, candidate authentication should be achieved together with anonymity during the marking. WATA achieves this contradictory combination in various forms since its first release. Additional requirements are auditability, verifiability and usability. In particular, to meet the last, the system should be managed remotely. The current version, WATA3, meets some of these requirements, but is also found to suffer some serious weaknesses. Thus, a novel version, WATA4, is advanced to achieve all of the desired requirements.

Speaker: MohammadReza Mousavi
Title: In Processes, We Believe! -- On Marrying Process Algebra and Epistemic Logic
(Result of joint work with: Francien Dechesne, HamidReza Mahrooghi and Simona Orzan)
Abstract:
Process algebras, on one hand, provide a convenient means for specifying protocols. Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties of such protocols (e.g., anonymity or secrecy). These two approaches to specification and verification have so far developed in parallel and one has either to define ad-hoc correctness criteria for the process-algebraic model or use complicated epistemic models to specify the behavioral aspects. We work towards bridging this gap by proposing a combined framework which allows for modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic which combines temporal and epistemic operators.

Further, we report on an extension of this framework with cryptographic construct and its influence on the epistemic aspects and conclude with a brief comparison of our semantic framework with the interpreted systems model of Fagin and Vardi.

This talk does not assume any pre-knowledge of either of the two fields (and in particular of process algebras).

Speaker: Evangelos Rekleitis
Title: Beyond Single RFID Authentication Protocols: Anonymous and Forward Secure Grouping Proof Protocols
Abstract: In an actively investigated field; as RFID security, there can still exist terrae incognitae awaiting further exploration. Off-line (verifiable) grouping-proof protocols appear to be one such 'less explored' land. While the generation of proofs of existence, under the persistent presence of a verifier, doesn't pose (m)any difficulties -- one simply needs to execute an RFID authentication protocol for every group member --, their generation in an off-line mode becomes challenging. In this talk, I will discuss some novel results, of an ongoing research, on the creation of existence proofs for tag groups. Based on previously published work on holistic RFID security protocols, a set of important security goals and requirements will be put down, followed by an overview of existing solutions. Further, I will present a new anonymous & forward secure grouping-proof protocol family, along with an open discussion on its shortcomings and the existence (or not) of a formal proof of security.

Back to SRM presenations.

Contact

For questions and comments contact Barbara Kordy or Jean Lancrenon.