Trust negotiation is an authorizing technique based on digital credentials, in which both a user and a server gradually establish trust in each other by repeatedly exchanging their credentials. A trust negotiation strategy is a function that answers a set of credentials to disclose to the other party, depending on policies and the set of already disclosed credentials. The disclosure tree strategy (DTS), proposed by Yu et al., is one of the strategies that satisfies preferable properties. DTS in a simple implementation requires exponential time and space; however, neither an efficient algorithm nor the lower-bound of its complexity was known. In this paper, we investigate the computational complexity of DTS. We formulate subproblems of DTS as problems on derivation trees of a context-free grammar (CFG), and analyze the computational complexity of the subproblems using the concepts of CFGs. As a result, we show that two subproblems EVL and MSET of DTS are NP-complete and NP-hard, respectively, while both are solvable in polynomial time if we modify EVL not to require non-redundancy and MSET not to answer any subset useless for leading the negotiation to success.

It is well-known that pushdown systems (PDS) effectively preserve regularity. This property implies the decidability of the reachability problem for PDS and has been applied to automatic program verification. The backward regularity preservation property was also shown for an extension of PDS by adding registers. This paper aims to show the forward regularity preservation property. First, we provide a concise definition of the register model called register pushdown systems (RPDS). Second, we show the forward regularity preservation property of RPDS by providing a saturation algorithm that constructs a register automaton (RA) recognizing $post^{ast}_calP(L(calA))$ where $calA$ and $calP$ are a given RA and an RPDS, respectively, and $post^{ast}_calP$ is the forward image of the mapping induced by $calP$. We also give an example of applying the proposed algorithm to malware detection.

Register context-free grammars (RCFG) is an extension of context-free grammars to handle data values in a restricted way. In RCFG, a certain number of data values in registers are associated with each nonterminal symbol and a production rule has the guard condition, which checks the equality between the content of a register and an input data value. This paper starts with RCFG and introduces register type, which is a finite representation of a relation among the contents of registers. By using register type, the paper provides a translation of RCFG to a normal form and ϵ-removal from a given RCFG. We then define a generalized RCFG (GRCFG) where an arbitrary binary relation can be specified in the guard condition. Since the membership and emptiness problems are shown to be undecidable in general, we extend register type for GRCFG and introduce two properties of GRCFG, simulation and progress, which guarantee the decidability of these problems. As a corollary, these problems are shown to be EXPTIME-complete for GRCFG with a total order over a dense set.

A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.

Register automaton (RA), register context-free grammar (RCFG) and register tree automaton (RTA) are computational models with registers which deal with data values. This paper shows pumping lemmas for the classes of languages expressed by RA, RCFG and RTA. Among them, the first lemma was already proved in terms of nominal automata, which is an abstraction of RA. We define RTA in a deterministic and bottom-up manner. For these languages, the notion of ‘pumped word’ must be relaxed in such a way that a pumped subword is not always the same as the original subword, but is any word equivalent to the original subword in terms of data type defined in this paper. By using the lemmas, we give examples of languages that do not belong to the above-mentioned classes of languages.

Register automaton (RA) is an extension of finite automaton by adding registers storing data values. RA has good properties such as the decidability of the membership and emptiness problems. Linear temporal logic with the freeze quantifier (LTL↓) proposed by Demri and Lazić is a counterpart of RA. However, the expressive power of LTL↓ is too high to be applied to automatic verification. In this paper, we propose a subclass of modal µ-calculus with the freeze quantifier, which has the same expressive power as RA. Since a conjunction ψ1 ∧ ψ2 in a general LTL↓ formula cannot be simulated by RA, the proposed subclass prohibits at least one of ψ1 and ψ2 from containing the freeze quantifier or a temporal operator other than X (next). Since the obtained subclass of LTL↓ does not have the ability to represent a cycle in RA, we adopt µ-calculus over the subclass of LTL↓, which allows recursive definition of temporal formulas. We provide equivalent translations from the proposed subclass of µ-calculus to RA and vice versa and prove their correctness.

Synthesis problems on multiplayer non-zero-sum games (MG) with multiple environment players that behave rationally are the problems to find a good strategy of the system and have been extensively studied. This paper concerns the synthesis problems on stochastic MG (SMG), where a special controller other than players, called nature, which chooses a move in its turn randomly, may exist. Two types of synthesis problems on SMG exist: cooperative rational synthesis problem (CRSP) and non-cooperative rational synthesis problem (NCRSP). The rationality of environment players is modeled by Nash equilibria, and CRSP is the problem to decide whether there exists a Nash equilibrium that gives the system a payoff not less than a given threshold. Ummels et al. studied the complexity of CRSP for various classes of objectives and strategies of players. CRSP fits the situation where the system can make a suggestion of a strategy profile (a tuple of strategies of all players) to the environment players. However, in real applications, the system may rarely have an opportunity to make suggestions to the environment, and thus CRSP is optimistic. NCRSP is the problem to decide whether there exists a strategy σ0 of the system satisfying that for every strategy profile of the environment players that forms a 0-fixed Nash equilibrium (a Nash equilibrium where the system's strategy is fixed to σ0), the system obtains a payoff not less than a given threshold. In this paper, we investigate the complexity of NCRSP for positional (i.e. pure memoryless) strategies. We consider ω-regular objectives as the model of players' objectives, and show the complexity results of the problem for several subclasses of ω-regular objectives. In particular, the problem for terminal reachability (TR) objectives is shown to be Σp2-complete.

This paper compares the expressive power of five language-based access control models. We show that the expressive powers are incomparable between any pair of history-based access control, regular stack inspection and shallow history automata. Based on these results, we introduce an extension of HBAC, of which expressive power exceeds that of regular stack inspection.

Information-Based Access Control (IBAC) has been proposed as an improvement to History-Based Access Control (HBAC) model. In modern component-based systems, these access control models verify that all the code responsible for a security-sensitive operation is sufficiently authorized to execute that operation. The HBAC model, although safe, may incorrectly prevent the execution of operations that should be executed. The IBAC has been shown to be more precise than HBAC maintaining its safety level while allowing sufficiently authorized operations to be executed. However the verification problem of IBAC program has not been discussed. This paper presents a formal model for IBAC programs based on extended weighted pushdown systems (EWPDS). The mapping process between the IBAC original semantics and the EWPDS structure is described. Moreover, the verification problem for IBAC programs is discussed and several typical IBAC program examples using our model are implemented.

This paper proposes an event-based transition system called A-LTS. An A-LTS is a simple system consisting of two agents, a basic program and a monitor. The monitor observes the behavior of the basic program and if the behavior matches some pre-defined pattern, then the monitor interrupts the execution of the basic program and possibly triggers the execution of another specific program. An A-LTS models a common feature found in recent software technologies such as Aspect-Oriented Programming (AOP), history-based access control and active database. We investigate the expressive power of A-LTS and show that it is strictly stronger than finite state machines and strictly weaker than pushdown automata (PDA). This implies that the model checking problem for A-LTS is decidable. It is also shown that the expressive power of A-LTS, linear context-free grammar and deterministic PDA are mutually incomparable. We also discuss the relationship between A-LTS and pointcut/advice in AOP.

Register pushdown system (RPDS) is an extension of pushdown system (PDS) that has registers for dealing with data values. An LTL model checking method for RPDS with regular valuations has been proposed in previous work; however, the method requires the register automata (RA) used for defining a regular valuation to be backward-deterministic. This paper proposes another approach to the same problem, in which the model checking problem for RPDS is reduced to that problem for PDS by constructing a PDS bisimulation equivalent to a given RPDS. This construction is simpler than the previous model checking method and does not require RAs deterministic or backward-deterministic, and the bisimulation equivalence clearly guarantees the correctness of the reduction. On the other hand, the proposed method requires every RPDS (and RA) to have the freshness property, in which whenever the RPDS updates a register with a data value not stored in any register or the stack top, the value should be fresh. This paper also shows that the model checking problem with regular valuations defined by general RA is undecidable, and thus the freshness constraint is essential in the proposed method.

A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied and applied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values from an infinite domain. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show that the problems are EXPTIME-complete. As practical examples, we show solutions of a malware detection and an XML schema checking in the proposed framework.