Secrecy for mobile implementations of security protocols

Giambiagi, Pablo (2001) Secrecy for mobile implementations of security protocols. Licentiate thesis, KTH.

Full text not available from this repository.


Mobile code technology offers interesting possibilities to the practitioner, but also raises strong concerns about security. One aspect of security is secrecy, the preservation of confidential information. This thesis investigates the modelling, specification and verification of secrecy in mobile applications, which access and transmit confidential information through a possibly compromised medium (e.g. the Internet). These applications can be expected to communicate secret information using a security protocol, a mechanism to guarantee that the transmitted data does not reach unauthorised entities. The central idea is therefore to relate the secrecy properties of the application to those of the protocol it implements, through the definition of a ``confidential protocol implementation'' relation. The argument takes an indirect form, showing that a confidential implementation transmits secret data only in the ways indicated by the protocol. We define the implementation relation using labelled transition semantics, bisimulations and relabelling functions. To justify its technical definition, we relate this property to a notion of non-interference for non-deterministic systems derived from Cohen's definition of Selective Independence. We also provide simple and local conditions that greatly simplify its verification, and report on our experiments on an architecture showing how the proposed formulations could be used in practice to enforce secrecy of mobile code.

Item Type:Thesis (Licentiate)
Additional Information:, Also published as SICS technical report T2001:19.
ID Code:3111
Deposited On:17 Jun 2008
Last Modified:18 Nov 2009 16:17

Repository Staff Only: item control page