Categorical Models of Syntactic Control of Intereference Revisited, Revisited

The question of what categorical structure is required to give semantics to O‘Hearn et al.'s type system Syntactic Control of Interference Revisited (SCIR) is considered. The previously proposed notion of bireflective model is rejected as being too restrictive to accommodate important concrete models based on game semantics and object spaces; furthermore it is argued that the existing proof-sketch of the important property of coherence for these models is incorrect. A new, more general notion of model is proposed and the coherence property proved.

Unfair Noisy Channels and Oblivious Transfer

In a paper from EuroCrypt'99, Damgård, Kilian and Salvail show various positive and negative results on constructing Bit Commitment (BC) and Oblivious Transfer (OT) from Unfair Noisy Channels (UNC), i.e., binary symmetric channels where the error rate is only known to be in a certain interval [gamma ..delta] and can be chosen adversarily. They also introduce a related primitive called PassiveUNC. We prove in this paper that any OT protocol that can be constructed based on a PassiveUNC and is secure against a passive adversary can be transformed using a generic "compiler'' into an OT protocol based on a UNC which is secure against an active adversary. Apart from making positive results easier to prove in general, this also allows correcting a problem in the EuroCrypt'99 paper: There, a positive result was claimed on constructing from UNC an OT that is secure against active cheating. We point out that the proof sketch given for this was incomplete, and we show that a correct proof of a much stronger result follows from our general compilation result and a new technique for transforming between weaker versions of OT with different parameters.

Derivation of an Algorithm for Location Management for Mobile Communication Devices

In a network supporting mobile communication devices, a mechanism to find the location of a device, wherever it may be, is needed. In this paper, we present a distributed algorithm for this purpose along with its formal specification and proof sketch. Starting with an algorithm due to Wang, the process of formalization together with careful attention to abstraction leads to a more regular, general, and robust algorithm with a clearer description. An incidental contribution is a useful theorem for proving progress properties in distributed algorithms that use tokens.