Formal Methods Forum

Autumn 2002

This is a seminar on formal methods in computer science and engineering organized by the Laboratory for Theoretical Computer Science at HUT. We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science building.

For further information, please contact Ilkka Niemelä.

Program

• 6.9.2002 Edith Elkind (Princeton): Advanced notions of security for encryption

  Abstract: Encryption schemes are among the most fundamental tools provided by modern cryptography. The most basic level of security we can expect from an encryption scheme is security against a passive adversary (an eavesdropper). However, in many contexts a stronger notion of security is needed, namely, even a more powerful adversary who is allowed to decrypt arbitrary ciphertexts other that the one it is challenged on should be unable to gain any information about the corresponding plaintext. This type of attack is called a chosen-ciphertext attack (CCA). The first public-key encryption scheme provably secure against adaptive chosen-ciphertext attack was given in the pioneering work of Dolev, Dwork, and Naor. In the last few years, two additional results have significantly informed our understanding of provable chosen-ciphertext security. The first was the Cramer--Shoup cryptosystem, which is based on Decisional Diffie--Hellman Assumption and provides the first practical schemes with this level of security. The second was the construction of Sahai, which, while being based on a general (rather than a number-theoretic) assumption, is significantly simpler than that of [DDN]. The latter paper also introduces the notion of simulation-sound zero-knowledge. Although a number of researchers have noticed that certain components of these schemes have a lot in common, the proof techniques of these two works were seemingly very different, and the exact relationship between them was not clear. The main result we are going to present in this talk is a model that unifies both of these constructions, and, more generally, gives rise to a new methodology for constructing CCA-secure encryption schemes. This model, which we call the ``oblivious decryptors model'' produces clean and modular proofs of security, thus significantly simplifying the original proof of [CS98]. Also, it allows for the use of efficient special-purpose simulation-sound NIZK proofs, such as those recently put forward by Cramer and Shoup. In the talk, we show how to represent these schemes as particular cases of our model and sketch the proof of security for the general case.

  (Joint work with Amit Sahai)

• 13.9.2002 Jukka Järvenpää and Marko Mäkelä: Towards Automated Checking of Component-Oriented Enterprise Applications

  Abstract: Building enterprise applications using component-based frameworks has been suggested as a way to help companies manage their software assets. We propose tool support for managing these high-level data-centric applications with formal methods. Our method is based on extracting a system model from the models of components and from the application code which glues the components together. This model is used for generating state spaces that can be checked for desired or undesired properties. In order to manage the state space explosion problem we propose that the application developer controls some parameters of the model. Even though the insight of the application developer is still needed, we believe that creating tool support for the proposed method could contribute to the success of the component-based approach.

• 1.10.2002 Prof. Victor W. Marek (University of Kentucky): On Logic Programs with Cardinality Constraints and Some Generalization
  Note: The talk is held at 14.15 in room TB353.

  Abstract: We investigate cardinality-constraint (CC) logic programs implemented in the ASP solver smodels and prove a number of results as a conceptual explanation of their semantics. Niemela, Simons and collaborators defined a notion of stable model, which we call CC-stable, for CC-logic programs that differs from the usual notion of stable model of logic programs in a variety of ways. For example, it is not always the case that the set of CC-stable models of a CC-program form an anti-chain. One result of this research is to show that there is a natural transformation of a CC-logic program P into a standard logic program Q in an extended language such that the CC-stable models of P are the projections of the stable models of Q to the original language. In addition to our work presented at NMR02, we will discuss several results:

  1. We show that there is a notion of stratification for CC-programs and we prove that stratified programs have stable models.
  2. We show that there is a natural notion of multivalued operator assoviated with a CC-program and that stable models are fixpoints of that operator.
  3. We find that the notion of stable model can be naturally extended to a larger class of programs with, possibly, natural applications.

  (This is joint research with Jeffrey B. Remmel, University of California.)

• 11.10.2002 Dr. Tomi Janhunen: An Approach to Capture Stable Models with Classical Ones

  Abstract: In the talk, I address the relationship of two important ASP formalisms, namely normal logic programs (under stable model semantics) and sets of clauses (under classical models). It is easy to reduce the latter to the former, but translations in the other direction are more or less troublesome. In simple cases (e.g. tight programs addressed by Lifschitz), Clark's program completion does the job, but programs containing positive loops are not necessarily covered. There are also theoretical results indicating that removing positive loops cannot be done in a modular and faithful way. Despite of these difficulties, I present in this talk a non-modular and faithful translation. As distinctive features (compared to earlier approaches) we obtain a bijective correspondence between the models and the size of the translation grows linearly in the length of the input times the logarithm of the number of atoms is the input. I have also developed an implementation of the translation. The results from my preliminary experiments look promising, although the performance of the implementation, used together with a leading sat solver zchaff, is still behind smodels. To conclude, further optimizations are needed to really compete with smodels.

• 25.10.2002 Manel Guerrero Zapata and N. Asokan (Nokia Research Center): Securing Ad hoc Routing Protocols

  Abstract: We consider the problem of incorporating security mechanisms into routing protocols for ad hoc networks. Canned security solutions like IPSec are not applicable. We look at AODV in detail and develop a security mechanism to protect its routing information. We also briefly discuss whether our techniques would also be applicable to other similar routing protocols and about how a key management scheme could be used in conjunction with the solution that we provide.

• 1.11.2002 The public defence of a doctoral thesis (at 12noon, CS building, lecture hall T2)
  Sam Sandqvist: Aspects of Modelling and Simulation of Genetic Algorithms: A Formal Approach

• 8.11.2002 Emilia Oikarinen: On the Equivalence of Logic Programs

  Abstract: To solve a problem in answer set programming, one needs to construct a logic program so that its answer sets correspond to the solutions to the problem at hand. During the development of a program, it is common to have multiple versions of the program that e.g. optimize the execution time or space. The programmer, however, faces a new problem, for it is necessary to ensure that these different encodings yield the same answer sets. To ease this task, we present a method for testing the equivalence of logic programs P and Q. We translate P and Q into a single logic program. The answer sets of the translation (if there are any) yield counter-examples to the equivalence of P and Q. Experiments performed with an implementation of the translation (LPEQ) and SMODELS suggest that in several cases it is faster to establish the equivalence using the translation than to do an explicit cross-check for the answer sets.

  This is joint work with Dr. Tomi Janhunen, who also has implemented the translator LPEQ.

• 15.11.2002 Timo Latvala: On Model Checking Safety Properties

  Abstract: Safety properties are an interesting subset of general temporal properties for systems. In the linear time paradigm, model checking of safety properties is easier than the general case, because safety properties can be captured by finite automata. We discus the theoretical and some of the practical issues related to model checking LTL safety properties. We present an efficient algorithm for translating LTL safety properties to deterministic finite automata. The implementation of the translation algorithm is experimentally evaluated. Experiments corroborate the feasibility of the approach. In many tests the implementation is quite competitive when compared to algorithms translating full LTL to Büchi automata. The implementation also includes a pathologic check for LTL formulae, which according to experiments performs well.

• 29.11.2002 Teemu Tynjälä: Combining Abstractions with Reachability Analysis: A Case Study of the RLC Protocol

  Abstract: Today's telecommunication systems are complex and thus prone to logical errors. Formal methods offer one solution to the design problem of such systems. A formal model of a system may be verified before system's implementation and thus a reassurance of the specification's correctness is obtained. Normally it is impossible to make a verbatim model of a telecom system. The analysis is rendered tractable by the employment of abstractions. When using abstractions, the verification engineer should ascertain that they do not hide inherent features of the system. In this work a UMTS (Universal Mobile Telephony System) radio protocol RLC (Radio Link Control) was verified. RLC is a non-trivial protocol whose specification includes 56 pages of graphical SDL (Specification and Description Language) code. The SDL description of the RLC was manually converted to algebraic Petri Nets. The Petri Net model was enhanced with certain abstractions to alleviate the state explosion. The resulting net was analyzed by the Maria analyzer.

• 13.12.2002 Petteri Kaski: A classification approach for Steiner triple systems and some related combinatorial objects

  Abstract: A Steiner triple system of order v (STS(v)) is a set of triples, called blocks, constructed over a set of v points, such that every pair of distinct points occurs in a unique block. Previously, a complete classification of the nonisomorphic STS(v) was known only for v <= 15. In this talk we describe the computer-aided classification approach that was used to settle the next open case, v = 19. The classification proceeds in two stages. First, we construct an initial set of 25-block seed configurations. Then, using an algorithm for the exact cover problem, we determine all completions of the seeds to STS(19). Isomorph rejection on the STS(19) is carried out using the graph canonical labelling package "nauty" supplemented with a vertex invariant based on Pasch configurations. We also illustrate the applicability of the approach to the classification of some related combinatorial objects, such as 1-factorizations of a complete graph.