Language-based and process calculi-based information security are well developed fields of computer security. Although these fields have much in common, it is somewhat surprising that the literature lacks a comprehensive account of a formal link between the two disciplines. This paper develops such a link between a language-based specification of security and a process-algebraic framework for security properties. Encoding imperative programs into a CCS-like process calculus, we show that timing-sensitive security for these programs exactly corresponds to the well understood process-algebraic security property of persistent bisimulation-based nondeducibility on compositions (P_BNDC). This rigorous connection opens up possibilities for cross-fertilization, leading to both flexible policies when specifying the security of heterogeneous systems and to a synergy of techniques for enforcing security specifications.
|Data di pubblicazione:||2005|
|Titolo:||Bridging Language-Based and Process Calculi Security|
|Titolo del libro:||Foundations of Software Science and Computational Structures|
|Appare nelle tipologie:||4.1 Articolo in Atti di convegno|
File in questo prodotto:
|fossacs05-079.pdf||Documento in Pre-print||Accesso chiuso-personale||Riservato|