基于Agent的移动计算及其安全性研究
|
摘要
随着近来计算机网络技术、通信技术的飞速发展,基于因特网的全球性的计算平台已经建立起来;同时,由于高速无线通信技术的出现以及器件快速小型化,许多便携式设备如:笔记本电脑,移动电话,PDA,以及各种信息家电也接入到网络中来。以并发性、移动性、分布性、实时性、异构性和互操作性为主要特征的移动计算系统已经成为计算机技术领域的一个研究热点,很多研究成果已经在实际信息系统的开发中得到广泛应用。对于移动计算而言,安全性是移动计算能否成功应用的关键问题。
本文研究基于agent的移动计算系统的形式化理论和技术,并在形式化模型基础上深入研究了基于agent的移动计算系统的安全性理论和技术,包括静态安全性分析,安全信息流分析和基于安全自动机的动态监测技术,最后探讨了基于agent的移动基础设施和消息传递算法。主要工作包括以下六个方面:
(1)首先对移动计算系统中的安全要求、安全威胁和安全机制进行了讨论,提出了移动计算的统一安全框架,并指出在移动计算中可以在统一的形式化计算模型中描述移动计算系统并设计和表示不同的安全机制。
(2)在基于进程代数的π演算框架下,通过引入位置、计算边界和限制区域,建立了一个扩展的π演算模型:Confined-π演算。并在限制声明的基础上对进程的行为进行了规范,使得安全策略通过由计算边界定义的格和限制区域的包含关系编码到Confined-π演算中。
(3)在Confined-π演算平台上,从静态分析的角度考查了实现移动计算系统静态安全性分析的方法。通过在Confined-π演算中引入带安全标记(计算边界标记和限制区域标记)的类型系统,移动计算的安全要求,如限制agent移动和通信等,被转换成类型系统中的形式化特性,从而将移动计算系统中的一些安全性问题转化成基于类型的静态分析问题。
The recent rapid development of computer network technology and tele- communications technology have made it possible to envisage a global computing platform; Meanwhile, with rapid component miniaturization and the emergence of high-speed wireless communication, various devices like notebook computer, mobile phones, PDAs and other information home appliances are connected to the networks too. At present time, mobile computation system with properties like the concurrency, mobility, distribution, real time, heterogeneity and interoperability have become the main direction of current computer technology, and have been widely applied to development of real information system. For mobile computation, security is the key aspect for its successful application.
The formal methods and theory of mobile computation based on agent have been studied in this paper. Farther more, with the formal platform designed in this paper, a deep study relating to security in mobile computation have been carried off. These studies included static security analyzing, security information flow analyzing and dynamic monitoring technology based on security automaton. At last, a kind of mobile infrastructure and message passing algorithm based on agent have been designed. The main task includes the following six aspects:
(1) First, the security requirements, security threats and security mechanisms have been deeply studied, then constructed a uniform security structure in mobile computation. The mobile system description and security formality can be
本文研究基于agent的移动计算系统的形式化理论和技术,并在形式化模型基础上深入研究了基于agent的移动计算系统的安全性理论和技术,包括静态安全性分析,安全信息流分析和基于安全自动机的动态监测技术,最后探讨了基于agent的移动基础设施和消息传递算法。主要工作包括以下六个方面:
(1)首先对移动计算系统中的安全要求、安全威胁和安全机制进行了讨论,提出了移动计算的统一安全框架,并指出在移动计算中可以在统一的形式化计算模型中描述移动计算系统并设计和表示不同的安全机制。
(2)在基于进程代数的π演算框架下,通过引入位置、计算边界和限制区域,建立了一个扩展的π演算模型:Confined-π演算。并在限制声明的基础上对进程的行为进行了规范,使得安全策略通过由计算边界定义的格和限制区域的包含关系编码到Confined-π演算中。
(3)在Confined-π演算平台上,从静态分析的角度考查了实现移动计算系统静态安全性分析的方法。通过在Confined-π演算中引入带安全标记(计算边界标记和限制区域标记)的类型系统,移动计算的安全要求,如限制agent移动和通信等,被转换成类型系统中的形式化特性,从而将移动计算系统中的一些安全性问题转化成基于类型的静态分析问题。
The recent rapid development of computer network technology and tele- communications technology have made it possible to envisage a global computing platform; Meanwhile, with rapid component miniaturization and the emergence of high-speed wireless communication, various devices like notebook computer, mobile phones, PDAs and other information home appliances are connected to the networks too. At present time, mobile computation system with properties like the concurrency, mobility, distribution, real time, heterogeneity and interoperability have become the main direction of current computer technology, and have been widely applied to development of real information system. For mobile computation, security is the key aspect for its successful application.
The formal methods and theory of mobile computation based on agent have been studied in this paper. Farther more, with the formal platform designed in this paper, a deep study relating to security in mobile computation have been carried off. These studies included static security analyzing, security information flow analyzing and dynamic monitoring technology based on security automaton. At last, a kind of mobile infrastructure and message passing algorithm based on agent have been designed. The main task includes the following six aspects:
(1) First, the security requirements, security threats and security mechanisms have been deeply studied, then constructed a uniform security structure in mobile computation. The mobile system description and security formality can be
引文
[1] G.H. Forman and J. Zahorjan, The Challenges of Mobile Computing, Computer, vol. 27, no. 4, 38–47, 1994.
[2] M.Satyanarayanan, Fundamental Challenges in Mobile Computing, Proc. ACM SigMobile, 1, 1, 1- 7, April 1997.
[3] G.C.Roman, A.L.Murphy, G.P.Picco, A Software Engineering Perspective on Mobility, In The Future of Software Engineering, Ed. A. Finkelstein, ACM Press, pp. 241-258, 2000.
[4] G.C. Roman, A.L. Murphy, and G.P. Picco, Coordination and Mobility, In Coordination of Internet Agents: Models, Technologies, and Applications, Ed. A. Omicini, F. Zambonelli, M. Klusch, and R. Tolksdorf, Springer, pp. 254-273, 2000.
[5] Dijkstra, E.W. A constructive approach to the problem of program corrcctness. BIT 8 (1968), 174-186.
[6] Dijkstra, E,W, Hierarchical ordering of sequential processes. In Operating Systems Techniques, Academic Press, New York, 1972.
[7] Hoare, C.A.R. Towards a theory of parallel programming. In Operating Systens techniques, Academic Press, New York, 1972.
[8] Hoare, C.A.R. Proof of correctness of data representations. Acta Informatica 1 (1972), 271-281.
[9] D. S. Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Science and Systems, 1970.
[10] D. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Tech. mono. PRC6, 1971.
[11] M. B. Smyth. Effectivly given domains. Theoretical Computer Science, 5, 1977.
[12] D. Kozen. Semantics of probabilistic programs. Computer and System Sciences, 22(3), 1981.
[13] G.D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
[14] G.D. Plotkin, Lecture notes in domain theory, University of Edinburgh, 1981.
[15] David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981 .
[16] Robin Milner, Communicating and mobile Systems: The π-calculus, Cambridge University Press, 1999.
[17] Sangiorgi D., Walker D. The π-calculus: a Theory of Mobile Processes [M]. Cambridge University Press, 2001.
[18] Hennessy M., Riely J., Resource access control in systems of mobile agents, Information and Computation, Volume 173, Number 1, pp. 82-120(39), February 2002.
[19] Roberto M. Amadio, Sanjiva Prasad. Localities and Failures [C]. In FST-TCS, volume 880 of LNCS. Springer, 1994.
[20] K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In Proc. of ECOOP'91 Workshop, LNCS 612, pages 21-- 51, 1991.
[21] Tom Chothia and Ian Stark, A distributed calculus with local areas of communication, In HLCL 2000: Proceedings of the 4th International Workshop on High-Level Concurrent Languages. Montreal, Canada, September 20, 2000.
[22] ASIS U. Nomadic π-calculus: Its Theories and Applications [M]. PhD thesis, University of Cambridge, Computer Laboratory. 2001 March.
[23] A. Church, The Calculi of Lambda Conversion, Princeton University Press, 1941.
[24] Sekiguchi, T., Yonezawa, A.: A calculus with code mobility. In: FMOODS ’97: Proceeding of the IFIP TC6 WG6.1 International Workshop on Formal Methods for Open Object-based Distributed Systems, Chapman & Hall, Ltd. (1997) 21–36.
[25] Cardelli L., Gordon A.D., Mobile Ambients, In Maurice Nivat, editor, Proc. FOSSACS'98, International Conference on Foundations of Software Science and Computation Structures, volume 1378 of Lecture Notes in Computer Science, pages 140-155. Springer-Verlag, 1998.
[26] J.Vitek and G.Castagna, A calculus of secure mobile computations. In Proceedings of the IEEE Workshop on Internet Programming Languages, (WIPL). Chicago, Ill, 1998.
[27] G.C.Roman, P,J. McCann, J,Y. Plun, Mobile UNITY: reasoning and specification in mobile computing, ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 6, Issue 3, 250 – 282, 1997.
[28] Hyacinth S. Nwana, Software Agents:An Overview, Knowledge Engineering Review, Vol. 11, No 3, pp.1-40, Sept 1996.
[29] Minshy,Marvin,The society of Mind.NewYork:Simo and Schuster,1985.
[30] Genesereth M.R,Ketchet S P. Software agents. Communication of the ACM,1993,37(7):48-53.
[31] Wooldrige, N,Jennings N R. Intelligent agent: theory and practice. The Knowledge Engineering Review, 1995, 13(2):115-152.
[32] ShohamY., Agent-oriented programming: An Overview and Summary of recent research,In proc。Of Artificial Intelligence,1992.
[33] M.Baldi et al, Exploiting Code Mobility in Decentralized and Flexible Network Management, Mobile Agents, Lecture Notes in Comp.Sci.Series,Vol.1219,pp.13-26,Springer,1997.
[34] K.Schelderup, J.Olnes, Mobile Agent Security: Issues and Directions. In IS&N’99,volume LNCS1597,Mar.1999.
[35] H. S. Nwana & D. T. Ndumu, A Perspective on Software Agents Research, In: The Knowledge Engineering Review, Vol 14, No 2, pp 1-18, 1999.
[36] M.S.Greenberg, J.C.Byington, Mobile Agents and Security, IEEE Communications Magazine, 76-85,1998.
[37] Vu Anh Pham, A.Karmouch, Mobile Software Agents: An Overview, IEEE Communications Magazine, 26-37, 1998.
[38] Neeran M.Karnik, Anand R.Tripathi, A Security Architecture for Mobile Agents in Ajanta, Proceedings of the The 20th International Conference on Distributed Computing Systems ( ICDCS 2000), 2000.
[39] G.Karjoth,D.Lange,and M.Oshima. A Security Model for Aglets. IEEE Internet Computing,4(1):68-77,July-August 1997.
[40] K.Schelderup and J.Olnes.Mobile Agent Security:Issues and Directions.In IS&N’99,volume LNCS1597,Mar.1999.
[41] Dennis M. Volpano, Geoffrey Smith: Language Issues in Mobile Program Security. Mobile Agents and Security 1998: 25-43.
[42] R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc. Secaucus, NJ, USA , 1982.
[43] H.Baker, C.Hewitt, The Incremental Garbage Collection of Processes", ACM Sigplan Notices 12, 8, 55-59, 1977.
[44] J.M.Lucassen, Types and Effects-Towards the Integration of Functional and Imperative Programming. PHD thesis, MIT Laboratory for Computer Science, 1987.
[45] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference for partial types. Information Processing Letters, 43:175--180, 1992.
[46] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128--141, 1995.
[47] A.Aiken, M.Fahndrich, and R.Levien, Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation, 174-185, La Jolla, California, 1995.
[48] Ole Agesen, David L. Detlefs, J. Eliot B. Moss. 1998. Garbage Collection and Local Variable Type-precision and Liveness in JavaTM Virtual Machines . ACM. Proceedings of the ACM SIGPLAN '98 conference on Programming language design and implementation, pages 269-279.
[49] D.P.Walker, Typed memory management, PHD thesis, Cornell University, 2001.
[50] A. Salcianu, C. Boyapati, W. Beebee, Jr., and M. Rinard., A Type System for Safe Region-Based Memory Management in Real-Time Java, Technical Report TR-869, MIT Laboratory for Computer Science, November 2002.
[51] C. Boyapati, A. Salcianu, W. Beebee, Jr., and M. Rinard. Ownership types for safe region-based memory management in Real-Time Java. In Programming Language Design and Implementation (PLDI), June 2003.
[52] Chandrasekhar Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, February 2004.
[53] R.S.Sandhu, G.S.Suri, Implementation considerations for the typed access matrix model in a distributed environment, In Proceeding of the 15th NISTNCSC National Computer Security Conference, 1992.
[54] J.Tidswell, J.Potter, Domain and Type Enforcement in a μ-Kernel, In Proceedings of the 20th Australasian Computer Science Conference, 1997.
[55] J.Tidswell, J.Potter, A Dynamically Typed Access Control Model. In Proceedings of the Third Australasian Conference on Information Security and Privacy, 1998.
[56] Jonathon E. Tidswell, Geo rey H. Outhred, and John M. Potter. Dynamic rights: Safe extensible access control. In Workshop on Role-based Access Control, 1999.
[57] Tom Chothia, Dominic Duggan, and Jan Vitek, Type-Based Distributed Access Control, In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), pages 170-186. IEEE Computer Society, 2003.
[58] T.Higuchi, Atsushi Ohori, A Static Type System for JVM Access Control, ACM ICFP Conference, 2003.
[59] M.Bugliesi, D.Colazzo and S.Crafa, Type Based Discretionary Access Control. CONCUR'04 - Concurrency Theory. LNCS n.3170, 2004.
[60] D. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236--242, 1976.
[61] Dorothy E. Denning and Peter J. Denning. Certification of programs for secure information flow. Communication of the ACM, 20(7):504-512, July 1977.
[62] Neil D. Jones. Flow analysis of lambda expressions. In Proceedings of Eighth Colloquium on Automata, Languages, and Programming, volume 115 of LNCS. Springer-Verlag, 1981.
[63] R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85--97, 1985.
[64] Sutherland. A model of information. Proceedings of the 9th National Computer Security Conference; National Bureau of Standards, National Computer Security Center, 15.-18. September 1986, 175-183.
[65] Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In Functional Programming Languages and Computer Architecture, pages 260-272, September 1989.
[66] J. Palsberg and P. O'Keefe. A type system equivalent to flow analysis. In 22nd symposium Principles of Programming Languages, pages 367-378. ACM Press, 1995.
[67] N. Heintze. Control-flow analysis and type systems. In Proc. 2nd Int'l Static Analysis Symp., pp. 189--206, 1995.
[68] D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1-21, 1996.
[69] D. Volpano and G. Smith. A type-based approach to program security. In Proceedings of TAPSOFT'97, Colloqium on Formal Approaches in Software Engineering, 1997.
[70] Tse and S. Zdancewic. Run-time principals in information-flow type systems. Technical Report MSCIS -03-39, University of Pennsylvania, 2004.
[71] N. Heintze and D. McAllester. On the cubic bottleneck in subtyping and flow analysis. In LICS '97: Proceedings of the IEEE Symposium on Logic in Computer Science, 1997.
[72] F.Nielson, H.R.Nielson, C.Hankin, Principles of Program Analysis, Springer-Verlag press, Berlin Heidelberg, 1999.
[73] T.Amtoft, F.Nielson, H.R.Nielson, Type and effect Systems: Behaviours for Concurrency, Imperial College Press, 1999.
[74] Geoffrey Smith. A new type system for secure information flow. In CSFW14, pages 115--125. IEEE Computer Society Press, jun 2001.
[75] A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
[76] G.Barthe, L.P.Nieto, Formally verifying information flow type systems for concurrent and thread systems, Proceedings of the 2004 ACM workshop on Formal methods in security engineering table of contents, Washington DC, USA, Pages: 13 – 22, 2004.
[77] H.R.Nielson and Flemming, Nielson, Automatic binding time analysis for a typed lambda calculus. Science of Computer Programming, pages 139-176, 1988.
[78] J.P.Talpin and P. Jouvelot, The type and effect disipline. In Proceedings of LICS'92, 1992.
[79] R.T.Oehrle, Term-labeled Categorial Type Systems, Linguistics and Philosophy, 17:633—678, 1994.
[80] Yan-Mei Tang, Control-Flow Analysis by Effect Systems and Abstract Interpretation. PhD thesis, Ecole National Superieure des Mines de Paris, 1994.
[81] K.L.Solberg, Annotated type systems for program analysis, Phd thesis, Aarhu University, Denmark, 1995.
[82] Flemming Nielson, Annotated type and effect systems, ACM Computing Surveys (CSUR), Vol.28(2), 344 – 345, 1996.
[83] N.Heintze, Jon G., Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, San Diego, California, United States, 365 – 377, 1998.
[84] Z.D.Kirli, Mobile Computation with Functions, Kluwer Academic Publishers, 2002.
[85] Steve Zdancewic, A Type System for Robust Decalssification, Theoretical Computer Science vol.83,1-16, 2004.
[86] Lhoussaine, C. and Sassone, V., A Dependently Typed Ambient Calculus. In Proceedings of European Symposium on Programming, ESOP'04. Lecture Notes in Computer Science 2986, pp. 171-187, 2004.
[87] Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon, Types for the Ambient Calculus, Information and Computation, Vol.177(2), IFIP TCS2000, 160 – 194, 2002.
[88] B. Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, Math. Struct. Comput. Sci.6(5)409-454, 1996.
[89] Davide Sangiorgi. An interpretation of typed objects into typed pi-calculus. INRIA RR-3000, 1996.
[90] K.Honda,V.T.Vasconcelos, N.Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.180-199, April 02, 2000.
[91] Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, 2002.
[92] Nobuko Yoshida , Matthew Hennessy, Assigning types to processes, Information and Computation, v.174 n.2, p.143-179, 2002.
[93] A. Igarashi, N. Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, Vol.311(1-3), 121 – 163, 2004.
[94] Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, 33 – 44, 2006.
[95] AD Gordon, M Abadi, A Calculus for Cryptographic Protocols: The Spi Calculus, 4th ACM Conference on Computer and Communications Security, 1997.
[96] AD Gordon, Nominal Calculi for Security and Mobility, DARPA Workshop on Foundations for Secure Mobile Code, 1997.
[97] Hennessy M., Riely J., Information flow vs resource access in the asynchronous pi-calculus, ICALP00, LNCS 1853, 415-427, Springer, 2000.
[98] Hennessy M., The security pi-calculus and noninterference, Technical Report 2000:05, University of Susex, 2000.
[99] F.Pottier, A simple view of type-secure information flow in the pi calculus, 320-330, 2002.
[100] Naoki Kobayashi. Type-based information flow analysis for the pi-calculus. Technical Report TR030007, Department of Computer Science, Tokyo Institute of Technology, October 2003.
[101] S.Eilenberg, Automata, Languages and Machines, Vol A. Academic Press, New York, 1974.
[102] L.Lamport, Proving the correctness of multiprocess programs, IEEE Trans. On Software Engineering SE-3, 2, 125-143, 1977.
[103] S. Owicki, L.Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol.4(3), 455 – 495, 1982.
[104] J. P. Queille and J. Sifakis. Speci_cation and veri_cation of concurrent systems in CESAR. In Proc. of the 5th international Symposium on Programming,vol. 137 of LNCS, 1982.
[105] B.Alpern and F.B.Schneider. Defning liveness. Information Processing Letters, 21(4):181-185, 1985.
[106] B.Alpern and F.B.Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117-126, 1987.
[107] H.P. Gumm. Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. Information Processing Letters,47 (6):291-294, 1993.
[108] E. Kindler. Safety and liveness properties: A survey. EATCS-Bulletin, 53:268{272, June 1994.
[109] A. P. Sistla. Safety, Liveness and fairness in temporal logic. Formal aspects of Computing, 6:495-511, 1994.
[110] F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security(TISSEC), 3(1):30-50, 2000.
[111] Ulfar Erlingsson, Schneider, SASI enforcement of security policies: a retrospective, New Security Paradigms Workshop, Proceedings of the 1999 workshop on New security paradigms, 87–95, 1999.
[112] David Walker, A Type System for Expressive Security Policies, Twenty-Seventh ACM SIGPLAN Symposium on Principles of Programming Languages, 254-267, Boston, 2000.
[113] L.Bauer, J.Ligatti and David Walker, Types and Effects for Non-interfering Program Monitors, International Symposium on Software Security, Tokyo,2002. Revised for printing in Software Security-Theory and Systems, LNCS 2609, Springer, pp 154-171. December 2002.
[114] Glynn Winkel, Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk, In BRICS reports series RS-94-1, 1994.
[115] R.Milner, A calculus of communicating systems, Lecture Notes in Computer Science, Vol92, Springer-Verlag, 1980.
[116] R.Milner, Communication and Concurrency, Pretice Hall, 1989.
[117] Hoare C., Communicating Sequential Processes, Prentice Hall, 1985.
[118] T. Thorn. Programming Languages for Mobile Code. ACM Cumpting Surveys, 29(3):213--239, September 1997.
[119] Commission of the European Communities, Information Technology Security Evaluation Criteria(ITSEC), Version 1.2, 1991.
[120] J. A. Goguen and J. Meseguer, Security Policies and Security Models, Proceedings of the 1982 IEEE Symposium on Security and Privacy, Washington D.C., 1982.
[121] R.Focardi, R.Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security , 3(1): 5-33, 1995.
[122] R. Focardi and R. Gorrieri, Non Interference: Past, Present and Future, In Proceedings of 1997 Foundations for Secure Mobile Code Workshop, 33-36, Sponsored by DARPA, 1997.
[123] Riccardo Focardi, Roberto Gorrieri: Classification of Security Properties (Part I: Information Flow). FOSAD 2000: 331-396, 2000.
[124] R. Focardi, R. Gorrieri, and F. Martinelli, Classification of Security Properties (Part II: Network Security), Tutorial Lectures, LNCS 2946, Springer, 2004.
[125] P.T.Wojciechowski, P.Sewell, Nomadic Pict Language and infrastructure design for mobile agent, Agent Systems and Applications, Third International Symposium on Mobile Agents. Proceedings. First International Symposium on, 3-6:2 - 12 ,Oct. 1999.
[126] P.T.Wojciechowski, Nomadic Pict: Language and infrastructure design for mobile Computation, PHD thesis, University of Cambridge, 2000.
[127] J.Riely and M.Hennessy, Trust and partial typing in open systems of mobile agents. Technical Report 4, Computer Science, University of Sussex, 1998.
[128] J.Riely and M.Hennessy, Distributed Processes and Location Failures, Final version appeared in Theoretical Computer Science, 226:693-735, 2001.
[129] Roberto M. Amadio: An Asynchronous Model of Locality, Failurem and Process Mobility, COORDINATION 1997: 374-391, 1997.
[130] A.Francalanza, M.Hennessy, A Study of System Behaviour in the presence of Node and Link Failure, Mikado/Myths Workshop, Sussex, England, June 2003.
[131] A.Francalanza, M.Hennessy, A Theory of System Behaviour in the Presence of Node and Link Failures, LNCS, CONCUR 2005 – Concurrency Theory, Springer Berlin / Heidelberg, 368-382, 2005.
[132] A.Francalanza, A Study of Failure in a Distributed Pi-calculus, PHD Thesis, University of Sussex, 2005.
[133] G.Berry, G.Boudol, The chemical abstract machine, Selected papers of the Second Workshop on Concurrency and compositionality, San Miniato, Italy, 217 – 248, 1992.
[134] 任洪敏,基于 Pi 演算的软件体系结构形式化研究,博士论文,复旦大学,2003。
[135] 廖军 , 谭浩 , 刘锦德,基于 Pi-演算的 Web 服务组合的描述和验证,计算机学报,28(4),635-643,2005。
[136] 廖军 , 谭浩 , 刘锦德,基于 Pi-演算的 Web 服务可替换性验证,华中科技大学学报,33(8),168～171,2005。
[137] D.Sangiorgi. Bisimulation for higher-order process calculi. Information and Computation , 131(2):141-178, 15 December 1996.
[138] B Awerbuch, D Peleg, Online tracking of mobile users, Journal of the ACM, 1995, 42(5):1021-1058.
[139] A. Tanenbaum, M V Steen, Distributed Systems Principles and Paradigms, Prentice Hall Inc., 2002, 57-66.
[140] P. T. Wojciechowski. Nomadic Pict: Language and Infrastucture Design for Mobile Computation, Univeristy of Cambridge, Phd thesis, 2000.
[141] J. Baumann, F. Hohl, M. Straber et al, Mole-Concepts of a mobile agent system, World Wide Web Journal, 1998, 1(3):123-137.
[142] E. Jul, H. Levy, N. Hutchinson et al, Fine-Grained mobility in the emerald system, ACM Transactions on Computer Systems, 1988,6(2):109-133.
[143] A. L. Murphy, G. P. Picco, Reliable communication for highly mobile Agents, Proceedings of the 1st International Symposium on Agent Systems and Applications. New York: IEEE Computer Society, 1999:141-150.
[144] P.C.Kanellakis, S.A.Smolka, CCS expressions, finite state processes and three problems of equivalence, Journal of Information and Computation (86) 43-68, 1990.
[145] M.Hennessy, H.Lin, Symbolic bisimulations, Theoretical Computer Science, (138) 353-389, 1995.
[2] M.Satyanarayanan, Fundamental Challenges in Mobile Computing, Proc. ACM SigMobile, 1, 1, 1- 7, April 1997.
[3] G.C.Roman, A.L.Murphy, G.P.Picco, A Software Engineering Perspective on Mobility, In The Future of Software Engineering, Ed. A. Finkelstein, ACM Press, pp. 241-258, 2000.
[4] G.C. Roman, A.L. Murphy, and G.P. Picco, Coordination and Mobility, In Coordination of Internet Agents: Models, Technologies, and Applications, Ed. A. Omicini, F. Zambonelli, M. Klusch, and R. Tolksdorf, Springer, pp. 254-273, 2000.
[5] Dijkstra, E.W. A constructive approach to the problem of program corrcctness. BIT 8 (1968), 174-186.
[6] Dijkstra, E,W, Hierarchical ordering of sequential processes. In Operating Systems Techniques, Academic Press, New York, 1972.
[7] Hoare, C.A.R. Towards a theory of parallel programming. In Operating Systens techniques, Academic Press, New York, 1972.
[8] Hoare, C.A.R. Proof of correctness of data representations. Acta Informatica 1 (1972), 271-281.
[9] D. S. Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Science and Systems, 1970.
[10] D. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Tech. mono. PRC6, 1971.
[11] M. B. Smyth. Effectivly given domains. Theoretical Computer Science, 5, 1977.
[12] D. Kozen. Semantics of probabilistic programs. Computer and System Sciences, 22(3), 1981.
[13] G.D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
[14] G.D. Plotkin, Lecture notes in domain theory, University of Edinburgh, 1981.
[15] David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981 .
[16] Robin Milner, Communicating and mobile Systems: The π-calculus, Cambridge University Press, 1999.
[17] Sangiorgi D., Walker D. The π-calculus: a Theory of Mobile Processes [M]. Cambridge University Press, 2001.
[18] Hennessy M., Riely J., Resource access control in systems of mobile agents, Information and Computation, Volume 173, Number 1, pp. 82-120(39), February 2002.
[19] Roberto M. Amadio, Sanjiva Prasad. Localities and Failures [C]. In FST-TCS, volume 880 of LNCS. Springer, 1994.
[20] K. Honda and M. Tokoro. On Asynchronous Communication Semantics. In Proc. of ECOOP'91 Workshop, LNCS 612, pages 21-- 51, 1991.
[21] Tom Chothia and Ian Stark, A distributed calculus with local areas of communication, In HLCL 2000: Proceedings of the 4th International Workshop on High-Level Concurrent Languages. Montreal, Canada, September 20, 2000.
[22] ASIS U. Nomadic π-calculus: Its Theories and Applications [M]. PhD thesis, University of Cambridge, Computer Laboratory. 2001 March.
[23] A. Church, The Calculi of Lambda Conversion, Princeton University Press, 1941.
[24] Sekiguchi, T., Yonezawa, A.: A calculus with code mobility. In: FMOODS ’97: Proceeding of the IFIP TC6 WG6.1 International Workshop on Formal Methods for Open Object-based Distributed Systems, Chapman & Hall, Ltd. (1997) 21–36.
[25] Cardelli L., Gordon A.D., Mobile Ambients, In Maurice Nivat, editor, Proc. FOSSACS'98, International Conference on Foundations of Software Science and Computation Structures, volume 1378 of Lecture Notes in Computer Science, pages 140-155. Springer-Verlag, 1998.
[26] J.Vitek and G.Castagna, A calculus of secure mobile computations. In Proceedings of the IEEE Workshop on Internet Programming Languages, (WIPL). Chicago, Ill, 1998.
[27] G.C.Roman, P,J. McCann, J,Y. Plun, Mobile UNITY: reasoning and specification in mobile computing, ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 6, Issue 3, 250 – 282, 1997.
[28] Hyacinth S. Nwana, Software Agents:An Overview, Knowledge Engineering Review, Vol. 11, No 3, pp.1-40, Sept 1996.
[29] Minshy,Marvin,The society of Mind.NewYork:Simo and Schuster,1985.
[30] Genesereth M.R,Ketchet S P. Software agents. Communication of the ACM,1993,37(7):48-53.
[31] Wooldrige, N,Jennings N R. Intelligent agent: theory and practice. The Knowledge Engineering Review, 1995, 13(2):115-152.
[32] ShohamY., Agent-oriented programming: An Overview and Summary of recent research,In proc。Of Artificial Intelligence,1992.
[33] M.Baldi et al, Exploiting Code Mobility in Decentralized and Flexible Network Management, Mobile Agents, Lecture Notes in Comp.Sci.Series,Vol.1219,pp.13-26,Springer,1997.
[34] K.Schelderup, J.Olnes, Mobile Agent Security: Issues and Directions. In IS&N’99,volume LNCS1597,Mar.1999.
[35] H. S. Nwana & D. T. Ndumu, A Perspective on Software Agents Research, In: The Knowledge Engineering Review, Vol 14, No 2, pp 1-18, 1999.
[36] M.S.Greenberg, J.C.Byington, Mobile Agents and Security, IEEE Communications Magazine, 76-85,1998.
[37] Vu Anh Pham, A.Karmouch, Mobile Software Agents: An Overview, IEEE Communications Magazine, 26-37, 1998.
[38] Neeran M.Karnik, Anand R.Tripathi, A Security Architecture for Mobile Agents in Ajanta, Proceedings of the The 20th International Conference on Distributed Computing Systems ( ICDCS 2000), 2000.
[39] G.Karjoth,D.Lange,and M.Oshima. A Security Model for Aglets. IEEE Internet Computing,4(1):68-77,July-August 1997.
[40] K.Schelderup and J.Olnes.Mobile Agent Security:Issues and Directions.In IS&N’99,volume LNCS1597,Mar.1999.
[41] Dennis M. Volpano, Geoffrey Smith: Language Issues in Mobile Program Security. Mobile Agents and Security 1998: 25-43.
[42] R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc. Secaucus, NJ, USA , 1982.
[43] H.Baker, C.Hewitt, The Incremental Garbage Collection of Processes", ACM Sigplan Notices 12, 8, 55-59, 1977.
[44] J.M.Lucassen, Types and Effects-Towards the Integration of Functional and Imperative Programming. PHD thesis, MIT Laboratory for Computer Science, 1987.
[45] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference for partial types. Information Processing Letters, 43:175--180, 1992.
[46] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128--141, 1995.
[47] A.Aiken, M.Fahndrich, and R.Levien, Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation, 174-185, La Jolla, California, 1995.
[48] Ole Agesen, David L. Detlefs, J. Eliot B. Moss. 1998. Garbage Collection and Local Variable Type-precision and Liveness in JavaTM Virtual Machines . ACM. Proceedings of the ACM SIGPLAN '98 conference on Programming language design and implementation, pages 269-279.
[49] D.P.Walker, Typed memory management, PHD thesis, Cornell University, 2001.
[50] A. Salcianu, C. Boyapati, W. Beebee, Jr., and M. Rinard., A Type System for Safe Region-Based Memory Management in Real-Time Java, Technical Report TR-869, MIT Laboratory for Computer Science, November 2002.
[51] C. Boyapati, A. Salcianu, W. Beebee, Jr., and M. Rinard. Ownership types for safe region-based memory management in Real-Time Java. In Programming Language Design and Implementation (PLDI), June 2003.
[52] Chandrasekhar Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, February 2004.
[53] R.S.Sandhu, G.S.Suri, Implementation considerations for the typed access matrix model in a distributed environment, In Proceeding of the 15th NISTNCSC National Computer Security Conference, 1992.
[54] J.Tidswell, J.Potter, Domain and Type Enforcement in a μ-Kernel, In Proceedings of the 20th Australasian Computer Science Conference, 1997.
[55] J.Tidswell, J.Potter, A Dynamically Typed Access Control Model. In Proceedings of the Third Australasian Conference on Information Security and Privacy, 1998.
[56] Jonathon E. Tidswell, Geo rey H. Outhred, and John M. Potter. Dynamic rights: Safe extensible access control. In Workshop on Role-based Access Control, 1999.
[57] Tom Chothia, Dominic Duggan, and Jan Vitek, Type-Based Distributed Access Control, In 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), pages 170-186. IEEE Computer Society, 2003.
[58] T.Higuchi, Atsushi Ohori, A Static Type System for JVM Access Control, ACM ICFP Conference, 2003.
[59] M.Bugliesi, D.Colazzo and S.Crafa, Type Based Discretionary Access Control. CONCUR'04 - Concurrency Theory. LNCS n.3170, 2004.
[60] D. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236--242, 1976.
[61] Dorothy E. Denning and Peter J. Denning. Certification of programs for secure information flow. Communication of the ACM, 20(7):504-512, July 1977.
[62] Neil D. Jones. Flow analysis of lambda expressions. In Proceedings of Eighth Colloquium on Automata, Languages, and Programming, volume 115 of LNCS. Springer-Verlag, 1981.
[63] R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85--97, 1985.
[64] Sutherland. A model of information. Proceedings of the 9th National Computer Security Conference; National Bureau of Standards, National Computer Security Center, 15.-18. September 1986, 175-183.
[65] Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In Functional Programming Languages and Computer Architecture, pages 260-272, September 1989.
[66] J. Palsberg and P. O'Keefe. A type system equivalent to flow analysis. In 22nd symposium Principles of Programming Languages, pages 367-378. ACM Press, 1995.
[67] N. Heintze. Control-flow analysis and type systems. In Proc. 2nd Int'l Static Analysis Symp., pp. 189--206, 1995.
[68] D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1-21, 1996.
[69] D. Volpano and G. Smith. A type-based approach to program security. In Proceedings of TAPSOFT'97, Colloqium on Formal Approaches in Software Engineering, 1997.
[70] Tse and S. Zdancewic. Run-time principals in information-flow type systems. Technical Report MSCIS -03-39, University of Pennsylvania, 2004.
[71] N. Heintze and D. McAllester. On the cubic bottleneck in subtyping and flow analysis. In LICS '97: Proceedings of the IEEE Symposium on Logic in Computer Science, 1997.
[72] F.Nielson, H.R.Nielson, C.Hankin, Principles of Program Analysis, Springer-Verlag press, Berlin Heidelberg, 1999.
[73] T.Amtoft, F.Nielson, H.R.Nielson, Type and effect Systems: Behaviours for Concurrency, Imperial College Press, 1999.
[74] Geoffrey Smith. A new type system for secure information flow. In CSFW14, pages 115--125. IEEE Computer Society Press, jun 2001.
[75] A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
[76] G.Barthe, L.P.Nieto, Formally verifying information flow type systems for concurrent and thread systems, Proceedings of the 2004 ACM workshop on Formal methods in security engineering table of contents, Washington DC, USA, Pages: 13 – 22, 2004.
[77] H.R.Nielson and Flemming, Nielson, Automatic binding time analysis for a typed lambda calculus. Science of Computer Programming, pages 139-176, 1988.
[78] J.P.Talpin and P. Jouvelot, The type and effect disipline. In Proceedings of LICS'92, 1992.
[79] R.T.Oehrle, Term-labeled Categorial Type Systems, Linguistics and Philosophy, 17:633—678, 1994.
[80] Yan-Mei Tang, Control-Flow Analysis by Effect Systems and Abstract Interpretation. PhD thesis, Ecole National Superieure des Mines de Paris, 1994.
[81] K.L.Solberg, Annotated type systems for program analysis, Phd thesis, Aarhu University, Denmark, 1995.
[82] Flemming Nielson, Annotated type and effect systems, ACM Computing Surveys (CSUR), Vol.28(2), 344 – 345, 1996.
[83] N.Heintze, Jon G., Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, San Diego, California, United States, 365 – 377, 1998.
[84] Z.D.Kirli, Mobile Computation with Functions, Kluwer Academic Publishers, 2002.
[85] Steve Zdancewic, A Type System for Robust Decalssification, Theoretical Computer Science vol.83,1-16, 2004.
[86] Lhoussaine, C. and Sassone, V., A Dependently Typed Ambient Calculus. In Proceedings of European Symposium on Programming, ESOP'04. Lecture Notes in Computer Science 2986, pp. 171-187, 2004.
[87] Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon, Types for the Ambient Calculus, Information and Computation, Vol.177(2), IFIP TCS2000, 160 – 194, 2002.
[88] B. Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, Math. Struct. Comput. Sci.6(5)409-454, 1996.
[89] Davide Sangiorgi. An interpretation of typed objects into typed pi-calculus. INRIA RR-3000, 1996.
[90] K.Honda,V.T.Vasconcelos, N.Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.180-199, April 02, 2000.
[91] Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, 2002.
[92] Nobuko Yoshida , Matthew Hennessy, Assigning types to processes, Information and Computation, v.174 n.2, p.143-179, 2002.
[93] A. Igarashi, N. Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, Vol.311(1-3), 121 – 163, 2004.
[94] Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, 33 – 44, 2006.
[95] AD Gordon, M Abadi, A Calculus for Cryptographic Protocols: The Spi Calculus, 4th ACM Conference on Computer and Communications Security, 1997.
[96] AD Gordon, Nominal Calculi for Security and Mobility, DARPA Workshop on Foundations for Secure Mobile Code, 1997.
[97] Hennessy M., Riely J., Information flow vs resource access in the asynchronous pi-calculus, ICALP00, LNCS 1853, 415-427, Springer, 2000.
[98] Hennessy M., The security pi-calculus and noninterference, Technical Report 2000:05, University of Susex, 2000.
[99] F.Pottier, A simple view of type-secure information flow in the pi calculus, 320-330, 2002.
[100] Naoki Kobayashi. Type-based information flow analysis for the pi-calculus. Technical Report TR030007, Department of Computer Science, Tokyo Institute of Technology, October 2003.
[101] S.Eilenberg, Automata, Languages and Machines, Vol A. Academic Press, New York, 1974.
[102] L.Lamport, Proving the correctness of multiprocess programs, IEEE Trans. On Software Engineering SE-3, 2, 125-143, 1977.
[103] S. Owicki, L.Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol.4(3), 455 – 495, 1982.
[104] J. P. Queille and J. Sifakis. Speci_cation and veri_cation of concurrent systems in CESAR. In Proc. of the 5th international Symposium on Programming,vol. 137 of LNCS, 1982.
[105] B.Alpern and F.B.Schneider. Defning liveness. Information Processing Letters, 21(4):181-185, 1985.
[106] B.Alpern and F.B.Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117-126, 1987.
[107] H.P. Gumm. Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. Information Processing Letters,47 (6):291-294, 1993.
[108] E. Kindler. Safety and liveness properties: A survey. EATCS-Bulletin, 53:268{272, June 1994.
[109] A. P. Sistla. Safety, Liveness and fairness in temporal logic. Formal aspects of Computing, 6:495-511, 1994.
[110] F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security(TISSEC), 3(1):30-50, 2000.
[111] Ulfar Erlingsson, Schneider, SASI enforcement of security policies: a retrospective, New Security Paradigms Workshop, Proceedings of the 1999 workshop on New security paradigms, 87–95, 1999.
[112] David Walker, A Type System for Expressive Security Policies, Twenty-Seventh ACM SIGPLAN Symposium on Principles of Programming Languages, 254-267, Boston, 2000.
[113] L.Bauer, J.Ligatti and David Walker, Types and Effects for Non-interfering Program Monitors, International Symposium on Software Security, Tokyo,2002. Revised for printing in Software Security-Theory and Systems, LNCS 2609, Springer, pp 154-171. December 2002.
[114] Glynn Winkel, Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk, In BRICS reports series RS-94-1, 1994.
[115] R.Milner, A calculus of communicating systems, Lecture Notes in Computer Science, Vol92, Springer-Verlag, 1980.
[116] R.Milner, Communication and Concurrency, Pretice Hall, 1989.
[117] Hoare C., Communicating Sequential Processes, Prentice Hall, 1985.
[118] T. Thorn. Programming Languages for Mobile Code. ACM Cumpting Surveys, 29(3):213--239, September 1997.
[119] Commission of the European Communities, Information Technology Security Evaluation Criteria(ITSEC), Version 1.2, 1991.
[120] J. A. Goguen and J. Meseguer, Security Policies and Security Models, Proceedings of the 1982 IEEE Symposium on Security and Privacy, Washington D.C., 1982.
[121] R.Focardi, R.Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security , 3(1): 5-33, 1995.
[122] R. Focardi and R. Gorrieri, Non Interference: Past, Present and Future, In Proceedings of 1997 Foundations for Secure Mobile Code Workshop, 33-36, Sponsored by DARPA, 1997.
[123] Riccardo Focardi, Roberto Gorrieri: Classification of Security Properties (Part I: Information Flow). FOSAD 2000: 331-396, 2000.
[124] R. Focardi, R. Gorrieri, and F. Martinelli, Classification of Security Properties (Part II: Network Security), Tutorial Lectures, LNCS 2946, Springer, 2004.
[125] P.T.Wojciechowski, P.Sewell, Nomadic Pict Language and infrastructure design for mobile agent, Agent Systems and Applications, Third International Symposium on Mobile Agents. Proceedings. First International Symposium on, 3-6:2 - 12 ,Oct. 1999.
[126] P.T.Wojciechowski, Nomadic Pict: Language and infrastructure design for mobile Computation, PHD thesis, University of Cambridge, 2000.
[127] J.Riely and M.Hennessy, Trust and partial typing in open systems of mobile agents. Technical Report 4, Computer Science, University of Sussex, 1998.
[128] J.Riely and M.Hennessy, Distributed Processes and Location Failures, Final version appeared in Theoretical Computer Science, 226:693-735, 2001.
[129] Roberto M. Amadio: An Asynchronous Model of Locality, Failurem and Process Mobility, COORDINATION 1997: 374-391, 1997.
[130] A.Francalanza, M.Hennessy, A Study of System Behaviour in the presence of Node and Link Failure, Mikado/Myths Workshop, Sussex, England, June 2003.
[131] A.Francalanza, M.Hennessy, A Theory of System Behaviour in the Presence of Node and Link Failures, LNCS, CONCUR 2005 – Concurrency Theory, Springer Berlin / Heidelberg, 368-382, 2005.
[132] A.Francalanza, A Study of Failure in a Distributed Pi-calculus, PHD Thesis, University of Sussex, 2005.
[133] G.Berry, G.Boudol, The chemical abstract machine, Selected papers of the Second Workshop on Concurrency and compositionality, San Miniato, Italy, 217 – 248, 1992.
[134] 任洪敏,基于 Pi 演算的软件体系结构形式化研究,博士论文,复旦大学,2003。
[135] 廖军 , 谭浩 , 刘锦德,基于 Pi-演算的 Web 服务组合的描述和验证,计算机学报,28(4),635-643,2005。
[136] 廖军 , 谭浩 , 刘锦德,基于 Pi-演算的 Web 服务可替换性验证,华中科技大学学报,33(8),168～171,2005。
[137] D.Sangiorgi. Bisimulation for higher-order process calculi. Information and Computation , 131(2):141-178, 15 December 1996.
[138] B Awerbuch, D Peleg, Online tracking of mobile users, Journal of the ACM, 1995, 42(5):1021-1058.
[139] A. Tanenbaum, M V Steen, Distributed Systems Principles and Paradigms, Prentice Hall Inc., 2002, 57-66.
[140] P. T. Wojciechowski. Nomadic Pict: Language and Infrastucture Design for Mobile Computation, Univeristy of Cambridge, Phd thesis, 2000.
[141] J. Baumann, F. Hohl, M. Straber et al, Mole-Concepts of a mobile agent system, World Wide Web Journal, 1998, 1(3):123-137.
[142] E. Jul, H. Levy, N. Hutchinson et al, Fine-Grained mobility in the emerald system, ACM Transactions on Computer Systems, 1988,6(2):109-133.
[143] A. L. Murphy, G. P. Picco, Reliable communication for highly mobile Agents, Proceedings of the 1st International Symposium on Agent Systems and Applications. New York: IEEE Computer Society, 1999:141-150.
[144] P.C.Kanellakis, S.A.Smolka, CCS expressions, finite state processes and three problems of equivalence, Journal of Information and Computation (86) 43-68, 1990.
[145] M.Hennessy, H.Lin, Symbolic bisimulations, Theoretical Computer Science, (138) 353-389, 1995.