Informatica

The DPLL procedure for the SAT problem is one of the fundamental algorithms in computer science, with many applications in a range of domains, including software and hardware verification. Most of the modern SAT solvers are based on this procedure, extending it with different heuristics. In this paper we present a formal proof that the DPLL procedure is correct. As far as we know, this is the first such proof. The proof was formalized within the Isabelle/Isar proof assistant system. This proof adds to the growing body of formalized mathematical knowledge and it also provides a number of lemmas relevant for proving correctness of modern SAT and SMT solvers.

Delegation of rights is a common practice in the real world. We present two identity-based threshold proxy signature schemes, which allow an original signer to delegate her signing capability to a group of n proxy signers, and it requires a consensus of t or more proxy signers in order to generate a valid signature. In addition to identity-based scheme, privacy protection for proxy singers and security assurance are two distinct features of this work. Our first scheme provides partial privacy protection to proxy signers such that all signers' identities are revealed, whereas none of those t participating signers is specified. On the other hand, all proxy signers remain anonymous in the second scheme. This provides a full privacy protection to all proxy signers; however, each valid signature contains a tag that allows one to trace all the participating proxy signers. Both our proposed schemes are secure against unforgeability under chosen message attack, and satisfy many other necessary conditions for proxy signature.

As a means of supporting quality of service guarantees, aggregate multiplexing has attracted a lot of attention in the networking community, since it requires less complexity than flow-based scheduling. However, contrary to what happens in the case of flow-based multiplexing, few results are available for aggregate-based multiplexing. In this paper, we consider a server multiplexer fed by several flows and analyze the impact caused by traffic aggregation on the flows at the output of the server. No restriction is imposed on the server multiplexer other than the fact that it must operate in a work-conserving fashion. We characterize the best arrival curves that constrain the number of bits that leave the server, in any time interval, for each individual flow. These curves can be used to obtain the delays suffered by packets in complex scenarios where multiplexers are interconnected, as well as to determine the maximum size of the buffers in the different servers. Previous results provide tight delay bounds for networks where servers are of the FIFO type. Here, we provide tight bounds for any work-conserving scheduling policy, so that our results can be applied to heterogeneous networks where the servers (routers) can use different work-conserving scheduling policies such as First-In First-Out (FIFO), Earliest Deadline First (EDF), Strict Priority (SP), Guaranteed Rate scheduling (GR), etc.

The genetic information in cells is stored in DNA sequences, represented by a string of four letters, each corresponding to a definite type of nucleotides. Genomic DNA sequences are very abundant in periodic patterns, which play important biological roles. The complexity of genetic sequences can be estimated using the information-theoretic methods. Low complexity regions are of particular interest to genome researchers, because they indicate to sequence repeats and patterns. In this paper, the complexity of genetic sequences is estimated using Shannon entropy, Rényi entropy and relative Kolmogorov complexity. The structural complexity based on periodicities is analyzed using the autocorrelation function and time delayed mutual information. As a case study, we analyze human 22nd chromosome and identify 3 and 49 bp periodicities.

New text independent speaker identification method is presented. Phase spectrum of all-pole linear prediction (LP) model is used to derive the speech features. The features are represented by pairs of numbers that are calculated from group delay extremums of LP model spectrum. The first component of the pair is an argument of maximum of group delay of all pole LP model spectrum and the second is an estimation of spectrum bandwidth at the point of spectrum extremum. A similarity metric that uses group delay features is introduced. The metric is adapted for text independent speaker identification with general assumption that test speech channel may contain multiple speakers. It is demonstrated that automatic speaker recognition system with proposed features and similarity metric outperforms systems based on Gaussian mixture model with Mel frequency cepstral coefficients, formants, antiformants and pitch features.

We propose a distributed key generation protocol for pairing-based cryptosystems which is adaptively secure in the erasure-free and secure channel model, and at the same time completely avoids the use of interactive zero-knowledge proofs. Utilizing it as the threshold key generation protocol, we present a secure (t,n) threshold signature scheme based on the Waters' signature scheme. We prove that our scheme is unforgeable and robust against any adaptive adversary who can choose players for corruption at any time during the run of the protocols and make adaptive chosen-message attacks. And the security proof of ours is in the standard model (without random oracles). In addition our scheme achieves optimal resilience, that is, the adversary can corrupt any t<n/2 players.

Many electronic cash systems have been proposed with the proliferation of the Internet and the activation of electronic commerce. E-cash enables the exchange of digital coins with value assured by the bank's signature and with concealed user identity. In an electronic cash system, a user can withdraw coins from the bank and then spends each coin anonymously and unlinkably. In this paper, we design an efficient anonymous mobile payment system based on bilinear pairings, in which the anonymity of coins is revocable by a trustee in case of dispute. The message transfer from the customer to the merchant occurs only once during the payment protocol. Also, the amount of communication between customer and merchant is about 800 bits. Therefore, our mobile payment system can be used in the wireless networks with the limited bandwidth. The security of the new system is under the computational Diffie–Hellman problem in the random oracle model.

ASPECTJ and composition filters are well-known influential approaches among a wide range of aspect-oriented programming languages that have appeared in the last decade. Although the two approaches are relatively mature and many research works have been devoted to their enhancement and use in practical applications, so far, there has been no attempt that aims at comparing deeply the two approaches. This article is a step towards this comparison; it proposes a mapping between ASPECTJ and Composition filters that put to the test the two approaches by confronting and relating their concepts. Our work shows that the mapping is neither straightforward nor one-to-one despite the fact that the two approaches belong to the same category and provide extension of the same Java language.

Digital signal processing is one of the most powerful technologies, developed by achievements in science and electronics engineering. Achievements of this technology significantly influenced communications, medicine technique, radiolocation and other. Digital signal processors are usually used for effective solution of digital signal processing problems class. Today digital signal processors are widely used practically in all fields, in which information processing in real-time is needed. Creation of diagnostic medicine systems is one of perspective fields using digital signal processors. The aim of this work was to create digital mathematical model of blood circulation analysis system using digital signal processing instead of analogical nodes of device. In first stage – work algorithm of blood circulation analysis system and mathematical model of blood circulation analysis system in Matlab–Simulink environment was created. In second stage – mathematical model was tested experimentally. Mathematically imitated Doppler signal was sent to tissue and was reflected. The signal was processed in digitally, blood flow direction was marked and blood speed was evaluated. Experimentation was done with real signals that were recorded while investigating patients in eye clinics. Gained results confirmed adequacy of created mathematical model to real analogical blood circulation analysis system (Lizi et al., 2003).

The article addresses the issues of combinatorial evolution of standards in transmission of multimedia information including the following: (a) brief descriptions of basic combinatorial models as multicriteria ranking, knapsack-like problems, clustering, combinatorial synthesis, multistage design, (b) a description of standard series (MPEG) for video information processing and a structural (combinatorial) description of system changes for the standards, (c) a set of system change operations (including multi-attribute description of the operations and binary relations over the operations), (d) combinatorial models for the system changes, and (e) a multistage combinatorial scheme (heuristic) for the analysis of the system changes. Expert experience is used. Numerical examples illustrate the suggested problems, models, and procedures.