Laboratory of Mathematical Logic at PDMI

Пятница, 30 марта, ауд. 106. Начало в 18:00.

Докладчик: Andre Scedrov (University of Pennsylvania, USA).

Тема: Collaborative Systems.

Abstract

Our earlier work with Kanovich and Rowe introduced a model of collaboration, in which the participants are unwilling to share all their information with each other, but some information sharing is unavoidable when achieving a common goal. The need to share information and the desire to keep it confidential are two competing notions which affect the outcome of a collaboration. Our model is based on the notion of a plan which originates in the AI literature. Here we consider two extensions of the model. The first extension allows for updates of values with fresh ones, such as updating a password. The second extension allows for the specification of policies and systems with explicit time. Time is discrete and is specified by timestamps attached to facts. Actions, goal and critical states may be constrained by means of relative time constraints. All the players inside our system, including potential adversaries, have similar capabilities. They have bounded storage capacity, that is, they can only remember a bounded number of facts. This is technically imposed by allowing only the so-called balanced actions, that is, actions that have the same number of facts in their pre and post conditions. We investigate the complexity of the planning problem, whether the players can reach a goal while avoiding certain critical configurations along the way. We show that this problem is PSPACE-complete.

As an application we turn to network security protocol analysis and demonstrate> that when an adversary has enough storage capacity, then many known protocol anomalies can also occur in the presence of a bounded memory intruder. We believe that precisely this is a theoretical reason for the successful use in the past years of model checkers in security protocol verification. This is joint work with T. Ban Kirigin, M. Kanovich, V. Nigam, R. Perovic, and C. Talcott.