Formal verification of bundle authentication mechanism in OSGi service platform: BAN Logic

Young Gab Kim, Chang Joo Moon, Dong Won Jeong, Doo Kwon Baik

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


Security is critical in a home gateway environment. Robust secure mechanisms must he put in place for protecting information transferred through a central location. In considering characteristics for the home gateway environment, this paper proposes a bundle authentication mechanism. We designed the exchange mechanism for transferring a shared secret key. This transports a service bundle safely in the bootstrapping step, by recognizing and initializing various components. In this paper, we propose a bundle authentication mechanism based on a MAC that uses a shared secret key created in the bootstrapping step. In addition, we verify the safety of the key exchange mechanism and bundle authentication mechanism using BAN Logic. From the verified result, we achieved goals of authentication. That is, the operator can trust the bundle provided by the service provider. The user who uses the service gateway can also express trust and use the bundle provided by the operator.

Original languageEnglish
Pages (from-to)153-173
Number of pages21
JournalInternational Journal of Software Engineering and Knowledge Engineering
Issue number2
Publication statusPublished - 2006 Apr


  • Authentication
  • BAN logic
  • MAC (message authentication code)
  • OSGI

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Computer Graphics and Computer-Aided Design
  • Artificial Intelligence


Dive into the research topics of 'Formal verification of bundle authentication mechanism in OSGi service platform: BAN Logic'. Together they form a unique fingerprint.

Cite this