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

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.