Journal of Computer Security - Volume 18, issue 2

Authors: Jajodia, Sushil | Millen, Jon

Article Type: Editorial

DOI: 10.3233/JCS-2010-0402

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 187-187, 2010

Authors: Gorla, Daniele | Palamidessi, Catuscia

Article Type: Editorial

DOI: 10.3233/JCS-2010-0359

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 189-189, 2010

Authors: Malacaria, Pasquale

Article Type: Research Article

Abstract: There is a clear intuitive connection between the notion of leakage of information in a program and concepts from Information Theory. We explore this connection by interpreting Information Theory as a security risk assessment of programs. Information Theory will then be used to introduce techniques to reason on looping constructs, which are the kind of programs that previous quantitative models failed to satisfactory address. The semantics here introduced allows to describe both the amount and rate of leakage; if either is small enough, then a program might be deemed “secure”. Using the semantics we provide an investigation and classification of …bounded and unbounded covert channels. Show more

Keywords: Quantitative Information Flow, Information Theory, language based security

DOI: 10.3233/JCS-2010-0360

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 191-228, 2010

Authors: Bodei, Chiara | Brodo, Linda | Degano, Pierpaolo | Gao, Han

Article Type: Research Article

Abstract: A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LYSA calculus to cope with types, by using tags to represent the intended types of terms. We develop a Control Flow Analysis for this calculus which soundly over-approximates all the possible behaviour of a protocol and, in particular, is able to capture any type confusion that may occur during the protocol execution. The analysis acts …in a descriptive way: it describes which violations may occur. In the same setting, our approach also offers a prescriptive usage: we can impose a type discipline, by forcing some data to be of the expected types. At this point, the analysis may statically check that type violations are not possible any longer. In other words, we instrument the code with the only checks necessary to enforce type security. Finally, we apply our framework to a multi-protocol setting, where the risk of having type flaw attacks is higher. Our analysis has been implemented and successfully applied to a number of security protocols, showing it is able to capture type flaw attacks. The implementation complexity of the analysis is low polynomial. Show more

Keywords: Security of cryptographic protocols, Control Flow Analysis, type flaw attacks

DOI: 10.3233/JCS-2010-0361

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 229-264, 2010

Authors: Hamadou, Sardaouna | Mullins, John

Article Type: Research Article

Abstract: It is customary to view the scheduler as an intruder when modelling security protocols by means of process calculi that express both nondeterministic and probabilistic behavior. It has been established that traditional schedulers need to be carefully calibrated in order to more accurately reflect an intruder's real power. We propose such a class of schedulers through a variant of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. (Theoretical Computer Science 353 (2006), 118–164) called PPCνσ . We define two levels of schedulers: adversarial schedulers which schedule a class of indistinguishable actions i.e. actions that we do not want …an attacker to distinguish, and internal schedulers, called task schedulers, which resolve the remaining nondeterminism within a chosen class. We also show how to apply them in order to design schedulers for the analysis of cryptographic protocols that accurately reflect an intruder's capacity for controlling communication networks, without allowing it to control the internal reactions of the protocol under attack. We give a new characterization of the asymptotic observational equivalence of Mitchell et al. (Theoretical Computer Science 353 (2006), 118–164) that is more suited for taking into account any observable trace rather than just one single action. This asymptotic observational equivalence is a congruence in accordance with these new schedulers. We illustrate the aptness of our approach by an extensive study of the Dining Cryptographers (DCP) (J. Cryptology 1 (1988), 65–75) protocol. Show more

Keywords: Process algebra, observational equivalence, probabilistic scheduling, analysis of cryptographic protocols

DOI: 10.3233/JCS-2010-0362

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 265-316, 2010

Authors: Delaune, Stéphanie | Kremer, Steve | Ryan, Mark D.

Article Type: Research Article

Abstract: We propose a symbolic semantics for the finite applied pi calculus. The applied pi calculus is a variant of the pi calculus with extensions for modelling cryptographic protocols. By treating inputs symbolically, our semantics avoids potentially infinite branching of execution trees due to inputs from the environment. Correctness is maintained by associating with each process a set of constraints on terms. We define a symbolic labelled bisimulation relation, which is shown to be sound but not complete with respect to standard bisimulation. We explore the lack of completeness and demonstrate that the symbolic bisimulation relation is sufficient for many practical …examples. This work is an important step towards automation of observational equivalence for the finite applied pi calculus, e.g. for verification of anonymity or strong secrecy properties. Show more

Keywords: Applied pi calculus, observational equivalence, security protocols

DOI: 10.3233/JCS-2010-0363

Citation: Journal of Computer Security, vol. 18, no. 2, pp. 317-377, 2010