Global Types with Internal Delegation

in Theoretical Computer Science (2019)

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This ... [more ▼]

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This means that delegation is inherently an inter-session mechanism, which requires session interleaving. Hence delegation falls outside the descriptive power of global types, which specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. Here we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (internal delegation) and may be captured by its global type. To increase flexibility in the use of delegation, our calculus uses connecting communications, which allow optional participants in the branches of choices. By these means, we are able to express conditional delegation. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property. [less ▲]

Efficient Algorithms for Secure Outsourcing of Bilinear Pairings

in Theoretical Computer Science (2014)

The computation of bilinear pairings has been considered the most expensive operation in pairing-based cryptographic protocols. In this paper, we first propose an efficient and secure outsourcing ... [more ▼]

The computation of bilinear pairings has been considered the most expensive operation in pairing-based cryptographic protocols. In this paper, we first propose an efficient and secure outsourcing algorithm for bilinear pairings in the two untrusted program model. Compared with the state-of-the-art algorithm, adistinguishing property of our proposed algorithm is that the (resource-constrained) outsourcer is not required to perform any expensive operations, such as point multiplications or exponentiations. Furthermore, we utilize this algorithm as a subroutine to achieve outsource-secure identity-based encryptions and signatures. [less ▲]

A Comparison of Semantic Models for Noninterference

in Theoretical Computer Science (2010), 411(47), 41234147

The literature on definitions of security based on causality-like notions such as noninterference has used several distinct semantic models for systems. Early work was based on state machine and trace-set ... [more ▼]

The literature on definitions of security based on causality-like notions such as noninterference has used several distinct semantic models for systems. Early work was based on state machine and trace-set definitions; more recent work has dealt with definitions of security in two distinct process algebraic settings. Comparisons between the definitions has been carried out mainly within semantic frameworks. This paper studies the relationship between semantic frameworks, by defining mappings between a number of semantic models and studying the relationship between notions of noninterference under these mappings. [less ▲]