A text-dependent i-vector extraction scheme and a lexicon-based binary vector (L-vector) representation are proposed to improve the performance of text-dependent speaker verification. I-vector and L-vector are used to represent the utterances for enrollment and test. An improved cosine distance kernel is constructed by combining i-vector and L-vector together and is used to distinguish both speaker identity and lexical (or text) diversity with back-end support vector machine (SVM). Experiments are conducted on RSR 2015 Corpus part 1 and part 2, the results indicate that at most 30% improvement can be obtained compared with traditional i-vector baseline.

Narrow swipe sensor based systems have drawn more and more attention in recent years. However, the size of captured image is significantly smaller than that obtained from the traditional area fingerprint sensor. Under this condition the available minutiae number is also limited. Therefore, only employing minutiae with the standard associated feature can hardly achieve high verification accuracy. To solve this problem, we present a novel Hybrid Minutiae Descriptor (HMD) which consists of two modules. The first one: Minutiae Ridge-Valley Orientation Descriptor captures the orientation information around minutia and also the trace points located at associated ridge and valley. The second one: Gabor Binary Code extracts and codes the image patch around minutiae. The proposed HMD enhances the representation capability of minutiae feature, and can be matched very efficiently. Experiments conducted over public databases and the database captured by the narrow swipe sensor show that this innovative method gives rise to significant improvements in reducing FRR (False Reject Rate) and EER (Equal Error Rate).

Speaker verification is the task of determining whether two utterances represent the same person. After representing the utterances in the i-vector space, the crucial problem is only how to compute the similarity of two i-vectors. Metric learning has provided a viable solution to this problem. Until now, many metric learning algorithms have been proposed, but they are usually limited to learning a linear transformation. In this paper, we propose a nonlinear metric learning method, which learns an explicit mapping from the original space to an optimal subspace using deep Restricted Boltzmann Machine network. The proposed method is evaluated on the NIST SRE 2008 dataset. Since the proposed method has a deep learning architecture, the evaluation results show superior performance than some state-of-the-art methods.

Many researchers studied computationally-secure (verifiable) secret sharing schemes which distribute multiple secrets with a bulletin board. However, the security definition is ambiguous in many of the past articles. In this paper, we first review existing schemes based on formal definitions of indistinguishability of secrets, verifiability of consistency, and cheater-detectability. And then, we propose a new secret sharing scheme which is the first scheme with indistinguishability of secrets, verifiability, and cheater-detectability, and allows to share secrets with arbitrary access structures. Further, our scheme is provably secure under well known computational assumptions.

In this paper, we give a formalization of the behavior of the Content-Centric Networking (CCN) protocol with parameterizing content managements. CCN is a communications architecture that is based on the names of contents, rather than on addresses. In the protocol used in CCN, each node sends packets to the nodes that are connected to it, which communicate with further nodes that are connected to them. This kind of behaviors prevents formalizing the CCN protocol as end-to-end communications. In our previous work, we formalized the CCN protocol using the proof assistant Coq. However, in this model, each node in the network can store any number of contents. The storage for each node is usually limited and the node may drop some of the contents due to its filled storage. The model proposed in this paper permits a node to have its own content management method, and still keeps the temporal properties that are also valid in the previous model. To demonstrate difference between these models, we give a specification that is valid in the previous model but invalid in the proposed model, called orthogonality. Since it is generally invalid in CCN, the proposed model is more precise than the previous one.

This paper presents an innovative fabrication process for a planar circuits at millimeter-wave frequency. Screen printing technology provides low cost and high performance coplanar waveguides (CPW) lines in planar devices operated at millimeter-wave frequency up to 110GHz. Printed transmission lines provide low insertion losses of 0.30dB/mm at 110GHz and small return loss like as impedance standard lines. In the paper, Multiline Thru-Reflect-Line (TRL) calibration was also demonstrated by using the impedance standard substrates (ISS) fabricated by screen printing. Regarding calibration capability validation, verification devices were measured and compare the results to the result obtained by the TRL calibration using commercial ISS. The comparison results obtained by calibration of screen printing ISS are almost the same as results measured based on conventional ISS technology.

This study presents a two-stage spoken term detection (STD) method that uses the same STD engine twice and a support vector machine (SVM)-based classifier to verify detected terms from the STD engine's output. In a front-end process, the STD engine is used to pre-index target spoken documents from a keyword list built from an automatic speech recognition result. The STD result includes a set of keywords and their detection intervals (positions) in the spoken documents. For keywords having competitive intervals, we rank them based on the STD matching cost and select the one having the longest duration among competitive detections. The selected keywords are registered in the pre-index. They are then used to train an SVM-based classifier. In a query term search process, a query term is searched by the same STD engine, and the output candidates are verified by the SVM-based classifier. Our proposed two-stage STD method with pre-indexing was evaluated using the NTCIR-10 SpokenDoc-2 STD task and it drastically outperformed the traditional STD method based on dynamic time warping and a confusion network-based index.

Deterioration of sewer pipes is one of very important problems in Japan. Sewer inspections have been carried out mainly by visual check or wired remote robots with a camera. However, such inspection schemes involve high labor and/or monetary cost. Sewer inspection with boat-type video cameras or unwired robots takes a long time to check the result of the inspection because video data are obtained after the equipment is retrieved from the pipe. To realize low cost, safe and quick inspection of sewer pipes, we have proposed a sewer inspection system using drifting wireless sensor nodes. Water, soil, and the narrow space in the pipe make the long-range and high throughput wireless radio communication difficult. Therefore, we have to identify suitable radio frequency and antenna configuration based on wireless communication characteristics in sewer pipes. If the frequency is higher, the Fresnel zone, the needed space for the line of sight is small, but the path loss in free space is large. On the other hand, if the frequency is lower, the size of the Fresnel zone is large, but the path loss in free space is small. We conducted wireless communication experiments using 920MHz, 2.4GHz, and 5GHz band off-the-shelf devices in an experimental underground pipe. The measurement results show that the wireless communication range of 5GHz (IEEE 802.11a) is over 8m in a 200mm-diameter pipe and is longer than 920MHz (ARIB STD-T108), 2.4GHz (IEEE 802.11g, IEEE 802.15.4) band at their maximum transmission power. In addition, we confirmed that devices that use IEEE 802.11a and 54Mbps bit rate can transmit about 43MB data while they are in the communication range of an AP and drift at 1m/s in a 200mm-diameter pipe, and it is bigger than one of devices that use other bit rate.

SDN (Software-Defined Networking) enables software applications to program individual network devices dynamically and therefore control the behavior of the network as a whole. Incomplete programming and/or inconsistency with the network policy of SDN software applications may lead to verification issues. The objective of this paper is to describe the formal modeling that uses the process algebra called pACSR and then suggest a method to verify the firewall application running on top of the SDN controller. The firewall rules are translated into a pACSR process which acts as the specification, and packet's behaviors in SDN are also translated to a pACSR process which is a role as the implementation. Then we prove the correctness by checking whether the parallel composition of two pACSR processes is deadlock-free. Moreover, in the case of network topology changes, our verification can be directly applied to check whether any mismatches or inconsistencies will occur.

Face verification in the presence of age progression is an important problem that has not been widely addressed. Despite appearance changes for same person due to aging, they are more similar compared to facial images from different individuals. Hence, we design common and adapted vocabularies, where common vocabulary describes contents of general population and adapted vocabulary represents specific characteristics of one of image facial pairs. And the other image is characterized with a concatenation histogram of common and adapted visual words counts, termed as “age-invariant distinctive representation”. The representation describes whether the image content is best modeled by the common vocabulary or the corresponding adapted vocabulary, which is further used to accomplish the face verification. The proposed approach is tested on the FGnet dataset and a collection of real-world facial images from identification card. The experimental results demonstrate the effectiveness of the proposed method for verification of identity at a modest computational cost.

Superconducting single-flux-quantum (SFQ) device is an emerging device which can realize digital circuits with high switching speed and low power consumption. In SFQ digital circuits, voltage pulses are used for carrier of information, and the representation of logic values is different from that of CMOS circuits. Design methods exclusive to SFQ circuits have been developed. In this paper, we present timing analysis and functional verification methods for SFQ circuits based on new timing model which we call delay-based time frame model. Assuming that possible pulse arrival is periodic, the model defines comprehensive time frames and representation of logic values. In static timing analysis, expected pulse arrival time is checked based on the model, and the order among pulse arrival times is calculated for each logic gate. In functional verification, the circuit behavior is abstracted in a form similar to a synchronous sequential circuit using the order of pulse arrival times, and then the behavior is verified using formal verification tools. Using our proposed methods, we can verify the functional behavior of SFQ circuits with complex clocking scheme, which appear often in practical design but cannot be dealt with in existing verification method. Experimental results show that our method can be applied to practical designs.

In this paper, we first propose a notion of multiple authorities attribute-based designated confirmer signature scheme with unified verification. In a multiple authorities attribute-based designated confirmer signature scheme with unified verification, both the signer and the designated confirmer can run the same protocols to confirm a valid signature or disavow an invalid signature. Then, we construct a multiple authorities attribute-based designated confirmer signature scheme with unified verification. Finally, we prove the correctness and security of the proposed scheme.

In OpenFlow, data and control plane are decoupled from switches or routers. While the data plane resides in the switches or routers, the control plane might be moved into one or more external servers (controllers). In this article, we propose verification mechanisms for the data plane functionality of switches. The latter consists of two parts: (1) Flow-Match Header part (to match a flow of incoming packets) and (2) action part (e.g., to forward incoming packets to an outgoing port). We propose a mechanism to verify the Flow-Match Header part of the data plane. The mechanism can be executed at the controller, or on an additional device or server (or virtual machines) attached to the network. Deploying a virtual machine (VM) or server for verification may decrease the load of the controller and/or consumed bandwidth between the controller and a switch. We propose a heuristic to place external verification devices or VMs in a network such that the verification time can be minimized. Verification time with respect to consumed resources are evaluated through emulation experiments. Results confirm that the verification time using the proposed heuristic is indeed shortened significantly, while requiring low bandwidth resources.

Code-based public-key encryption schemes (PKE) are the candidates for post-quantum cryptography, since they are believed to resist the attacks using quantum algorithms. The most famous such schemes are the McEliece encryption and the Niederreiter encryption. In this paper, we present the zero-knowledge (ZK) proof systems for proving statements about data encrypted using these schemes. Specifically, we present a proof of plaintext knowledge for both PKE's, and also a verifiable McEliece PKE. The main ingredients of our constructions are the ZK identification schemes by Stern from Crypto'93 and by Jain, Krenn, Pietrzak, and Tentes from Asiacrypt'12.

OSEK/VDX, a standard for an automobile OS, has been widely adopted by many manufacturers to design and develop a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more complex applications are be developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. To ensure the reliability of developed applications, model checking as an exhaustive technique can be applied to discover subtle errors in the development process. Many model checkers have been successfully applied to verify sequential software and general multi-threaded software. However, it is hard to directly use existing model checkers to precisely verify OSEK/VDX applications, since the execution characteristics of OSEK/VDX applications are different from the sequential software and general multi-threaded software. In this paper, we describe and develop an approach to translate OSEK/VDX applications into sequential programs in order to employ existing model checkers to precisely verify OSEK/VDX applications. The value of our approach is that it can be considered as a front-end translator for enabling existing model checkers to verify OSEK/VDX applications.

Verification of a design with respect to its requirement specification is important to prevent errors before constructing an actual implementation. The existing works focus on verifications where the specifications are described using temporal logics or using the same languages as that used to describe the designs. Our work considers cases where the specifications and the designs are described using different languages. To verify such cases, we propose a framework to check if a design conforms to its specification based on their simulation relation. Specifically, we define the semantics of the specifications and the designs commonly as labelled transition systems (LTSs). We appreciate LTSs since they could interpret information about the system and actions that the system may perform as well as the effect of these actions. Then, we check whether a design conforms to its specification based on the simulation relation of their LTS. In this paper, we present our framework for the verification of reactive systems, and we present the case where the specifications and the designs are described in Event-B and Promela/Spin, respectively. We also present two case studies with the results of several experiments to illustrate the applicability of our framework on practical systems.

Appearance changes conform to certain rules for a same person,while for different individuals the changes are uncontrolled. Hence, this paper studies the age progression rules to tackle face verification task. The age progression rules are discovered in the difference space of facial image pairs. For this, we first represent an image pair as a matrix whose elements are the difference of a set of visual words. Thereafter, the age progression rules are trained using Support Vector Machine (SVM) based on this matrix representation. Finally, we use these rules to accomplish the face verification tasks. The proposed approach is tested on the FGnet dataset and a collection of real-world images from identification card. The experimental results demonstrate the effectiveness of the proposed method for verification of identity.

In this study, Si(100) surface flattening process was investigated utilizing sacrificial oxidation method to improve Metal--Insulator--Semiconductor (MIS) diode characteristics. By etching of the 100,nm-thick sacrificial oxide formed by thermal oxidation at 1100$^{circ}$C, the surface roughness of Si substrate was reduced. The obtained Root-Mean-Square (RMS) roughness was decreased from 0.15,nm (as-cleaned) to 0.07,nm in the case of sacrificial oxide formed by wet oxidation, while it was 0.10,nm in the case of dry oxidation. Furthermore, time-dependent dielectric breakdown (TDDB) characteristic of Al/SiO$_{2}$(10,nm)/p-Si(100) MIS diode structures was found to be improved by the reduction of Si surface RMS roughness.

Resource Description Framework (RDF) access control suffers from an authorization conflict problem caused by RDF inference. When an access authorization is specified, it can lie in conflict with other access authorizations that have the opposite security sign as a result of RDF inference. In our former study, we analyzed the authorization conflict problem caused by subsumption inference, which is the key inference in RDF. The Rule Interchange Format (RIF) is a Web standard rule language recommended by W3C, and can be combined with RDF data. Therefore, as in RDF inference, an authorization conflict can be caused by RIF inference. In addition, this authorization conflict can arise as a result of the interaction of RIF inference and RDF inference rather than of RIF inference alone. In this paper, we analyze the authorization conflict problem caused by RIF inference and suggest an efficient authorization conflict detection algorithm. The algorithm exploits the graph labeling-based algorithm proposed in our earlier paper. Through experiments, we show that the performance of the graph labeling-based algorithm is outstanding for large RDF data.

We aim at constructing adaptive oblivious transfer protocols, enjoying fully simulatable security, from various well-known assumptions such as DDH, d-Linear, QR, and DCR. To this end, we present two generic constructions of adaptive OT, one of which utilizes verifiable shuffles together with threshold decryption schemes, while the other uses permutation networks together with what we call loosely-homomorphic key encapsulation schemes. The constructions follow a novel designing approach called “blind permutation”, which completely differs from existing ones. We then show that specific choices of the building blocks lead to concrete adaptive OT protocols with fully simulatable security in the standard model under the targeted assumptions. Our generic methods can be extended to build universally composable (UC) secure OT protocols, with a loss in efficiency.