SRM seminar

SaToSS home

• Related seminars
• SRM
• SRM 2023
• SRM 2022
• SRM 2021
• SRM 2020
• SRM 2019
• SRM 2018
• SRM 2017
• SRM 2016
• SRM 2015
• SRM 2014
• SRM 2013
• SRM 2012
• SRM 2011
• SRM 2010
• SRM 2009
• Seminar Rules

Abstracts 2009

• Speaker: Mohammad Torabi Dashti
• Title: Super-strings and multi-party contract signing
• Abstract: Problems related to scattered/consecutive super string of a set of strings are reviewed. A number of these (open) problems have direct applications in designing and verifying efficient multi-party contract signing protocols. Some tentative ways to approach these problems are discussed.

• Speaker: Chenyi Zhang
• Title: Information Flow in Systems with Schedulers
• Abstract: The focus of work on information flow security has primarily been on definitions of security in asynchronous systems models. This work considers systems with schedulers, which require synchronous variants of these definitions. In particular, it studies the dependence of these variant definitions of security on implementation details of the scheduler. Such independence is shown to hold for synchronous variants of trace-based definitions, but not for bisimulation-based definitions.

• Speaker: Peter Ryan
• Title: Pret a Voter a la Florentina
• Abstract: Pret a Voter 2006 uses re-encryption mixes and cyclic shifts of the candidate order. This is a little fragile in that an adversary has a systematic way to shift votes. I show how we can introduce the idea of Florentine squares to enrich the set of permutations that can be handled and counter the vote shifting attack.

• Speaker: Gerardo and Pim
• Midterm presentation of Master's thesis work

• Speaker: Barbara Kordy
• Title: A Rewrite Approach for Tree Pattern Containment
• Abstract: XPath is a language for navigating an XML tree and selecting a set of element nodes. Due to the wide use of XPath, which is embedded into several languages for querying and manipulating XML documents, the problem of efficiently answering XPath queries has received an increasing attention from the research community. The time required for the evaluation of an XPath query depends on its size, thus the possibility of replacing a given query by an equivalent one having the smallest size is essential form the point of view of complexity. On the other hand, query equivalence is simply two-way query containment.

  In this talk, we focus on a class of purely descendant XPath queries modeled with tree patterns. We propose to handle the query containment problem by using a rewrite approach. We introduce a system of rewrite rules based on the semantics of query containment, and show that for any two queries P and Q, P is contained in Q if and only if the pattern representing P can be rewritten to the pattern representing Q using these rules. This provides a new algebraic characterization of the query containment problem. Moreover, such a rewrite view gives us a uniform framework to treat also other problems, for instance query evaluation.

• Speaker: Ton van Deursen
• Title: Undecidability of checking security protocols
• Abstract: Security protocols are difficult to design and to verify for a variety of reasons. One of the reasons is that the security problem, i.e. deciding whether there exists an attack on a protocol, is undecidable. However, placing restrictions on (the size and structure of) protocols and protocol analysis may lead to decidable classes of security protocols, allowing automation of protocol verification. It is therefore important to find which classes of restrictions lead to decidability of the security problem.

  In this talk, I will present an undecidability result obtained by Kuesters and Truderung. They adopt the Dolev-Yao model of protocol execution, and prove that extending it with XOR leads to undecidability of the security problem. I will conclude by presenting related work with respect to (un)decidability of security protocols.

• Speaker: Xihui, Xin, and Ying
• Midterm presentation of Master's thesis work

• Speaker: Erik de Vink
• Title: Architecting Security with Paradigm
• Abstract: For large security systems a clear separation of concerns is achieved through architecting. Particularly the dynamic consistency between the architectural components is addressed, in addition to individual component behaviour. In this talk, the relevant coherence is specified by Paradigm, a coordination modeling language based on dynamic constraints. As it is argued, this fits well with security issues. A smaller example introduces the architectural approach towards implementing security policies. A larger casestudy illustrates the use of Paradigm in analyzing the FOO voting scheme. Translation of the Paradigm models into process algebra brings model checking within reach.

  Joint work with Suzana Andova, Luuk Groenewegen and Jan Verschuren.

• Speaker: Hugo Jonker
• Title: Nuovo DRM: Introducing Fair Exchange in DRM
• Abstract: We introduce Nuovo DRM, a digital rights management scheme aimed to provide formal and practical security. The scheme is based on a recent DRM scheme, which we formally specify in the mCRL process algebraic language. The original scheme stated the following security requirements: effectiveness, secrecy and resistance of content masquerading. We formalise these security requirements as well as strong fairness and formally check the original scheme against these requirements. This verification step uncovered several security weaknesses, which are addressed by Nuovo DRM. In addition to that, Nuovo DRM introduces several procedural practices to enhance the practical security of the scheme. A finite model of Nuovo DRM is subsequently model checked and shown to satisfy its design requirements, including secrecy, fairness and resistance to content masquerading.

• Speaker: Chenyi Zhang
• Title: How to Work with Honest but Curious Judges?
• Abstract: this talk presents an ongoing work about implementing a majority function with respect to anonymity. The protocol describes how to let 3 judges cast their vote -- such that the final verdict is guilty if and only if at least 2 vote for guilty, and in most cases each judge has no knowledge about the other two's votes.

• Speaker: Sasa Radomirovic
• Title: More on honest, but curious, judges
• Abstract: I will discuss several solutions to the judges problem introduces last week by Chenyi.

• Speaker: Baptiste Alcalde
• Title: Model-driven Fuzzing
• Abstract: In this talk, I will discuss under which conditions and how to use common testing techniques in the context of fuzz security testing.

• Speaker: Peter Ryan
• Title: OpenVeto and OpenVote
• Abstract: I will describe a "boardroom" style voting protocol that allows someone to anonymously cast a veto using only public channels. I then describe how this can be adapted firstly to a password authenticated key establishment protocol and then to a full voting protocol.

  Joint work with Feng Hoa and Piotr Zielinski

• Speaker: Hongyang Qu
• Title: MCMAS: A model checker for the verification of multi-agent systems
• Abstract: We present MCMAS, a symbolic model checker specifically tailored for agent-based specifications and scenarios. MCMAS supports specifications based on Computational Tree Logic (CTL), epistemic logic (including operators of common and explicit knowledge), Alternating Time Logic (ATL), and deontic modalities for correctness. The model input language includes variables and basic types and it implements the semantics of interpreted systems thereby naturally supporting the modularity present in agent- based systems. MCMAS implements Ordered Binary Decision Diagram (OBDD)-based algorithms optimised for interpreted systems and supports fairness, counter-example generation, and interactive execution (both in explicit and symbolic mode). It has been tested in a variety of scenarios including web-services, diagnosis and security. MCMAS comes with a GUI aimed at assisting the verification process.

• Speaker: Osman Akcatepe
• Title: Polarization Mode Dispersion and Chromatic Dispersion in Quantum Cryptography
• Abstract:
  1. A short introduction to Quantum Cryptography
  2. Some physical terms, definitions,...etc. relating the presentation.
  3. Chromatic Dispersion
  4. Polarization Mode Dispersion
  5. Comparison of Chromatic Dispersion and Polarization Mode Dispersion
  6. Conclusion

• Speaker: Sasa Radomirovic
• Title: Wallets
• Abstract: This talk is related to a question originally posed by Jan Bergstra.

  Consider three persons with a certain number of Euro coins in their wallets. Suppose they want to exchange some of their coins such that after the exchange everybody has the same amount of money he or she had before the exchange, but different coins. Can each such exchange be achieved through a series of pairwise exchanges? If not, what is the smallest example of an exchange that requires that all three persons simultaneously exchange coins?

  I will answer one of these questions and pose several open questions related to this problem.

• Speaker: Sjouke Mauw

• Speaker: Pim Vullers
• Title: Secure Ownership and Ownership Transfer in RFID Systems
• Abstract: I will present a verification framework for ownership related security requirements as well as two ownership transfer protocols designed with these requirements in mind.

• Speaker: Patrick Schweitzer
• Title: Accelerating Average Consensus - Weight Choosing with the Symprio Algorithm
• Abstract: The talk will be about distributed (e.g. local) algorithms which aim to reach a consensus in a wireless sensor network. One of the possible aims of these algorithms is to reach the average of sensor measurements in all sensors at the same time. The talk will be based upon my diploma thesis which first surveys state-of-the-art average consensus algorithms and then improves upon a special type of algorithm: the linear weight adjustment (LWA) algorithms. These LWA-algorithms will be explained using the basic Metropolis-Weights algorithm. After that the acceleration given by the linear weight choosing using Symprio weights will be explained and numerically shown.

• Speaker: Delphine Longuet
• Title: Testing from Logical Specifications: Proof-guided Test Selection
• Abstract: Testing is one of the most used method for the validation of software. When the implementation of the system under test is not known, the test cases to submit to the system can be selected and generated from a formal specification. Classically, logical (algebraic) specifications are used to test functional aspects of programs (data) while transition systems are used to test the dynamic and reactive behaviour of systems (actions and communications).

  I will first introduce the framework for testing from algebraic specifications, in particular the test case selection method called axiom unfolding. The principle of this method is to use proof techniques to guide the selection of test cases, which are built as derivations of the specification axioms. I will then show how this framework can be adapted and extended to first-order modal specifications, in order to provide a logical framework for testing the dynamic and reactive behavior of systems.

• Speaker: Ben Smyth
• Title: Automated reasoning for election verifiability in electronic voting protocol
• Abstract: I will present the first definition of election verifiability for electronic voting protocols. The definition is presented in terms of reachability assertions using the applied pi calculus and is amenable to automation using ProVerif. The definition allows sufficient voter capabilities to be established for election verifiability when using hostile computer systems. More precisely the voter is assumed to vote using Satan's computer. This paradigm also provides a benchmarking tool to compare the degree of election verifiability offered by protocols. The applicability of our methodology is demonstrated by analysing the protocols due to Fujioka, Okamoto & Ohta and Juels, Catalano & Jakobsson.

• Speaker: Peter Ryan
• Title: Pretty Good Democracy
• Abstract: I describe an internet voting scheme that takes ?code voting? as its starting point but adds a degree of end-to-end verifiability. The scheme contrasts with the VeryVote scheme presented at VoteId 2009 in that it proved receipt-freeness.

  Joint work with Vanessa Teague, Melbourne.

• Speaker: Tim Muller
• Title: The Expressivity of Kleene star in Process Algebras with the Empty Process
• Abstract: Let BPA*0, PA*0 and ACP*0 be the process algebras Basic Process Algebra, Process Algebra and Algebra of Communicating Processes extended with the Kleene star (*) and deadlocking (0). Bergstra, Bethke and Ponse proved in 1994 that BPA*0 is less expressive than PA*0, and that PA*0 is less expressive than ACP*0. We further extend BPA*0, PA*0 and ACP*0 to BPA*0,1, PA*0,1 and ACP*0,1 by addition of the empty process (1). We will derive that BPA*0,1 is less expressive than PA*0,1, and that PA*0,1 is less expressive than ACP*0,1.

• Speaker: Ying Zhang
• Title: Game-Based Verification of Multi-Party Contract Signing Protocols
• Abstract: A multi-party contract signing (MPCS) protocol is used for a number of signers to sign a digital contract over a network. We analyse the protocols of Mukhamedov and Ryan (MR), and of Mauw, Radomirovic and Torabi Dashti (MRT), using the finite-state model checker Mocha. Mocha allows for the specification of properties in alternating-time temporal logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives us an intuitive interpretation of the verification problem of crucial properties of MPCS protocols. We analyse the MR protocol with up to 5 signers and our analysis does not reveal any flaws. MRT protocols can be generated from minimal message sequences, depending on the number of signers. We discover an attack in a published MRT protocol with 3 signers, and present a solution for it. We also clarify Mauw, Radomirovic and Torabi Dashti's methodology of designing MRT protocols using minimal message sequences. We design a number of MRT protocols for 3 and 4 signers according to the clarified methodology and verify all of them in Mocha. We detect a flaw against abuse-freeness in MRT protocols and give a simple fix.

• Speaker: Xihui Chen
• Title: Improving automatic verification of security protocols with XOR
• Abstract: Kusters and Truderung recently proposed an automatic verification method for security protocols with exclusive or (XOR). Their method reduces protocols with XOR to their XOR-free equivalents, enabling efficient verification by tools such as ProVerif. Although the proposed method works well in verifying secrecy for a large class of protocols, for verification of authentication properties the class gets smaller and moreover, the verification is inefficient sometimes.

  In this thesis, we improve the work by Kusters and Truderung in two ways. First, we extend their method for authentication verification to a richer class of XOR-protocols by automatically introducing bounded verification. Second, we improve the efficiency of their approach by developing a number of dedicated optimizations. We show the applicability of our work by implementing a prototype and applying it to both existing benchmarks and RFID protocols. The experiments show promising results and uncover a flaw in a recently proposed RFID protocol.

• Speaker: An Xin
• Title: Model Checking Round-Based Distributed Algorithms
• Abstract: In the field of distributed computing, there are many round-based algorithms to solve fundamental problems, such as leader election and distributed consensus. Due to the nature of these algorithms, round numbers are unbounded and can increase infinitely during executions of the algorithms. This can lead to the state space explosion problem when verifying correctness of these algorithms using model checking.

  In this thesis, we present a general idea of investigating the relations of round numbers in round-based algorithms. We can manage to transform their state spaces into finite by maintaining such relations in a proper way, and thus make (fully) automatic verification of these algorithms possible. We apply this idea to several algorithms (including a new proposed algorithm in the thesis) and verify the correctness of them by using model checker Spin.

• Speaker: Graham Steel
• Title: Formal Analysis of Security APIs
• Abstract: A security API is the interface between a trusted component, such as a smartcard or tamper-resistant cryptoprocessor, and an untrusted component, such as a desktop PC. Such APIs are designed so that no matter what sequence of commands the untrusted component sends, certain security properties, such as secrecy of sensitive keys, will continue to hold. Over the last few years many attacks on such APIs have been found. Our recent research has involved applying methods for formal security analysis to security APIs. This talk will discuss attacks, our analysis approach, the results, and the outstanding problems.

• Speaker: Barbara Kordy
• Title: Verifying Security Protocols using Term Rewriting Techniques
• Abstract: The talk will give an introduction to how term rewriting techniques are used in the verification of security protocols. It is based on a paper by Jacquemard, Rusinowitch, and Vignerone.

• Speaker: Robert Carter
• Title: Location Aware Multifactor Authentication
• Abstract: Global Navigation Satellites Systems (GNSS) such as GPS are used in security systems to provide firstly a further authentication factor to existing and future transaction based systems. Secondly, GNSS is used for establishing if the place of the transaction matches with the position of an electronic mobile device associated with the authorised person at the time of the transaction to enable the secure authentication of the transaction.

  Furthermore a unique identifiable code or device DNA is sequenced from the device's embedded hardware and communication characteristics and combined with GNSS data to ensure the integrity of the device.

  These systems can be used in various domains but hitherto has been applied for use in credit card transaction processing. Herein the device switches a credit card into a ?transaction enabled? mode and during such state the location of the device can be established and compared to the location from where the request originates. This, in addition, needs to correspond with the place where the merchant is entitled to accept such card as well.

  This application a.k.a IPAYMO has won several awards and is currently part of the ESA Technology Transfer Programme and is incubated in ESA?s technology centre in Darmstadt (DE). It is partly funded through the Luxembourg Industrial Incentive Fund (LIIS) and by an industrial partner. A demonstrator is being built as part of the incubation project with the assistance of satellite navigation experts from ESOC, the ESA Space Operation Centre in Darmstadt.

• Speaker: Patrick Schweitzer
• Title: On Attack / Defense Trees
• Abstract: When modeling attacks on systems, the intuitive solution rapidly becomes infeasible. Hence there is a need for computer support, which requires a mathematical framework. We present one of the current approaches: "Attack Trees."

  We explain why there is a need for further expansion. For this expansion, the Attack / Defense Trees, we define a structure, give semantics, and deduce transformation rules to obtain a unique normal form. Then we outline the current difficulties in streamlining the approach.

• Speaker: Sjouke Mauw
• Title: Secret Santa protocols
• Abstract: Secret Santa is a traditional event which is known in many western countries under different names (Chris Kindle, Kris Kringle, Sinterklaassurprises). In this tradition members of a group are randomly assigned other members to whom they anonymously give a gift. A short literature study indicates that this problem has not been studied before in security protocol literature. In my talk I will propose a definition of the Secret Santa problem and I will sketch some solution directions. The purpose of the presentation will not be to answer questions but to initiate a discussion on possible solutions.

• Speaker: Gabriele Lenzini
• Title: Trust-Enhanced Security: Applying Trust Management in Systems' Security, Examples
• Abstract: In this talk we discuss, helped by a few examples, how trust management concepts can be used in the design of systems and of their security features. After recalling the basic structure of a general trust management solution, we will discuss an instance of it in the design of a middleware for a high level of security-assurance in embedded, component-based, devices. In the same time we recall a few concepts utilized in measuring software components' trustworthiness using Subjective Logic. In a second part we discuss an application of trust management in the design of an infrastructure for context- awareness. Here, trust measurement is the base of an evaluation of the belief that the system has in the presence of an identity in a certain location. This engine brings to the realization of a trust- based indoor localization system and, potentially, to a location- aware authentication engine.

Back to SRM presenations.

Contact

For questions and comments contact Saša.