Henning Schnoor

Henning Schnoor, Wilhelm Hasselbring

Coupling metrics are an established way to measure software architecture quality with respect to modularity. Static coupling metrics are obtained from the source or compiled code of a program, while dynamic metrics use runtime data gathered e.g., by monitoring a system in production. We study \emph{weighted} dynamic coupling that takes into account how often a connection is executed during a system's run. We investigate the correlation between dynamic weighted metrics and their static counterparts. We use data collected from four different experiments, each monitoring production use of a commercial software system over a period of four weeks. We observe an unexpected level of correlation between the static and the weighted dynamic case as well as revealing differences between class- and package-level analyses.

Wojciech Jamroga, Matthijs Melissen, Henning Schnoor

We study the security of interaction protocols when incentives of participants are taken into account. We begin by formally defining correctness of a protocol, given a notion of rationality and utilities of participating agents. Based on that, we propose how to assess security when the precise incentives are unknown. Then, the security level can be defined in terms of defender sets, i.e., sets of participants who can effectively "defend" the security property as long as they are in favor of the property. We present some theoretical characterizations of defendable protocols under Nash equilibrium, first for bijective games (a standard assumption in game theory), and then for games with non-injective outcomes that better correspond to interaction protocols. Finally, we apply our concepts to analyze fairness in the ASW contract-signing protocol.

Henning Schnoor, Oliver Woizekowski

We study linking attacks on communication protocols. We show that an active attacker is strictly more powerful in this setting than previously-considered passive attackers. We introduce a formal model to reason about active linkability attacks, formally define security against these attacks and give very general conditions for both security and insecurity of protocols. In addition, we introduce a composition-like technique that allows to obtain security proofs by only studying small components of a protocol.

Sebastian Eggert, Ron van der Meyden, Henning Schnoor et al.

The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable, as is checking ITO-security (van der Meyden). The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also lead to new unwinding proof techniques that are shown to be sound and complete for these notions of security, and enable the algorithms to return simple counter-examples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.

Rudolf Berghammer, Henning Schnoor

We present a relation-algebraic model of Condorcet voting and, based on it, relation-algebraic solutions of the constructive control problem via the removal of voters. We consider two winning conditions, viz. to be a Condorcet winner and to be in the (Gilles resp. upward) uncovered set. For the first condition the control problem is known to be NP-hard; for the second condition the NP-hardness of the control problem is shown in the paper. All relation-algebraic specifications we will develop in the paper immediately can be translated into the programming language of the BDD-based computer system RelView. Our approach is very flexible and especially appropriate for prototyping and experimentation, and as such very instructive for educational purposes. It can easily be applied to other voting rules and control problems.

Sebastian Eggert, Henning Schnoor, Thomas Wilke

We develop a theory for state-based noninterference in a setting where different security policies---we call them local policies---apply in different parts of a given system. Our theory comprises appropriate security definitions, characterizations of these definitions, for instance in terms of unwindings, algorithms for analyzing the security of systems with local policies, and corresponding complexity results.