In this work it is shown for the first time how to calculate in advance by momentum-based noise simulation for stationary Monte Carlo (MC) device simulations the CPU time, which is necessary to achieve a predefined error level. In addition, analytical expressions for the simulation-time factor of terminal current estimation are given. Without further improvements of the MC algorithm MC simulations of small terminal currents are found to be often prohibitively CPU intensive.

In 1999, Araki et al. proposed a convertible limited verifier signature scheme. In this letter, we propose a universal forgery attack on their scheme. We show that any one can forge a valid signature of a user UA on an arbitrary message.

Batch verification is a useful tool in verifying a large number of cryptographic items all at one time. It is especially effective in verifying predicates based on modular exponentiation. In some cases, however the items can be incorrect although they pass batch verification together. Such leniency can be eliminated by checking the domain of each item in advance. With this in mind, we introduce the strict batch verification and investigate if the strict batch verification can remain more effective than separate verification. In this paper, we estimate the efficiency of such strict batch verification in several types of groups, a prime subgroup of Zp with special/random prime p and prime subgroups defined on elliptic curves over Fp, F2m and Fpm, with are often used in DL-based cryptographic primitives. Our analysis concludes that the efficiency differs greatly depending on the choice of the group and parameters determined by the verifying predicate. Furthermore, we even show that there are some cases where batch verification, regardless of strictness, loses its computational advantage.

This paper describes an automatic interface insertion scheme for in-system verification of algorithm models. To insert the interface, an algorithm model described in C is translated into another source code that includes the communication with hardware components in the target system to be validated with the algorithm model. The communication between the algorithm model and hardware components is achieved using transactors that perform transformation between access operations and bus cycle transactions. I/O terminal is introduced as an interface model to relate the transactions to access operations during the execution of the algorithm model, i.e., accesses to I/O terminals invoke bus cycle transactions in hardware and vice versa. An automatic interface insertion tool is developed using the source-to-source translation to identify the I/O terminals and insert interface function calls in the source code. The proposed automatic interface insertion scheme is validated by emulating several multimedia algorithms written in C on real target systems.

Recently, Lin et al. addressed two weaknesses of a new strong-password authentication scheme, the SAS protocol, and then proposed an improved one called the OSPA (Optimal Strong-Password Authentication) protocol. However, we find that both the OSPA protocol and the SAS protocol are vulnerable to the stolen-verifier attack.

This paper develops a framework to support trace theoretic verification of timed circuits and systems. A theoretical foundation for classifying timed traces as either successes or failures is developed. The concept of the semimirror is introduced to allow conformance checking thus supporting hierarchical verification of timed circuits and systems. Finally, we relate our framework to those previously proposed for timing verification.

This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algorithm for checking consistency of those descriptions, up to a limited number of steps from initial states. As an example of high-level designs, we take a simple hardware/software codesign. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite number of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.

This paper describes an efficient symbolic model checking algorithm for verification of deadlock free property of high level robot control program called Task Control Architecture (TCA). TCA is a model of concurrent robot control processes. The verification tool we used is the Symbolic Model Verifier (SMV). Since the SMV is not so efficient for verification of liveness properties of many concurrent processes such as deadlock free property, we first described the deadlock free property by using safety properties that SMV can verify efficiently. In addition, we modify the symbolic model checking algorithm of the SMV so that it can handle many concurrent processes efficiently. Experimental measurements show that we can obtain more than 1000 times speed-up by these methods.

In this paper, a novel method of clock feedthrough reduction in CMOS autozeroed operational amplifiers with three-phase clock operation is presented. The operational amplifiers in the method are configured by two autozeroed-gain stages. The differential input stage and the second output gain stage are autozeroed individually by a three-phase clock for autozeroing. The three-phase clock is provided so as to finish the compensation period of the input stage earlier than the end of the second stage compensation period. This operation makes it possible to absorb affection of clock feedthrough in the input stage with the second stage. As a result, residual error of offset compensation is much reduced by the voltage gain of the first stage. The effect of the two-stage autozeroing has been confirmed with SPICE simulation and fabricated CMOS circuit. The results of SPICE simulation showed that the two-stage autozeroed operational amplifier has significant advantage as compared to conventional configuration. Affection of clock feedthrough is reduced to about 1/50 in the two-stage configuration. Fabricated CMOS circuit also showed high potential of the two-stage autozeroed operational amplifier for feedthrough reduction. It has been proven experimentally that the two-stage autozeroing is an effective design approach to reduce clock feedthrough error in CMOS autozeroed operational amplifiers.

This paper presents a formal verification method based on logic simulation. In our method, some restricted class of circuits which include data paths can be verified without abstraction of data paths by using symbolic values. Our verifier extracts a transition relation from the state graph (given as a specification) which is expressed using symbolic values, and verifies based on simulation using those symbolic values if the circuit behaves correctly with respect to each transition of the specification. If the verifier terminates with "correct," then it can be guaranteed that for any applicable input vector sequence, the circuit and the specification behaves identically. We have implemented the proposed method on a Unix workstation and verified some FIFO and LIFO circuits by using it.

We present a simple solution to secretly sharing a factoring witness (for given N) in a publicly-verifiable manner. Compared to the previous PVSS schemes to secretly sharing a factoring witness, the scheme enjoys the following properties: (1) the formal proofs of security can be given; (2) it is designed to be conceptually simpler; (3) it needs fewer communicated bits and, if not-so low exponent RSA (e.g., e > 219+1) is used in the previous schemes, fewer computations; (4) no general multi-party computation is required in the preparation phase.

Recently, biometrics such as a person's fingerprint, face, and voice has come to be used for personal authentication. At present, most biometrics authentication systems depend on verification (one-to-one matching) because such verification takes a short period of time and is expected to provide a quick response. In these systems, however, every single user has to enter an ID number for each authentication session and might feel incovenienced as a result. To improve the operation efficiency, identification (one-to-many matching) is required, but identification is currently assumed to require much more time than verification (i.e., the response time is not practical). After probing these problems, we developed a new method to achieve identification in a short period of time. This method shortens the response time by using a matching score matrix, which is constructed in the enrollment phase. The proposed method is shown to need only about 45 one-to-one matchings to identify data in a database with two thousand fingerprints, a count much less than by conventional methods.

Personal identity verification has a great variety of applications including access to computer terminals, buildings, credit card verification as well as EC. Algorithms for personal identity verification can be roughly classified into four categories depending on static/dynamic and biometric/physical or knowledge based. Finger prints, iris, retina, DNA, face, blood vessels, for instance, are static and biometric. Algorithms which are biometric and dynamic include lip movements, body movements and on-line signatures. Schemes which use passwords are static and knowledge based, whereas methods using magnetic cards and IC cards are physical. Each scheme naturally has its own advantages and disadvantages. A new algorithm is proposed for pen-input on-line signature verification incorporating pen-position, pen-pressure and pen-inclinations trajectories. A preliminary experiment is performed on a data base consisting of 293 genuine writings and 540 forgery writings, from 8 individuals. Average correct verification rate was 97.6% whereas average forgery refection rate was 98.7%. Since no fine tuning was done, this preliminary result looks very promising.

This paper is concerned with a comparative study of the accepting powers of deterministic, Las Vegas, self-verifying nondeterminisic, and nondeterministic (simple) multihead finite automata. We show that (1) for each k 2, one-way deterministic k-head (resp., simple k-head) finite automata are less powerful than one-way Las Vegas k-head (resp., simple k-head) finite automata, (2) there is a language accepted by a one-way self-verifying nondeterministic simple 2-head finite automaton, but not accepted by any one-way deterministic simple multihead finite automaton, (3) there is a language accepted by a one-way nondeterministic 2-head (resp., simple 2-head) finite automaton, but not accepted by any one-way self-verifying nondeterministic multihead (resp., simple multihead) finite automaton, (4) for each k 1, two-way Las Vegas k-head (resp., simple k-head) finite automata have the same accepting powers as two-way self-verifying nondeterministic k-head (resp., simple k-head) finite automata, and (5) two-way Las Vegas simple 2-head finite automata are more powerful than two-way deterministic simple 2-head finite automata.

Message Sequence Chart (MSC) standardized by International Telecommunication Union is a graphical and textual language for specification of concurrent systems. It has been used formally as well as informally to specify behavior of real-time systems, in particular telecommunication switching systems. Formal verification of a system specification is crucial to ensure that implementation of the system works correctly. In particular, verification methods based on finite states have been widely used in telecommunication systems design. The methods determine global system states and transitions between them (i. e. , build a global state transition graph (GSTG)), and verify the system's desired properties, such as safety and liveness, on the GSTG. In this paper, we focus on construction of GSTGs from MSC specifications. We propose action dependency graph as an intuitive description of semantics of MSC specifications and present an algorithm to translate MSC specifications to action dependency graphs as well as an algorithm to construct a global state transition graph from an action dependency graph.

This paper newly formalizes some notions of security for probabilistic public-key encryption schemes. The framework for these notions was originally presented in the work by Bellare et al., in which they consider non-malleability and indistinguishability under chosen-plaintext attack, non-adaptive chosen-ciphertext attack and adaptive chosen-ciphertext attack. This paper extends the results of Bellare et al. by introducing two goals, equivalence undecidability and non-verifiability under the above three attack models. Such goals are sometimes required in electronic voting and bids systems. It is shown that equivalence undecidability, non-verifiability and indistinguishability are all equivalent under the three attack models.

Timing verification of digital synchronous designs is a complex process that is traditionally carried out deep in the design cycle, at the gate level. A method, embodied in a C++ based design system, is presented that allows modeling and verification of clock regions at a higher level. By combining event-driven, clock-cycle true and behavioral simulation, we are able to perform static and dynamic timing analysis of the clock regions.

Multi-cycle paths are paths between registers where 2 or more clock cycles are allowed to propagate signals, and the detection of multi-cycle paths is important in deciding proper clock period, timing verification and logic optimization. This paper presents a satisfiability-based multi-cycle path detection method, where the detection problems are reduced to CNF formulae and the satisfiability is checked using SAT provers. We also show heuristics on conversion from multi-level circuits into CNF formulae. We have applied our method to ISCAS'89 benchmarks and other sample circuits. Experimental results show the remarkable improvements on the size of manipulatable circuits.

Generating state spaces is one of important and general methods in the analysis of Petri nets. There are two reasons why state spaces of Petri nets become so large. One is concurrent occurring of transitions, and the other is periodic occurring of firing sequences. This paper focuses on the second problem, and proposes a new algorithm for exploring state spaces of finite capacity Petri nets with large capacities. In the proposed algorithm, the state space is represented in the form of a tree such that a set of markings generated by periodic occurrences of firing sequences is associated with each node, and it is much smaller than the reachability graph.

We propose an extraction method of personal features based on on-line handwriting information. Most recent research has been focused on signature verification, especially in the field of on-line writer verification. However, signature verification has a serious problem in that it will accept forged handwriting. To solve this problem, we have introduced an on-line writer verification method which uses ordinary characters. In this method, any handwritten characters (i.e., ordinary characters) are accepted as a text in the verification process, and the text used in the verification process can be different from that in the enrollment process. However, in the proposed method, personal features are extracted only from the shape of strokes, and it is still uncertain how efficient other on-line information, such as writing pressure or pen inclination, is for extracting personal features. Therefore, we propose an extraction method of personal features based on on-line handwriting information, including writing-pressure and pen-inclination information. In the proposed method, handwriting information is described by a set of three-dimensional curves, and personal features are described by a set of Fourier descriptors for the three-dimensional curves. We also discuss the reliability of the proposed method with some simulation results using handwritten data. From these simulation results, it is clear that the proposed method effectively extracts personal features from ordinary characters.