TCS / Current / Theoretical Computer Science Forum / Autumn 2006
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

Theoretical Computer Science Forum

Autumn 2006

This is a forum for talks on theoretical computer science organized by the TCS Laboratory at HUT. We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science building. Any exceptions to this rule are reported below.

The talks given at TCS Forum aim at presenting recent advances in theoretical computer science that can be expected to attract interested audience also beyond the research groups of the laboratory. The Friday afternoon time slot is occasionally used also for presentations about ongoing work and results from student's projects at what is called as TCS Lounge. The main goal of the TSC Lounge is to improve transfer of knowledge and ideas between the different research groups of the TCS laboratory.

For further information, please contact Kaisa Nyberg.


Program

Forthcoming presentations

  • 12.1.2007 FORUM Juhani Hyvärinen, Säteilyturvakeskus (STUK) :

    Ydinvoimalaitosten automaatio ja sen viranomaisvalvonta

    Abstract: tba


Past presentations

  • 8.12.2006 FORUM Dr. Keijo Heljanko (TCS/TKK):

    Bounded Model Checking for Weak Alternating Büchi Automata

    Abstract: We present an incremental bounded model checking encoding into propositional satisfiability where the property specification is expressed as a weak alternating Büchi automaton (WABA). The encoding is linear in the specification WABA transition relation size. Minimal length counterexamples can also be found by increasing the encoding size to be quadratic in the number of states in the largest component of the WABA. The proposed encoding can be used to implement more efficient bounded model checking algorithms for omega-regular industrial specification languages such as Accellera's Property Specification Language (PSL). Encouraging experimental results on a prototype implementation are reported. This is joint work with Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala.

  • 23.11.2006 FORUM Prof. Fabio Massacci (Università di Trento) :

    Security by Contract
    Or How to Use Automated Reasoning for Boosting Security of Mobile Code

    Abstract: There is increasing demand for running multiple times a number of interacting applications in a secure and controllable way on mobile devices. Such demand is not supported by the Java/.NET security models based on trust domains nor by current security monitors or language-based security approaches. Trust domains don't allow for interactions while language-based security doesn't support enough customizable policies. I will argue for the notion of security by contract where a contract is a claim by a mobile application on the interaction with relevant security and privacy features of a mobile platform. This contract should be published by applications, understood by devices and all stakeholders (users, mobile operators, developers, platform developers, etc.). The contract should be negotiated, and enforced during development, at time of delivery and loading, and during execution of the application by the mobile platform. A careful analysis of the security requirements in the booming domain of mobile games reveals that most practical security requirements can be represented with an enhanced notion of pure past temporal Logic augmented with the intuitive notion of session. We propose an approach that allows security policies that are i) expressive enough to capture multiple sessions and interacting applications, ii) suitable for efficient monitoring, iii) convenient for a developer to specify them. Since getting all three at once is impossible, we advocate a logical language, 2D-LTL a bi-dimensional temporal logic fit for multiple sessions and for which efficient monitoring algorithms can be given, and a graphical language based on standard UML sequence diagrams with a tight correspondence between the two. This work is a part of a collaborative European Project S3MS .

  • 23.11.2006 FORUM Prof. Bart Preneel (Katholieke Universiteit Leuven, Dept. Elektrotechniek-ESAT /COSIC) :

    Cryptanalysis of ABC and Py

    Abstract: In this talk attacks on two eSTREAM Phase 2 stream ciphers will be presented. The first attack is on ABC v2 and v3 (joint work with Hongjun Wu). The second attack is on Py (joint work with Souradyuti Paul).

  • 17.11.2006 LOUNGE Sven Laur, TCS/TKK :

    Black-Box Knowledge Extraction Revisited

    Abstract: Rewinding techniques form the essence of many security reductions including proofs for identification and signature schemes. We propose a simple and modular approach for the construction of such proofs. Straightforward applications of our central result include, but are not limited to, the security and soundness of identification schemes, generic signatures and ring signatures. These results are well known, however, we generalise them in such a way that our technique can be used off-the-shelf for future applications. We note that less is more: as a side-effect of our less complex analysis, all our proofs are more precise; for example, we get a new proof of the forking lemma that is 2^15 times more precise than the original result by Pointcheval and Stern. Secondly, we establish some outstanding results about "fast" knowledge-extraction that forms the core of tight security proofs for many generic signature schemes. However, these techniques are applicable in many different contexts. For example, they can be used in precise security analysis of Blum's coin flipping protocol with long string commitments.

  • 10.11.2006 LOUNGE Mikko Särelä, TCS/TKK :

    Defence against wormhole attacks

    Abstract: In ad hoc networks, a wormhole attack creates a false image of the network topology to the participating nodes by relaying hello and routing messages between two or more nodes, and thus making them believe they are neighbors. It is an especially efficient for mounting Denial-of-Service attacks as it can be mounted without any knowledge of cryptographic keys or shared secrets. In this talk, we explore a method to verify the physical closeness of two nodes by measuring the time delay of a response to a challenge. We calculate an upper bound on the distance by measuring the return round trip delay of a challenge and removing the lower bound estimates of processing and transmission delays from the result, and then discuss the deployability of the protocol.

  • 22.9.2006 FORUM Alexandre Duret-Lutz, Laboratoire d'Informatique de Paris 6 :

    Generalized Emptiness Checks: Survey and Extensions

    Abstract:"Emptiness check" is a key operation in the automata-theoretic approach to LTL verification. Usually, it is done on Büchi automata with a single acceptance condition. In this talk, we review existing on-the-fly emptiness check algorithms for generalized Büchi automata (i.e., with multiple acceptance conditions) and show how they compete favorably with emptiness checks for degeneralized automata, especially in presence of weak fairness assumptions. Then we introduce two extensions of one of these algorithms (Couvreur's):

    • One modification of the algorithm allows us to check Streett automata, a must-have to support strong fairness assumptions.
    • Another variation deals with a class of generalized Büchi automata whose states represent sets that may include each other. We illustrate this with a symmetry-based reduction of the state space. Here the new algorithm use inclusion checks to help direct and further reduce the on-the-fly construction of the state space.

  • 20.9.2006 FORUM Dr. Stefan Woltran: Technical University of Vienna

    Replacements in Non-Ground Answer-Set Programming

    Abstract: In this work, we study replacements in nonmonotonic logic programs within the answer-set programming paradigm. Of particular interest are replacements retaining specific notions of equivalence, among them the prominent notions of strong and uniform equivalence, which have been introduced as theoretical tools for program optimization and verification. The main contribution of this work is to generalize results about particular replacement schemas which have been established for ground programs to the non-ground case. As well, we report a number of complexity results which address the problem of deciding how hard it is to apply a replacement to a given program. Our results provide an important step towards the development of effective optimization methods for non-ground answer-set programming, an issue which has not been addressed much so far.

  • 8.9.2006 FORUM Henrik Petander (National ICT Australia) :

    Network Mobility in IPv6

    Abstract: "Measuring the performance of an implementation of a set of protocols and analyzing the results is crucial to understanding the performance and limitations of the protocols in a real network environment. Based on this information, the protocols and their interactions can be improved to enhance the performance of the whole system. To this end, we have developed a network mobility test bed and implemented the NEMO Basic Support Protocol and have identified problems in the architecture which affect the handoff and routing performance. The identified handoff performance issues affect both Mobile Hosts and Routers and they can be addressed through infrastructure or Mobile Router based solutions. On the infrastructure side, Fast Handovers for Mobile IPv6 can be used to improve handoff performance of Mobile Hosts and Routers. Based on the Fast Handovers framework we have designed a new protocol, SafetyNet, which enables seamless horizontal and vertical handoffs. Infrastructure support is not likely to exist in all cases due to legacy equipment or the networks being run by different operators. In such a network environment, a Mobile Host or Router can still achieve near seamless handoff performance by utilizing Make-Before-Break handoffs with two network interfaces. We complement this seamless handoff architecture with a route optimization scheme, OptiNets, which reduces the overheads of NEMO to a level comparable with Mobile IPv6 route optimization. Together these performance improvements address the main shortcomings of NEMO, the handoff performance and suboptimal routing paths."

  • 1.9.2006 FORUM Alexander Maximov (University of Luxemburg) :

    Modern trends in design and cryptanalysis of stream ciphers

    Abstract: In the world of cryptography, stream ciphers are known as primitives used to ensure privacy over a communication channel. Although the idea of such constructions is known since the middle of the last century, a serious investigation of stream ciphers has just started around 20 years ago. The use of various construction blocks in these primitives has always been evaluating, from Boolean functions till currently attractive nonlinear feedback shift registers. Cryptanalysis techniques of such construction blocks have been accumulated from various research results, helping people to choose building blocks for stream ciphers properly. In recent years, many designs of stream ciphers have been proposed in an effort to find a proper candidate to be chosen as a world standard for data encryption. It also includes the work done during two European projects NESSIE and eSTREAM. That potential candidate should be proven good by time and by the results of cryptanalysis. In fact, different methods of analysis explain how a stream cipher should be constructed. Therefore, techniques for cryptanalysis are important. In this seminar, we will focus on two principles for construction of stream ciphers: primitives based on linear and nonlinear feedback shift registers, such as SNOW 2.0 , Grain, and Trivium. Various linear cryptanalysis techniques will be considered, such as distinguishing and correlation attacks. In relation to practical bottlenecks in cryptanalysis, a class of pseudo-linear functions will be introduced. The importance of fast Fourier and Hadamard transforms in cryptanalysis will be shown.

  • 11.8.2006 André Schumacher (TCS/TKK) :

    Optimization Algorithms for Multihop Wireless Networks

    Abstract: Due to their wireless and decentralized nature, multihop wireless (ad hoc) networks are attractive for a variety of applications. However, these properties also pose significant challenges to their developers. As they are unable to rely on a centralized entity, ad hoc network nodes have to cooperate in a distributed and self-organizing manner. Additional side constraints, such as energy consumption, have to be taken into account as well. We are interested in the application of distributed optimization algorithms to ad hoc networks. The goal is to optimize objectives, such as energy consumption or end-to-end throughput, within a general framework based on formulations as linear or convex optimization problems. As a case study we consider the application of a distributed flow balancing algorithm to ad hoc networks for throughput maximization. The algorithm is non-heuristic and works on a linear program formulation of the problem. It is implemented as an extension to the DSR routing protocol and its performance is evaluated using the ns2 network simulator. The preliminary results indicate that the approach results in improvements compared to the standard DSR implementation.


[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 09 December 2006. Kaisa Nyberg