|
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:
- We show that there is a notion of stratification for CC-programs and
we prove that stratified programs have stable models.
- 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.
- 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.
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 09 January 2005.
Ilkka Niemelä
|