A Syntactic Criterion for Injectivity of Authentication Protocols

Injectivity is essential when studying the correctness of authentication protocols, because noninjective protocols may suffer from replay attacks. The standard ways of verifying injectivity either make use of a counting argument, which only seems to be applicable in a verification methodology based on model-checking, or draw conclusions on the basis of the details of the data-model used. We propose and study a property, the loop property, that can be syntactically verified and is sufficient to guarantee injectivity. Our result is generic in the sense that it holds for a wide range of security protocol models, and does not depend on the details of message contents or nonce freshness.     

Making an engine: performativities of building information standards

ABSTRACT

Digitization of buildings requires the systematic handling of a variety and volumes of data. It is a common vision to aim for coordinated homogenization of data structures, enabled by the classification of information. This paper studies the role of building information standards for classification in digitization of the building life cycle. It draws on science and technology studies of information technology standards, big data and building information modelling (BIM) in building research. The approach is based on performativity of standards for information systems, viewing performativity as potentially non-linear and multiple. The five-year design process of a large hospital in Denmark is examined as episodes of performance of the building information standard, particularly one recent standard, the Cuneco Classification System (CCS). The study shows that despite client demands, several building information standards are active over time: an ‘expansive’ design brief process adds user demands and uses room classification. Another process diminishes the design brief more than 50%, with several standards in use. The client’s facilities management system, which performs the structuring of data ‘backwards’ into the design process, makes architects and engineers (but not contractors) use CCS. This fragmentation of performing standards is denoted ‘multiple performativities’ and includes temporal and compartmental performativity.     

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability.Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.     

Preventing active re-identification attacks on social graphs via sybil subgraph obfuscation

Knowledge and Information Systems - Active re-identification attacks constitute a serious threat to privacy-preserving social graph publication, because of the ability of active adversaries to...     

Game-based verification of contract signing protocols with minimal messages

A multi-party contract signing (MPCS) protocol is used for a group of signers to sign a digital contract over a network. We analyse the protocols of Mauw, Radomirović and Torabi Dashti (MRT), using the finite-state model checker Mocha. Mocha allows for the specification of properties in alternating-time temporal logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives us an intuitive interpretation of the verification problem of crucial properties of MPCS protocols. MRT protocols can be generated from minimal message sequences, depending on the number of signers. We discover an attack on fairness in a published MRT protocol with three signers and a general attack on abuse-freeness for all MRT protocols. For both attacks, we present solutions. The abuse-freeness attack leads us to a revision of the methodology to construct an MRT protocol. Following this revised methodology, we design a number of MRT protocols using minimal message sequences for three and four signers, all of whom have been successfully model checked in Mocha.     

An algorithm for the asynchronous Write-All problem based on process collision

Summary. The problem of using P processes to write a given value to all positions of a shared array of size N is called the Write-All problem. We present and analyze an asynchronous algorithm with work complexity , where (assuming and ). Our algorithm is a generalization of the naive two-processor algorithm where the two processes each start at one side of the array and walk towards each other until they collide. Received: October 1999 / Accepted: September 2000     

Task Allocation in a Multi-Server System

We consider a slotted queueing system with C servers (processors) that can handle tasks (jobs). Tasks arrive in batches of random size at the start of every slot. Any task can be executed by any server in one slot with success probability . If a task execution fails, then the task must be handled in some later time slot until it has been completed successfully. Tasks may be processed by several servers simultaneously. In that case, the task is completed successfully if the task execution is successful on at least one of the servers.We examine the impact of various allocation strategies on the mean number of tasks in the system and the mean response time of tasks. It is proven that both these performance measures are minimized by the strategy which always distributes the tasks over the servers as evenly as possible. Subsequently, we determine the distribution of the number of tasks in the system for a broad class of task allocation strategies, which includes the above optimal strategy as a special case. Some numerical experiments are performed to illustrate the performance characteristics of the various strategies.     

Design and analysis of dynamic leader election protocols in broadcast networks

Summary.  The well-known problem of leader election in distributed systems is considered in a dynamic context where processes may participate and crash spontaneously. Processes communicate by means of buffered broadcasting as opposed to usual point-to-point communication. In this paper we design a leader election protocol in such a dynamic context. As the problem at hand is considerably complex we develop the protocol in three steps. In the initial design processes are considered to be perfect and a leader is assumed to be present initially. In the second protocol, the assumption of an initial leader is dropped. This leads to a symmetric protocol which uses an (abstract) timeout mechanism to detect the absence of a leader. Finally, in the last step of the design processes may crash without giving any notification of other processes. The worst case message complexity of all protocols is addressed. A formal approach to the specification and verification of the leader election protocols is adopted. The requirements are specified in a property-oriented way and the protocols are denoted by means of extended finite state machines. It is proven using linear-time temporal logic that the fault-tolerant protocol satisfies its requirements. Received: September 1993 / Revised: September 1995