@TECHREPORT\{IMM2002-01254,
    author       = "H. Riis Nielson and F. Nielson and M. Buchholtz",
    title        = "Security for Mobility",
    year         = "2002",
    keywords     = "Security, Mobility, Flow Logic, Mobile Ambients",
    number       = "",
    series       = "",
    institution  = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/1254-full.html",
    abstract     = "We show how to use static analysis to provide information about security issues related to mobility. First the syntax and semantics of Mobile Ambients is reviewed and we show how to obtain a so-called {0CFA} analysis that can be implemented in polynomial time. Next we consider discretionary access control where we devise Discretionary Ambients, based on Safe Ambients, and we adapt the semantics and {0CFA} analysis; to strengthen the analysis we incorporate context-sensitivity to obtain a {1CFA} analysis. This paves the way for dealing with mandatory access control where we express both a Bell-LaPadula model for confidentiality as well as a Biba model for integrity. Finally, we use Boxed Ambients as a means for expressing cryptographic key exchange protocols and we adapt the operational semantics and the {0CFA} analysis.",
    isbn_issn    = "IMM-TR-2002-20"
}