We present a mathematical formulation of a trust metric using a quality and quantity pair. Under a certain assumption, we regard trust as an additive value and define the soundness of a trust computation as not to exceed the total sum. Moreover, we point out the importance of not only soundness of each computed trust but also the stability of the trust computation procedure against changes in trust value assignment. In this setting, we define trust composition operators. We also propose a trust computation protocol and prove its soundness and stability using the operators.

In this paper, we construct the first efficient leakage-resilient CCA2 (LR-CCA2)-secure attribute-based encryption (ABE) schemes. We also construct the first efficient LR-CCA2-secure identity-based encryption (IBE) scheme with optimal leakage rate. To obtain our results, we develop a new quasi-adaptive non-interactive zero-knowledge (QA-NIZK) argument for the ciphertext consistency of the LR-CPA-secure schemes. Our ABE schemes are obtained by boosting the LR-CPA-security of some existing schemes to the LR-CCA2-security by using our QA-NIZK arguments. The schemes are almost as efficient as the underlying LR-CPA-secure schemes.

Workflow nets (WF-nets for short) are a subclass of Petri nets and are used for modeling and analysis of workflows. Soundness is a criterion of logical correctness defined for WF-nets. A WF-net is said to be sound if it satisfies three conditions: (i) option to complete, (ii) proper completion, and (iii) no dead tasks. In this paper, focusing our analysis on acyclic free choice WF-nets, we revealed that (1) Conditions (i) and (ii) of soundness are respectively equivalent to the liveness and the boundedness of its short-circuited net; (2) The decision problem for each condition of soundness is co-NP-complete; and (3) If the short-circuited net has no disjoint paths from a transition to a place (or no disjoint paths from a place to a transition), each condition can be checked in polynomial time.

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.

Workflow nets (WF-nets for short) are a standard way to automate business processes. Well-Structured WF-nets (WS WF-nets for short) are an important subclass of WF-nets because they have a well-balanced capability to expression power and analysis power. In this paper, we revealed structural and behavioral properties of WS WF-nets. Our results on structural properties are: (i) There is no EFC but non-FC WF-net in WS WF-nets; (ii) A WS WF-net is sound iff it is a van Hee et al.'s ST-net. Our results on behavioral properties are: (i) Any WS WF-net is safe; (ii) Any WS WF-net is separable; (iii) A necessary and sufficient condition on reachability of sound WS WF-net (N,[pIk]). Finally we illustrated the usefulness of the proposed properties with an application example of analyzing workflow evolution.

A workflow may be extended to adapt to market growth, legal reform, and so on. The extended workflow must be logically correct, and inherit the behavior of the existing workflow. Even if the extended workflow inherits the behavior, it may be not logically correct. Can we modify it so that it satisfies not only behavioral inheritance but also logical correctness? This is named behavioral inheritance preserving soundizability problem. There are two kinds of behavioral inheritance: protocol inheritance and projection inheritance. In this paper, we tackled protocol inheritance preserving soundizability problem using a subclass of Petri nets called workflow nets. Limiting our analysis to acyclic free choice workflow nets, we formalized the problem. And we gave a necessary and sufficient condition on the problem, which is the existence of a key structure of free choice workflow nets called TP-handle. Based on this condition, we also constructed a polynomial time procedure to solve the problem.

In resetting attacks against a proof system, a prover or a verifier is reset and enforced to use the same random tape on various inputs as many times as an adversary may want. Recent deployment of cloud computing gives these attacks a new importance. This paper shows that argument systems for any NP language that are both resettably-sound and resettable zero-knowledge are possible by a constant-round protocol in the BPK model. For that sake, we define and construct a resettably-extractable conditional commitment scheme.

A workflow net (WF-net for short) is a Petri net which represents a workflow. There are two important subclasses of WF-nets: extended free-choice (EFC for short) and well-structured (WS for short). It is known that most actual workflows can be modeled as EFC WF-nets; Acyclic WS is a subclass of acyclic EFC but has more analysis methods. An acyclic EFC WF-net may be transformed to an acyclic WS WF-net without changing the external behavior of the net. We name such a transformation Acyclic EFC WF-net refactoring. We give a formal definition of acyclic EFC WF-net refactoring problem. We also give a necessary condition and a sufficient condition for solving the problem. Those conditions can be checked in polynomial time. These result in the enhancement of the analysis power of acyclic EFC WF-nets.

The Workflow Management Coalition, WfMC for short, has given a protocol for interorganizational workflows, interworkflows for short. In the protocol, an interworkflow is constructed by connecting two or more existing workflows; and there are three models to connect those workflows: chained, nested, and parallelsynchronized. Business continuity requires the interworkflow to preserve the behavior of the existing workflows. This requirement is called behavioral inheritance, which has three variations: protocol inheritance, projection inheritance, and life-cycle inheritance. Van der Aalst et al. have proposed workflow nets, WF-nets for short, and have shown that the behavioral inheritance problem is decidable but intractable. In this paper, we first show that all WF-nets of the chained model satisfy life-cycle inheritance, and all WF-nets of the nested model satisfy projection inheritance. Next we show that soundness is a necessary condition of projection inheritance for an acyclic extended free choice WF-net of the parallelsynchronized model. Then we prove that the necessary condition can be verified in polynomial time. Finally we show that the necessary condition is a sufficient condition if the WF-net is obtained by connecting state machine WF-nets.

This paper deals with WF-net based modeling and verification of interorganizational workflows (interworkflows for short) based on the protocol of WfMC. In the protocol, there are three patterns of interoperability: Chained, Nested, and Parallel synchronized; and an interworkflow is constructed by using those interoperability patterns. We first give a WF-net based modeling method. In this modeling method, the three interoperability patterns are respectively expressed in terms of WF-nets. They enable us to model a given interworkflow as a WF-net by connecting WF-nets representing its constituent workflows. We also indicate that if free choice WF-nets are connected by means of any combination of the three patterns then the resultant WF-net is asymmetric choice. Next we discuss verification of WF-nets obtained through the modeling method. Intuitively, a WF-net is said to be sound if, for any case, the initial state is always transformed to the final state. Unfortunately, even if every constituent WF-net is sound FC, the resultant WF-net is not always sound. We give a sufficient condition of non-soundness checkable in polynomial time. We also show that if they are connected by only the Nested pattern then the resultant WF-net is sound.