With the development of Global Navigation Satellite System (GNSS), the amount of related research is growing rapidly in China. A lot of accomplishments have been achieved in all branches of the satellite navigation field, especially motivated by the BeiDou Program. In this paper, the current status, technologies and developments in satellite positioning and navigation in China are introduced. Firstly, an overview and update of the BeiDou Program is presented, known as the three-step development strategy for different services. Then signal design for the BeiDou system is discussed, including the generation of pseudo-random noise (PRN) codes for currently available signal B1, and the investigation of a new signal modulation scheme for interoperability at open frequency B1C. The B1C signal should comply to Multiplexed Binary Offset Carrier (MBOC) constrains, and a modulation called Quadrature Multiplexed BOC (QMBOC) is presented, which is equivalent to time-multiplexed BOC (TMBOC) for GPS and composite BOC (CBOC) for Galileo, while overcomes the drawback of CBOC. Besides, the inter and intra system compatibility is discussed, based on the effective C/N0 proposed by International Telecommunication Union (ITU). After that, receiver technologies in challenging environments are introduced, such as weak signal acquisition and assisted GNSS (A-GNSS). Moreover, a method of ambiguity mitigation for adaptive digital beam forming (ADBF) in large spacing antenna arrays is proposed, by which interference suppression is available. Furthermore, cutting edge technologies are brought in, including seamless navigation for indoor and outdoor, and collaborative navigation. After all, GNSS applications in China for industry and daily life are shown, as well as the market prospection.

Web Service Business Process Execution Language (BPEL) has become the de facto standard for developing instant service-oriented workflow applications in open environment. The correctness and reliability of BPEL processes have gained increasing concerns. However, the unique features (e.g., dead path elimination (DPE) semantics, parallelism, etc.) of BPEL language have raised enormous problems to it, especially in path feasibility analysis of BPEL processes. Path feasibility analysis of BPEL processes is the basis of BPEL testing, for it relates to the test case generation. Since BPEL processes support both parallelism and DPE semantics, existing techniques can't be directly applied to its path feasibility analysis. To address this problem, we present a novel technique to analyze the path feasibility for BPEL processes. First, to tackle unique features mentioned above, we transform a BPEL process into an intermediary model — BPEL control flow graph, which is proposed to abstract the execution flow of BPEL processes. Second, based on this abstraction, we symbolically encode every path of BPEL processes as some Satisfiability formulas. Finally, we solve these formulas with the help of Satisfiability Modulo Theory (SMT) solvers and the feasible paths of BPEL processes are obtained. We illustrate the applicability and feasibility of our technique through a case study.

In a 1-out-of-n oblivious signature scheme, a user provides a set of messages to a signer for signatures but he/she can only obtain a valid signature for a specific message chosen from the message set. There are two security requirements for 1-out-of-n oblivious signature. The first is ambiguity, which requires that the signer is not aware which message among the set is signed. The other one is unforgeability which requires that the user is not able to derive any other valid signature for any messages beyond the one that he/she has chosen. In this paper, we provide a generic construction of 1-out-of-n oblivious signature. Our generic construction consists of two building blocks, a commitment scheme and a standard signature scheme. Our construction is round efficient since it only asks one interaction (i.e., two rounds) between the user and signer. Meanwhile, in our construction, the ambiguity of the 1-out-of-n oblivious signature scheme is based on the hiding property of the underlying commitment, while the unforgeability is based on the binding property of the underlying commitment scheme and the unforgeability of the underlying signature scheme. Moreover, our construction can also enjoy strong unforgeability as long as the underlying building blocks have strong binding property and strong unforgeability respectively. Given the fact that commitment and digital signature are well-studied topics in cryptography and numerous concrete schemes have been proposed in the standard model, our generic construction immediately yields a bunch of instantiations in the standard model based on well-known assumptions, including not only traditional assumptions like Decision Diffie-Hellman (DDH), Decision Composite Residue (DCR), etc., but also some post-quantum assumption like Learning with Errors (LWE). As far as we know, our construction admits the first 1-out-of-n oblivious signature schemes based on the standard model.