Type-Based Security for Mobile Computing: Integrity, Secrecy and Liveness


Home
References
Investigators
Publications
Related Publications
Prototype

Objectives

  • To develop a general type-based framework to solve three issues concerning security: secrecy (privacy of data), liveness (availability) and integrity (access control and session integrity), using two basic concurrency models, the pi-calculus and the higher-order pi-calculus. Previous researches by myself with co-authors have shown that the typing systems of these models can be used as a tool to guarantee safe program mobility.
  • To apply the developed theory to the language design and implementation of mobile and communications programs by constructing a typing system for the subset of concurrent and distributed Java which can ensure safety with respect to secrecy, liveness and access integrity. We prove correctness of the typing system via a core Java models or extensions of mobile processes based on the first order or higher order pi-calculus developed in 1.
  • To apply the developed theory to the language design of mobile programs by constructing a typing system for the subset of multi-threaded Java which can ensure safety with respect to secrecy, liveness and access control. We prove correctness of the typing system via its translation into the higher order pi-calculus developed in 1.