In this letter, we improve NF'07 (Nakanishi and Funabiki) VLR group signature scheme such that it satisfies exculpability and has lower computation costs. In the proposed scheme, a group member generates his own private key together with the group manager in order to realize exculpability while the signature size is not made longer. Also, a new revocation check method is proposed at the step of verifying, and the computation costs of verifying are independent of the number of the revoked members, while they are linear with the number of the revoked members in the original scheme. Thus, the proposed scheme is more efficient than the original scheme and can be applicable to mobile environments such as IEEE 802.1x.

AlN/GaN Metal Insulator Semiconductor Field Effect Transistors (MISFETs) were designed, simulated and fabricated. DC, S-parameter and power measurements were also performed. Drift-diffusion simulations using DESSIS compared AlN/GaN MISFETs and Al32Ga68N/GaN Heterostructure FETs (HFETs) with the same geometries. The simulation results show the advantages of AlN/GaN MISFETs in terms of higher saturation current, lower gate leakage and higher transconductance than AlGaN/GaN HFETs. First results from fabricated AlN/GaN devices with 1 µm gate length and 200 µm gate width showed a maximum drain current density of 380 mA/mm and a peak extrinsic transconductance of 85 mS/mm. S-parameter measurements showed that current-gain cutoff frequency (fT) and maximum oscillation frequency (fmax) were 5.85 GHz and 10.57 GHz, respectively. Power characteristics were measured at 2 GHz and showed output power density of 850 mW/mm with 23.8% PAE at VDS = 15 V. To the authors knowledge this is the first report of a systematic study of AlN/GaN MISFETs addressing their physical modeling and experimental high-frequency characteristics including the power performance.

There are two ways to describe a state machine as an algebraic specification: a behavioral specification and a rewrite specification. In this study, we propose a translation system from behavioral specifications to rewrite specifications to obtain a verification system which has the strong points of verification techniques for both specifications. Since our translation system is complete with respect to invariant properties, it helps us to obtain a counter-example for an invariant property through automatic exhaustive searching for a rewrite specification.

The use of a formal method is a promising approach to developing reliable computer programs. This paper presents a formal method for anonymity, which is an important security property of communication protocols with regard to a user's identity. When verifying the anonymity of security protocols, we need to consider the presence of adversaries. To formalize stronger adversaries, we introduce an adversary model for simulation-based anonymity proof. This paper also demonstrates the formal verification of a communication protocol. We employ Crowds, which is an implementation of an anonymous router, and verify its anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem prover.

We have previously proposed a noise-robust speaker verification method using fundamental frequency (F0) extracted using the Hough transform. The method also incorporates an automatic stream-weight and decision threshold estimation technique. It has been confirmed that the proposed method is effective for white noise at various SNR conditions. This paper evaluates the proposed method in more practical in-car and elevator-hall noise conditions. The paper first describes the noise-robust F0 extraction method and details of our robust speaker verification method using multi-stream HMMs for integrating the extracted F0 and cepstral features. Details of the automatic stream-weight and threshold estimation method for multi-stream speaker verification framework are also explained. This method simultaneously optimizes stream-weights and a decision threshold by combining the linear discriminant analysis (LDA) and the Adaboost technique. Experiments were conducted using Japanese connected digit speech contaminated by white, in-car, or elevator-hall noise at various SNRs. Experimental results show that the F0 features improve the verification performance in various noisy environments, and that our stream-weight and threshold optimization method effectively estimates control parameters so that FARs and FRRs are adjusted to achieve equal error rates (EERs) under various noisy conditions.

We present a new framework for checking safety failures. The approach is based on the conservative inference of the internal states of a system by the observation of the interaction with its environment. It is based on two similar mechanisms : forward implication, which performs the analysis of the consequences of an input applied to the system, and backward implication, that performs the same task for an output transition. While being a very simple approach, it is general and we believe it can yield efficient algorithms in different safety-failure checking problems. As a case study, we have applied this framework to an existing problem, the hazard checking in (speed-independent) asynchronous circuits. Our new methodology yields an efficient algorithm that performs better or as well as all existing algorithms, while being more general than the fastest one.

In forensic voice telephony speaker verification, we may be requested to identify a speaker in a very noisy environment, unlike the conditions in general research. In a noisy environment, we process speech first by clarifying it. However, the previous study of speaker verification from clarified speech did not yield satisfactory results. In this study, we experimented on speaker verification with clarification of speech in a noisy environment, and we examined the relationship between improving acoustic quality and speaker verification results. Moreover, experiments with realistic noise such as a crime prevention alarm and power supply noise was conducted, and speaker verification accuracy in a realistic environment was examined. We confirmed the validity of speaker verification with clarification of speech in a realistic noisy environment.

Synthesis of quantum circuits is essential for building quantum computers. It is important to verify that the circuits designed perform the correct functions. In this paper, we propose an algorithm which can be used to verify the quantum circuits synthesized by any method. The proposed algorithm is based on BDD (Binary Decision Diagram) and is called X-decomposition Quantum Decision Diagram (XQDD). In this method, quantum operations are modeled using a graphic method and the verification process is based on comparing these graphic diagrams. We also develop an algorithm to verify reversible circuits even if they have a different number of garbage qubits. In most cases, the number of nodes used in XQDD is less than that in other representations. In general, the proposed method is more efficient in terms of space and time and can be used to verify many quantum circuits in polynomial time.

A fair exchange scheme is a protocol by which two parties Alice and Bob swap items or services without allowing either party to gain an advantage by quitting prematurely or otherwise misbehaving. Verifiably committed signature is a generalized and unified model for non-interactive optimistic fair exchange scheme. The state-of-the-art verifiably committed signature that enjoys the off-line, setup-free and stand-alone properties is due to Zhu and Bao [1]. In this article, we show that the Zhu-Bao's verifiably committed signature is insecure in the multi-user setting and then consider possible countermeasures.

Correctness of Java programs is important because they are executed in distributed computing environments. The object initialization scheme in the Java programming language is complicated, and this complexity may lead to undesirable semantic bugs. Various tools have been developed for detecting program patterns that might cause errors during program execution. However, current tools cannot identify code patterns in which an uninitialized field is accessed when an object is initialized. We refer to such erroneous patterns as uninitialized field references. In this paper, we propose a static pattern detection algorithm for identifying uninitialized field references. We design a sound analysis for this problem and implement an analyzer using the Soot framework. In addition, we apply our algorithm to some real Java applications. From the experiments, we identify 12 suspicious field references in the applications, and among those we find two suspected errors by manual inspection.

DTW-based text-dependent speaker verification technology is an effective scheme for protecting personal information in personal electronic products from others. To enhance the performance of a DTW-based system, an impostor database covering all possible passwords is generally required for the matching scores normalization. However, it becomes impossible in our practical application scenario since users are not restricted in their choice of password. We propose a method to generate pseudo-impostor data by employing an acoustic codebook. Based on the pseudo-impostor data, two normalization algorithms are developed. Besides, a template compression approach based on the codebook is introduced. Some modifications to the conventional DTW global constraints are also made for the compressed template. Combining the normalization and template compression methods, we obtain more than 66% and 35% relative reduction in storage and EER, respectively. We expect that other DTW-based tasks may also benefit from our methods.

We present MobileOBJ, a formal framework for specifying and verifying mobile systems. Based on hidden algebra, the components of a mobile system are specified as behavioral objects or Observational Transition Systems, a kind of transition system, enriched with special action and observation operators related to the distinct characteristics of mobile computing systems. The whole system comes up as the concurrent composition of these components. The implementation of the abstract model is achieved using CafeOBJ, an executable, industrial strength algebraic specification language. The visualization of the specification can be done using CafeOBJ graphical notation. In addition, invariant and behavioral properties of mobile systems can be proved through theorem proving techniques, such as structural induction and coinduction that are fully supported by the CafeOBJ system. The application of the proposed framework is presented through the modeling of a mobile computing environment and the services that need to be supported by the former.

The selection of the most representative utterances coming from a speaker is essential for the right performance of automatic enrollment in speaker verification. Model quality measures and threshold estimation methods mainly deal with the scarcity of data and the difficulty of obtaining data from impostors in real applications. Conventional methods estimate the quality of the training utterances once the model is created. In such case, it is not possible to ask the user for more utterances during the training session if necessary. A new training session must be started. That was especially unusable in applications where only one or two enrolment sessions were allowed. In this paper, a new on-line quality method based on a male and a female Universal Background Model (UBM) is introduced. The two models act as a reference for new utterances and show if they belong to the same speaker and provide a measure of its quality at the same time. On the other hand, the estimation of the verification threshold is also strongly influenced by the previous selection of the speaker's utterances. In this context, potential outliers, i.e., those client scores which are distant with regard to mean, could lead to wrong mean and variance client estimations. To alleviate this problem, some efficient threshold estimation methods based on removing or weighting scores are proposed here. Before estimating the threshold, the client scores catalogued as outliers are removed, pruned or weighted, improving subsequent estimations. Text-dependent experiments have been carried out by using a telephonic multi-session database in Spanish. The database has been recorded by the authors and has 184 speakers.

In this paper, we describe a novel focusing mechanism that uses a varifocal mirror and its application to measuring the shape of solder bumps arrayed on an LSI package board based on the shape-from-focus technique. We used a copper-alloy mirror deformed by a piezoelectric actuator as a varifocal mirror to build a simple yet fast focusing mechanism. The varifocal mirror was situated at the focal point of the image-taking lens in image space so that the lateral magnification was constant during focusing and an orthographic projection was perfectly established. The focused plane could be shifted along the optical axis with a precision of 1.4 µm in a depth range of 1.3 mm by driving the varifocal mirror. A magnification of 1.97 was maintained during focusing. Evaluating the curvature of field and removing its effect from the depth data reduced errors. The shapes of 208 solder bumps, 260 µm high and arrayed at a pitch of 500 µm on the board, were measured. The entire 10 mm10 mm board was segmented into 34 partly overlapping sections. We captured 101 images in each section with a high-resolution camera at different focal points at 15 µm intervals. The shape of almost the entire upper hemisphere of a solder bump could be measured. The error in measuring the bump heights was less than 12 µm.

We propose here the first efficient publicly verifiable hybrid mix-net. Previous publicly verifiable mix-net was only efficient for short ciphertexts and was not suitable for mixing long messages. Previous hybrid mix-net can mix long messages but did not have public verifiability. The proposed scheme is efficient enough to treat large scale electronic questionnaires of long messages as well as voting with write-ins, and offers public verifiability of the correctness of the tally. The scheme is provably secure if we assume random oracles, semantic security of a one-time symmetric-key cryptosystem, and intractability of decision Diffie-Hellman problem. This paper is the full version of the extended abstract appeared in FC 2006 [10].

Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a synchronization verification method for system-level designs described in the SpecC language. Instead of modeling the design with timed FSMs and using a model checker for timed automata (such as UPPAAL or KRONOS), we formulate the timing constraints with equalities/inequalities that can be solved by integer linear programming (ILP) tools. Verification is conducted in two steps. First, similar to other software model checkers, we compute the reachability of an error state in the absence of timing constraints. Then, if a path to an error state exists, its feasibility is checked by using the ILP solver to evaluate the timing constraints along the path. This approach can drastically increase the sizes of the designs that can be verified. Abstraction and abstraction refinement techniques based on the Counterexample-Guided Abstraction Refinement (CEGAR) paradigm are applied.

We present a TSK (Takagi-Sugeno-Kang)-based Linguistic Fuzzy Model (TSK-LFM) with uncertain model output. Based on the Linguistic Model (LM) proposed by Pedrycz, we develop a comprehensive design framework. The main design process is composed of the automatic generation of the contexts, fuzzy rule extraction by Context-based Fuzzy C-Means (CFCM) clustering, connection of bias term, and combination of TSK and linguistic context. Finally, we contrast the performance of the presented models with other models for coagulant dosing process in a water purification plant.

In the European Telecommunication Standards Institute (ETSI), Distributed Speech Recognition (DSR) front-end, the distortion added due to feature compression on the front end side increases the variance flooring effect, which in turn increases the identification error rate. The penalty incurred in reducing the bit rate is the degradation in speaker recognition performance. In this paper, we present a nontraditional solution for the previously mentioned problem. To reduce the bit rate, a speech signal is segmented at the client, and the most effective phonemes (determined according to their type and frequency) for speaker recognition are selected and sent to the server. Speaker recognition occurs at the server. Applying this approach to YOHO corpus, we achieved an identification error rate (ER) of 0.05% using an average segment of 20.4% for a testing utterance in a speaker identification task. We also achieved an equal error rate (EER) of 0.42% using an average segment of 15.1% for a testing utterance in a speaker verification task.

This paper presents a synthesizable testbench architecture based on a defined instruction for standalone mode verification. A set of instructions describes transitions of a signal. The set of instructions can be changed easily to describe different signal transitions by loading the different set of instructions on emulator's memory. The proposed testbench enables a fast emulation and increases flexibility and reusability by using an instruction set. To prove the performance of instruction based synthesizable testbench, we verified Bluetooth and IEEE 802.11a PHY baseband systems and compared their performance with those of co-sim mode and modified co-sim mode emulation.

In order to reduce the computational complexity of the DWT domain on-line signature verification, the authors propose to utilize the pen-movement vector as an input parameter. Experimental results indicate that the verification rate obtained using the pen-movement vector parameter is equivalent to that obtained by the conventional method, although the computational complexity of the proposed method is approximately half that of the conventional method.