×

Security of multi-agent systems: a case study on comparison shopping. (English) Zbl 1122.68092

Summary: The multi-agent-systems paradigm is becoming more and more popular as a basis for realizing net-based solutions. This development is accompanied by an increasing relevance of security issues. For instance, the potential loss of privacy and other assets is a major concern for, both merchants and customers, in Internet-based commerce and, without being properly addressed, such very legitimate concerns hamper the growth of e-commerce.
This article uses a comparison-shopping scenario to introduce a general methodology for formally verifying the security of multi-agent systems. Following the approach of possibilistic information flow security, the flow of information between and within agents is restricted in order to ensure that secrets will not be disclosed to unauthorized meddlers. The security requirements for the overall system are then decomposed into requirements for the individual agents that can be verified independently from each other. Exploiting the modular structure of a multi-agent system considerably reduces the complexity of the overall security analysis. The techniques for decomposing security requirements, for verifying individual agents, and for deriving global security guarantees for the entire system from locally verified properties are all generic in the sense that they apply also to many other systems and security requirements than the ones that appear in the example scenario.

MSC:

68T01 General topics in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Autexier, S.; Hutter, D.; Langenstein, B.; Mantel, H.; Rock, G.; Schairer, A.; Stephan, W.; Vogt, R.; Wolpers, A., VSE: formal methods meet industrial needs, Internat. J. Software Tools Technol. Transfer, 3, 1, 66-77 (2000), (special issue on Mechanized Theorem Proving for Technology Transfer of the STTT) · Zbl 1060.68673
[2] Bundy, A.; Basin, D.; Hutter, D.; Ireland, A., Rippling: Meta-level Guidance for Mathematical Reasoning (2005), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1095.68108
[3] Blackwell, R. D.; Minard, P. W.; Engel, J. F., Consumer Behaviour (2002), Thomson Learning
[4] A. Bossi, D. Macedonio, C. Piazza, S. Rossi, Secure contexts for confidential data, in: Proceedings of the IEEE Computer Security Foundations Workshop, 2003, pp. 14-25; A. Bossi, D. Macedonio, C. Piazza, S. Rossi, Secure contexts for confidential data, in: Proceedings of the IEEE Computer Security Foundations Workshop, 2003, pp. 14-25
[5] Engel, J. F.; Kollat, D. T.; Blackwell, R. D., Consumer Behavior (1968), Holt, Rinehart & Winston: Holt, Rinehart & Winston New York
[6] Focardi, R.; Gorrieri, R., A classification of security properties for process algebras, J. Computer Security, 3, 1, 5-33 (1995)
[7] W.M. Farmer, J.D. Guttman, V. Swarup, Security for mobile agents: Authentication and state appraisal, in: Proceedings of the 4th European Symposium on Research in Computer Security, Rome, Italy, 1996, pp. 118-130; W.M. Farmer, J.D. Guttman, V. Swarup, Security for mobile agents: Authentication and state appraisal, in: Proceedings of the 4th European Symposium on Research in Computer Security, Rome, Italy, 1996, pp. 118-130
[8] J.A. Goguen, J. Meseguer, Security policies and security models, in: IEEE Symposium on Security and Privacy, 1982, pp. 11-20; J.A. Goguen, J. Meseguer, Security policies and security models, in: IEEE Symposium on Security and Privacy, 1982, pp. 11-20
[9] J.A. Goguen, J. Meseguer, Inference control and unwinding, in: IEEE Symposium on Security and Privacy, 1984, pp. 75-86; J.A. Goguen, J. Meseguer, Inference control and unwinding, in: IEEE Symposium on Security and Privacy, 1984, pp. 75-86
[10] J.D. Guttman, M.E. Nadel, What needs securing? in: Proceedings of the IEEE Computer Security Foundations Workshop, 1988, pp. 34-57; J.D. Guttman, M.E. Nadel, What needs securing? in: Proceedings of the IEEE Computer Security Foundations Workshop, 1988, pp. 34-57
[11] J. Halpern, K. O’Neill, Secrecy in multiagent systems, in: Proceedings of the 15th IEEE Computer Security Foundations Workshop, 2002; J. Halpern, K. O’Neill, Secrecy in multiagent systems, in: Proceedings of the 15th IEEE Computer Security Foundations Workshop, 2002
[12] J. Halpern, K. O’Neill, Anonymity and information hiding in multiagent systems, in: Proc. of 16th IEEE Computer Security Foundations Workshop, 2003; J. Halpern, K. O’Neill, Anonymity and information hiding in multiagent systems, in: Proc. of 16th IEEE Computer Security Foundations Workshop, 2003
[13] Hoare, C. A.R., Communicating Sequential Processes, International Series in Computer Science (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[14] F. Hohl, An approach to solve the problem of malicious hosts, Technical Report 1997/03, Universität Stuttgart, Germany, 1997; F. Hohl, An approach to solve the problem of malicious hosts, Technical Report 1997/03, Universität Stuttgart, Germany, 1997
[15] Howard, J. A.; Sheth, J. N., The Theory of Buying Behavior (1969), John Wiley & Sons: John Wiley & Sons New York
[16] Hutter, D.; Schairer, A., Possibilistic information flow control in the presence of encrypted communication, (Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS 2004). Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS 2004), Lecture Notes in Computer Science, vol. 3193 (2004), Springer: Springer Berlin), 209-224 · Zbl 1487.68066
[17] Hutter, D., Deductive verification of invariants of state-transition systems, (Herzog, O.; Günter, A., KI-98: Advances in Artificial Intelligence. KI-98: Advances in Artificial Intelligence, Lecture Notes in Artificial Intelligence, vol. 1504 (1998), Springer: Springer Berlin)
[18] H. Mantel, Possibilistic definitions of security—an assembly kit, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, Cambridge, UK, 2000, pp. 185-199; H. Mantel, Possibilistic definitions of security—an assembly kit, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, Cambridge, UK, 2000, pp. 185-199
[19] Mantel, H., Unwinding possibilistic security properties, (European Symposium on Research in Computer Security (ESORICS). European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, vol. 1895 (2000), Springer: Springer Berlin), 238-254 · Zbl 1487.68071
[20] Mantel, H., Information flow control and applications—bridging a gap, (Proceedings of FME 2001: Formal Methods for Increasing Software Productivity. Proceedings of FME 2001: Formal Methods for Increasing Software Productivity, Lecture Notes in Computer Science, vol. 2021 (2001), Springer: Springer Berlin), 153-172 · Zbl 0977.68681
[21] Mantel, H., On the composition of secure systems, (Proceedings of the IEEE Symposium on Security and Privacy. Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA (2002), IEEE Computer Society), 88-101
[22] H. Mantel, A uniform framework for the formal specification and verification of information flow security, PhD thesis, Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät I, 2003; H. Mantel, A uniform framework for the formal specification and verification of information flow security, PhD thesis, Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät I, 2003
[23] D. McCullough, Specifications for multi-level security and a hook-up property, in: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 1987, pp. 161-166; D. McCullough, Specifications for multi-level security and a hook-up property, in: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 1987, pp. 161-166
[24] J.D. McLean, A general theory of composition for trace sets closed under selective interleaving functions, in: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1994, pp. 79-93; J.D. McLean, A general theory of composition for trace sets closed under selective interleaving functions, in: Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1994, pp. 79-93
[25] McLean, J. D., A general theory of composition for a class of “possibilistic” security properties, IEEE Trans. Software Engrg., 22, 1, 53-67 (1996)
[26] C. Meadows, Detecting attacks on mobile agents, in: Proceedings of the 1997 Foundations for Secure Mobile Code Workshop, Monterey, CA, March 1997, pp. 64-65; C. Meadows, Detecting attacks on mobile agents, in: Proceedings of the 1997 Foundations for Secure Mobile Code Workshop, Monterey, CA, March 1997, pp. 64-65
[27] Milner, R., Communication and Concurrency, International Series in Computer Science (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[28] J.T. Moore, Mobile code security techniques, Technical Report MS-CIS-98-28, University of Pennsylvania, 1998; J.T. Moore, Mobile code security techniques, Technical Report MS-CIS-98-28, University of Pennsylvania, 1998
[29] H. Mantel, A. Sabelfeld, A generic approach to the security of multi-threaded programs, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, 2001, pp. 126-142; H. Mantel, A. Sabelfeld, A generic approach to the security of multi-threaded programs, in: Proceedings of the 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, 2001, pp. 126-142
[30] Mantel, H.; Schairer, A., Exploiting generic aspects of security models in formal developments, (Hutter, D.; Stephan, W., Festschrift in Honor of Jörg Siekmann. Festschrift in Honor of Jörg Siekmann, Lecture Notes in Computer Science, vol. 2605 (2005), Springer: Springer Berlin), 452-475 · Zbl 1098.68588
[31] G.C. Necula, Proof-carrying code, in: Conference Record of POPL ’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 106-119; G.C. Necula, Proof-carrying code, in: Conference Record of POPL ’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 1997, pp. 106-119
[32] Nicosia, F. M., Consumer Decision Processes (1966), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[33] C. O’Halloran, A calculus of information flow, in: Proceedings of the European Symposium on Research in Computer Security (ESORICS), Toulouse, France, 1990, pp. 147-159; C. O’Halloran, A calculus of information flow, in: Proceedings of the European Symposium on Research in Computer Security (ESORICS), Toulouse, France, 1990, pp. 147-159
[34] P.Y.A. Ryan, S.A. Schneider, Process algebra and non-interference, in: Proceedings of the 12th IEEE Computer Security Foundations Workshop, Mordano, Italy, 1999, pp. 214-227; P.Y.A. Ryan, S.A. Schneider, Process algebra and non-interference, in: Proceedings of the 12th IEEE Computer Security Foundations Workshop, Mordano, Italy, 1999, pp. 214-227
[35] J.M. Rushby, Noninterference, transitivity, and channel-control security policies, Technical Report CSL-92-02, SRI International, 1992; J.M. Rushby, Noninterference, transitivity, and channel-control security policies, Technical Report CSL-92-02, SRI International, 1992
[36] Subrahmanian, V. S.; Bonatti, P.; Dix, J.; Eiter, T.; Kraus, S.; Özcan, F.; Ross, R., Secure agent programs, (Heterogeneous Agent Systems (2000), MIT Press: MIT Press Cambridge, MA), (Chapter 10)
[37] I. Schaefer, Secure mobile multiagent systems on electronic marketplaces—a case study on comparison shopping, Technical Report RR-02-02, DFKI GmbH, 2002; I. Schaefer, Secure mobile multiagent systems on electronic marketplaces—a case study on comparison shopping, Technical Report RR-02-02, DFKI GmbH, 2002
[38] Schairer, A., Towards using possibilistic information flow control to design secure multiagent systems, (Hutter, D.; Müller, G.; Stephan, W.; Ullmann, M., Proceedings of the First International Conference on Security in Pervasive Computing. Proceedings of the First International Conference on Security in Pervasive Computing, Lecture Notes in Computer Science, vol. 2802 (2003), Springer: Springer Berlin)
[39] I. Schaefer, Information flow control for multiagent systems—a case study on comparison shopping, Technical Report RR-04-01, DFKI GmbH, 2004; I. Schaefer, Information flow control for multiagent systems—a case study on comparison shopping, Technical Report RR-04-01, DFKI GmbH, 2004
[40] Schairer, A.; Hutter, D., Proof transformations for evolutionary formal software development, (Proceedings 9th International Conference on Algebraic Methodology And Software Technology, AMAST2002. Proceedings 9th International Conference on Algebraic Methodology And Software Technology, AMAST2002, Lecture Notes in Computer Science, vol. 2422 (2002), Springer: Springer Berlin) · Zbl 1275.68059
[41] Sander, T.; Tschudin, C., Towards mobile cryptography, (Proceedings of the IEEE Symposium on Security and Privacy. Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA (1998), IEEE Computer Society Press)
[42] D. Sutherland, A model of information, in: Proceedings of the 9th National Computer Security Conference, 1986; D. Sutherland, A model of information, in: Proceedings of the 9th National Computer Security Conference, 1986
[43] The Agent Oriented Software Group, JACK Development Environment (JDE) (2004)
[44] Vigna, G., Cryptographic traces for mobile agents, (Vigna, G., Mobile Agents and Security (1998), Springer: Springer Heidelberg), 137-153
[45] Oheimb, D. V., Information flow control revisited: noninfluence=noninterference+nonleakage, (Proceedings of the European Symposium on Research in Computer Security (ESORICS). Proceedings of the European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, vol. 3193 (2004), Springer: Springer Berlin), 225-243
[46] B.S. Yee, A sanctuary for mobile agents, in: Proceedings of the DARPA Workshop on Foundations for Secure Mobile Code, Monterey, USA, March 1997; B.S. Yee, A sanctuary for mobile agents, in: Proceedings of the DARPA Workshop on Foundations for Secure Mobile Code, Monterey, USA, March 1997
[47] A. Zakinthinos, E.S. Lee, A general theory of security properties, in: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 1997, pp. 94-102; A. Zakinthinos, E.S. Lee, A general theory of security properties, in: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, 1997, pp. 94-102
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.