Abstract: Security is essential for mobile systems. Usually mobile system modeling and its security policies specification are realized through different techniques. So when constructing a mobile system using formal methods, it is difficult to verify if the system comply with any given security policy. This paper introduces a method to express security policy specified by security automata as processes in an extended π-calculus. The method is very simple for realizing secure mobile computation.

Key words: mobile computation, safety property, security policy, security automaton, process

摘要： 安全策略为移动计算的安全性提供了必要的保证，而其表达和移动计算的形式化模型往往采用不同的技术实现。该文给出安全策略的一种进程表示方法，通过安全策略的进程表示，很容易将移动计算模型及移动计算的安全性问题在统一的框架下实现。为实现移动计算及其安全性提供了一种简单、可行的方法。

关键词: 移动计算, 安全属性, 安全策略, 安全自动机, 进程

CLC Number: 

• TP309