Fair exchange is an important tool to achieve “fairness” of electronic commerce. Several previous schemes satisfy universally composable security which provides security preserving property under complex networks like the Internet. In recent years, as the demand for electronic commerce increases, fair exchange for electronic vouchers (e.g., electronic tickets, moneys, etc.) to obtain services or contents is in the spotlight. The definition of fairness for electronic vouchers is different from that for general electronic items (e.g., the sender must not do duplicate use of exchanged electronic vouchers). However, although there are universally composable schemes for electronic items, there is no previous study for electronic vouchers. In this paper, we introduce a universally composable definition of fair voucher exchange, that is, an ideal functionality of fair voucher exchange. Also, we prove the equivalence between our universally composable definition and the conventional definition for electronic vouchers. Thus, our formulation of the ideal functionality is justified. Finally, we propose a new fair voucher exchange scheme from non-blocking atomic commitment as black-box, which satisfies our security definition and is adequate for mobile environments. By instantiating general building blocks with known practical ones, our scheme can be also practical because it is implemented without trusted third party in usual executions.

We propose attribute-based encryption schemes where encryptor-specified policies (called ciphertext policies) are hidden. By using our schemes, an encryptor can encrypt data with a hidden access control policy. A decryptor obtains her secret key associated with her attributes from a trusted authority in advance and if the attributes associated with the decryptor's secret key do not satisfy the access control policy associated with the encrypted data, the decryptor cannot decrypt the data or guess even what access control policy was specified by the encryptor. We prove security of our construction based on the Decisional Bilinear Diffie-Hellman assumption and the Decision Linear assumption. In our security notion, even the legitimate decryptor cannot obtain the information about the access control policy associated with the encrypted data more than the fact that she can decrypt the data.

Password-based authenticated key exchange protocols are more convenient and practical, since users employ human-memorable passwords that are simpler to remember than cryptographic secret keys or public/private keys. Abdalla, Fouque, and Pointcheval proposed the password-based authenticated key exchange protocol in a 3-party model (GPAKE) in which clients trying to establish a secret do not share a password between themselves but only with a trusted server. On the other hand, Canetti presented a general framework, which is called universally composable (UC) framework, for representing cryptographic protocols and analyzing their security. In this framework, the security of protocols is maintained under a general protocol composition operation called universal composition. Canetti also proved a UC composition theorem, which states that the definition of UC-security achieves the goal of concurrent general composition. A server must manage all the passwords of clients when the 3-party password-based authenticated key exchange protocols are realized in large-scale networks. In order to resolve this problem, we propose a hierarchical hybrid authenticated key exchange protocol (H2AKE). In H2AKE, forwarding servers are located between each client and a distribution server, and the distribution server sends the client an authentication key via the forwarding servers. In H2AKE, public/private keys are used between servers, while passwords are also used between clients and forwarding servers. Thus, in H2AKE, the load on the distribution server can be distributed to the forwarding servers concerning password management. In this paper, we define hierarchical hybrid authenticated key exchange functionality. H2AKE is the universal form of the hierarchical (hybrid) authenticated key exchange protocol, which includes a 3-party model, and it has the characteristic that the construction of the protocol can flexibly change according to the situation. We also prove that H2AKE is secure in the UC framework with the security-preserving composition property.

Smart contracts are protocols that can automatically execute a transaction including an electronic contract when a condition is satisfied without a trusted third party. In a representative use-case, a smart contract is executed when multiple parties fairly trade on a blockchain asset. On blockchain systems, a smart contract can be regarded as a system participant, responding to the information received, receiving and storing values, and sending information and values outwards. Also, a smart contract can temporarily keep assets, and always perform operations in accordance with prior rules. Many cryptocurrencies have implemented smart contracts. At POST2018, Atzei et al. give formulations of seven fair exchange protocols using smart contract on Bitcoin: oracle, escrow, intermediated payment, timed commitment, micropayment channels, fair lotteries, and contingent payment. However, they only give an informal discussion on security. In this paper, we verify the fairness of their seven protocols by using the formal verification tool ProVerif. As a result, we show that five protocols (the oracle, intermediated payment, timed commitment, micropayment channels and fair lotteries protocols) satisfy fairness, which were not proved formally. Also, we re-find known attacks to break fairness of two protocols (the escrow and contingent payment protocols). For the escrow protocol, we formalize the two-party scheme and the three-party scheme with an arbitrator, and show that the two-party scheme does not satisfy fairness as Atzei et al. showed. For the contingent payment protocol, we formalize the protocol with the non-interactive zero-knowledge proof (NIZK), and re-find the attack shown by Campanelli et al. at CCS 2017. Also, we show that a countermeasure with subversion NIZK against the attack works properly while it is not formally proved.

ISO/IEC standardizes several chosen ciphertext-secure key encapsulation mechanism (KEM) schemes in ISO/IEC 18033-2. However, all ISO/IEC KEM schemes are not quantum resilient. In this paper, we introduce new isogeny-based KEM schemes (i.e., CSIDH-ECIES-KEM and CSIDH-PSEC-KEM) by modifying Diffie-Hellman-based KEM schemes in ISO/IEC standards. The main advantage of our schemes are compactness. The key size and the ciphertext overhead of our schemes are smaller than these of SIKE, which is submitted to NIST's post-quantum cryptosystems standardization, for current security analyses. Moreover, though SIKE is proved in the classical random oracle model, CSIDH-PSEC-KEM is proved in the quantum random oracle model. Finally, we discuss difficulty to construct isogeny-based KEM from ISO/IEC KEM schemes in the standard model (i.e., ACE-KEM and FACE-KEM).

This paper firstly provides the extended Canetti-Krawzcyk (eCK) security model for predicate-based authenticated key exchange (AKE) that guarantees resistance to leakage of ephemeral secret keys. Moreover, we propose two-pass key-policy (resp. session-policy) attribute-based AKE protocol secure in the proposed predicate-based eCK security model based on key-policy (resp. ciphertext-policy) attribute-based encryption. The proposed protocols have advantages in security against leakage of ephemeral secret keys and the round complexity compared to the previous predicate-based AKE protocols.

In this paper, the substitutability of the indifferentiability framework with non-sequential scheduling is examined by reformulating the framework through applying the Task-PIOA framework, which provides non-sequential activation with oblivious task sequences. First, the indifferentiability framework with non-sequential scheduling is shown to be able to retain the substitutability. Thus, the substitutability can be applied in another situation that processes of the systems may behave non-sequentially. Next, this framework is shown to be closely related to reducibility of systems. Reducibility is useful to discuss about the construction of a system from a weaker system. Finally, two modelings with respectively sequential scheduling and non-sequential scheduling are shown to be mutually independent. We find examples of systems which are indifferentiable under one model but differentiable under the other. Thus, the importance of scheduling in the indifferentiability framework is clarified.

In this paper, we propose a generic construction of one-round attribute-based (implicitly) authenticated key exchange (ABAKE). The construction is based on a chosen-ciphertext (CCA) secure attribute-based KEM and the decisional Diffie-Hellman (DDH) assumption. If an underlying attribute-based KEM scheme allows expressive access controls and is secure in the standard model (StdM), an instantiated ABAKE scheme also achieves them. Our scheme enjoys the best of both worlds: efficiency and security. The number of rounds is one (optimal) while the known secure scheme in the StdM is not one-round protocol. Our scheme is comparable in communication complexity with the most efficient known scheme that is not proved in the StdM. Also, our scheme is proved to satisfy security against advanced attacks like key compromise impersonation.

Forward secrecy (FS) is a central security requirement of authenticated key exchange (AKE). Especially, strong FS (sFS) is desirable because it can guarantee security against a very realistic attack scenario that an adversary is allowed to be active in the target session. However, most of AKE schemes cannot achieve sFS, and currently known schemes with sFS are only proved in the random oracle model. In this paper, we propose a generic construction of AKE protocol with sFS in the standard model against a constrained adversary. The constraint is that session-specific intermediate computation results (i.e., session state) cannot be revealed to the adversary for achieving sFS, that is shown to be inevitable by Boyd and González Nieto. However, our scheme maintains weak FS (wFS) if session state is available to the adversary. Thus, our scheme satisfies one of strongest security definitions, the CK+ model, which includes wFS and session state reveal. The main idea to achieve sFS is to use signcryption KEM while the previous CK+ secure construction uses ordinary KEM. We show a possible instantiation of our construction from Diffie-Hellman problems.

In this paper, we propose an identity-based authenticated key exchange (ID-AKE) protocol that is secure in the identity-based extended Canetti-Krawczyk (id-eCK) model in the random oracle model under the gap Bilinear Diffie-Hellman assumption. The proposed ID-AKE protocol is the most efficient among the existing ID-AKE protocols that is id-eCK secure, and it can be extended to use in asymmetric pairing.

Almost all existing password-based authenticated key exchange (PAKE) schemes achieve concurrent security in the standard model by relying on the common reference string (CRS) model. A drawback of the CRS model is to require a centralized trusted authority in the setup phase; thus, passwords of parties may be revealed if the authority ill-uses trapdoor information of the CRS. There are a few secure PAKE schemes in the plain model, but, these are not achievable in a constant round (i.e., containing a linear number of rounds). In this paper, we discuss how to relax the setup assumption for (constant round) PAKE schemes. We focus on the multi-string (MS) model that allows a number of authorities (including malicious one) to provide some reference strings independently. The MS model is a more relaxed setup assumption than the CRS model because we do not trust any single authority (i.e., just assuming that a majority of authorities honestly generate their reference strings). Though the MS model is slightly restrictive than the plain model, it is very reasonable assumption because it is very easy to implement. We construct a (concurrently secure) three-move PAKE scheme in the MS model (justly without random oracles) based on the Groce-Katz PAKE scheme. The main ingredient of our scheme is the multi-string simulation-extractable non-interactive zero-knowledge proof that provides both the simulation-extractability and the extraction zero-knowledge property even if minority authorities are malicious. This work can be seen as a milestone toward constant round PAKE schemes in the plain model.

Home Energy Management Systems (HEMS) contain devices of multiple manufacturers. Also, a large number of groups of devices must be managed according to several clustering situations. Hence, since it is necessary to establish a common secret group key among group members, the group key management scheme of IEEE 802.21 is used. However, no security verification result by formal methods is known. In this paper, we give the first formal verification result of secrecy and authenticity of the group key management scheme of IEEE 802.21 against insider and outsider attacks using ProVerif, which is an automatic verification tool for cryptographic protocols. As a result, we clarify that a spoofing attack by an insider and a replay attack by an outsider are found for the basic scheme, but these attacks can be prevented by using the scheme with the digital signature option.

In this paper, a method is proposed to construct a visual secret sharing (VSS) scheme for multiple secret images in which each share can be rotated with 180 degrees in decryption. The proposed VSS scheme can encrypt more number of secret images compared with the normal VSS schemes. Furthermore, the proposed technique can be applied to the VSS scheme that allows to turn over some shares in decryption. From the theoretical point of view, it is interesting to note that such VSS schemes cannot be obtained from so-called basis matrices straightforwardly.

Asymmetric bilinear maps using Type-3 pairings are known to be advantageous in several points (e.g., the speed and the size of a group element) to symmetric bilinear maps using Type-1 pairings. Kremer and Mazaré introduce a symbolic model to analyze protocols based on bilinear maps, and show that the symbolic model is computationally sound. However, their model only covers symmetric bilinear maps. In this paper, we propose a new symbolic model to capture asymmetric bilinear maps. Our model allows us to analyze security of various protocols based on asymmetric bilinear maps (e.g., Joux's tripartite key exchange, and Scott's client-server ID-based key exchange). Also, we show computational soundness of our symbolic model under the decisional bilinear Diffie-Hellman assumption.

This work focuses on a vulnerability of hash functions due to sloppy usages or implementations in the real world. If our cryptographic research community succeeded in the development of a perfectly secure random function as the random oracle, it might be broken in some sense by invalid uses. In this paper, we propose a new variant of the random oracle model in order to analyze the security of cryptographic protocols under the situation of an invalid use of hash functions. Our model allows adversaries to obtain contents of the hash list of input and output pairs arbitrarily. Also, we analyze the security of several prevailing protocols (FDH, OAEP, Cramer-Shoup cryptosystem, Kurosawa-Desmedt cryptosystem, NAXOS) in our model. As the result of analyses, we clarify that FDH and Cramer-Shoup cryptosystem are still secure but others are insecure in our model. This result shows the separation between our model and the standard model.

There are two extensions of oblivious polynomial evaluation (OPE), OPEE (oblivious polynomial evaluation in the exponent) and OPEE2. At TCC 2015, Hazay showed two OPEE2 protocols. In this paper, we first show that her first OPEE2 protocol does not run in polynomial time if the computational DH assumption holds. We next present a constant round OPEE protocol under the DDH assumption.

Group signature (GS) schemes guarantee anonymity of the actual signer among group members. Previous GS schemes assume that randomness in signing is never exposed. However, in the real world, full randomness exposure can be caused by implementation problems (e.g., using a bad random number generator). In this paper, we study (im)possibility of achieving anonymity against full randomness exposure. First, we formulate a new security model for GS schemes capturing full randomness exposure. Next, we clarify that it is impossible to achieve full-anonymity against full randomness exposure without any secure component (e.g., a tamper-proof module or a trusted outside storage). Finally, we show a possibility result that selfless-anonymity can be achieved against full randomness exposure. While selfless-anonymity is weaker than full-anonymity, it is strong enough in practice. Our transformation is quite simple; and thus, previous GS schemes used in real-world systems can be easily replaced by a slight modification to strengthen the security.

LINE is currently the most popular messaging service in Japan. Communications using LINE are protected by the original encryption scheme, called LINE Encryption, and specifications of the client-to-server transport encryption protocol and the client-to-client message end-to-end encryption protocol are published by the Technical Whitepaper. Though a spoofing attack (i.e., a malicious client makes another client misunderstand the identity of the peer) and a reply attack (i.e., a message in a session is sent again in another session by a man-in-the-middle adversary, and the receiver accepts these messages) to the end-to-end protocol have been shown, no formal security analysis of these protocols is known. In this paper, we show a formal verification result of secrecy of application data and authenticity for protocols of LINE Encryption (Version 1.0) by using the automated security verification tool ProVerif. Especially, since it is claimed that the transport protocol satisfies forward secrecy (i.e., even if the static private key is leaked, security of application data is guaranteed), we verify forward secrecy for client's data and for server's data of the transport protocol, and we find an attack to break secrecy of client's application data. Moreover, we find the spoofing attack and the reply attack, which are reported in previous papers.

Authenticated Key Exchange (AKE) is a cryptographic protocol to share a common session key among multiple parties. Usually, PKI-based AKE schemes are designed to guarantee secrecy of the session key and mutual authentication. However, in practice, there are many cases where mutual authentication is undesirable such as in anonymous networks like Tor and Riffle, or difficult to achieve due to the certificate management at the user level such as the Internet. Goldberg et al. formulated a model of anonymous one-sided AKE which guarantees the anonymity of the client by allowing only the client to authenticate the server, and proposed a concrete scheme. However, existing anonymous one-sided AKE schemes are only known to be secure in the random oracle model. In this paper, we propose generic constructions of anonymous one-sided AKE in the random oracle model and in the standard model, respectively. Our constructions allow us to construct the first post-quantum anonymous one-sided AKE scheme from isogenies in the standard model.

In this paper, we propose the first identity-based dynamic multi-cast key distribution (ID-DMKD) protocol which is secure against maximum exposure of secret information (e.g., secret keys and session-specific randomness). In DMKD protocols, users share a common session key without revealing any information of the session key to the semi-honest server, and can join/leave to/from the group at any time even after establishing the session key. Most of the known DMKD protocols are insecure if some secret information is exposed. Recently, an exposure resilient DMKD protocol was introduced, however, each user must manage his/her certificate by using the public-key infrastructure. We solve this problem by constructing the DMKD protocol authenticated by user's ID (i.e., without certificate). We introduce a formal security definition for ID-DMKD by extending the previous definition for DMKD. We must carefully consider exposure of the server's static secret key in the ID-DMKD setting because exposure of the server's static secret key causes exposure of all users' static secret keys. We prove that our protocol is secure in our security model in the standard model. Another advantage of our protocol is scalability: communication and computation costs of each user are independent from the number of users. Furthermore, we show how to extend our protocol to achieve non-interactive join by using certificateless encryption. Such an extension is useful in applications that the group members frequently change like group chat services.