Authors: Bugliesi, Michele | Rossi, Sabina
Article Type: Research Article
Abstract: Non-interference has been advocated by various authors as a uniform framework for the formal specification of security properties in cryptographic protocols. Unfortunately, specifications based on non-interference are often non-effective, as they require protocol analyses in the presence of all possible intruders. This paper develops new characterizations of non-interference that rely on a finitary representation of intruders. These characterizations draw on equivalence relations built on top of labelled transition systems in which the presence of intruders is accounted for, indirectly, in terms of their (the intruders') knowledge of the protocols' initial data. The new characterizations apply uniformly to trace and bisimulation …non-interference, yielding proof techniques for the analysis of various security properties. We demonstrate the effectiveness of such techniques in the analysis of different properties of a fair exchange protocol. Show more
Keywords: Process calculi, concurrency, behavioral equivalences, security
DOI: 10.3233/JCS-2005-13104
Citation: Journal of Computer Security, vol. 13, no. 1, pp. 87-113, 2005
Authors: Calzavara, Stefano | Rabitti, Alvise | Bugliesi, Michele
Article Type: Research Article
Abstract: Since cookies act as the only proof of a user identity, web sessions are particularly vulnerable to session hijacking attacks, where the browser run by a given user sends requests associated to the identity of another user. When n > 1 cookies are used to implement a session, there might actually be n sub-sessions running at the same website, where each cookie is used to retrieve part of the state information related to the session. Sub-session hijacking breaks the ideal view of the existence of a unique user session by selectively hijacking m sub-sessions, with m < n . This …may reduce the security of the session to the security of its weakest sub-session. In this paper, we take a systematic look at the root causes of sub-session hijacking attacks and we introduce sub-session linking as a possible defense mechanism. Out of two flavors of sub-session linking desirable for security, which we call intra-scope and inter-scope sub-session linking respectively, only the former is relatively smooth to implement. Luckily, we also identify programming practices to void the need for inter-scope sub-session linking. We finally present Warden, a server-side proxy which automatically enforces intra-scope sub-session linking on incoming HTTP(S) requests, and we evaluate it in terms of protection, performances, backward compatibility and ease of deployment. Show more
Keywords: Web application security, web sessions, HTTP cookies
DOI: 10.3233/JCS-181149
Citation: Journal of Computer Security, vol. 27, no. 2, pp. 233-257, 2019
Authors: Bugliesi, Michele | Focardi, Riccardo | Maffei, Matteo
Article Type: Research Article
Abstract: We propose a type and effect system for authentication protocols built upon a tagging scheme that formalizes the intended semantics of ciphertexts. The main result is that the validation of each component in isolation is provably sound and fully compositional: if all the protocol participants are independently validated, then the protocol as a whole guarantees authentication in the presence of Dolev–Yao intruders possibly sharing long term keys with honest principals. Protocols are thus validated in the presence of both malicious outsiders and compromised insiders. The highly compositional nature of the analysis makes it suitable for multi-protocol systems, where different protocols …might be executed concurrently. Show more
DOI: 10.3233/JCS-2007-15602
Citation: Journal of Computer Security, vol. 15, no. 6, pp. 563-617, 2007
Authors: Bugliesi, Michele | Calzavara, Stefano | Focardi, Riccardo | Khan, Wilayat
Article Type: Research Article
Abstract: Session cookies constitute one of the main attack targets against client authentication on the Web. To counter these attacks, modern web browsers implement native cookie protection mechanisms based on the HttpOnly and Secure flags. While there is a general understanding about the effectiveness of these defenses, no formal result has so far been proved about the security guarantees they convey. With the present paper we provide the first such result, by presenting a mechanized proof of noninterference assessing the robustness of the HttpOnly and Secure cookie flags against both web and network attackers with the ability to perform arbitrary XSS …code injection. We then develop CookiExt , a browser extension that provides client-side protection against session hijacking, based on appropriate flagging of session cookies and automatic redirection over HTTPS for HTTP requests carrying these cookies. Our solution improves over existing client-side defenses by combining protection against both web and network attacks, while at the same time being designed so as to minimise its effects on the user’s browsing experience. Finally, we report on the experiments we carried out to practically evaluate the effectiveness of our approach. Show more
Keywords: Browser security, session cookies, formal methods, noninterference
DOI: 10.3233/JCS-150529
Citation: Journal of Computer Security, vol. 23, no. 4, pp. 509-537, 2015
Authors: Bono, Viviana | Bugliesi, Michele | Dezani-Ciancaglini, Mariangiola | Liquori, Luigi
Article Type: Research Article
Abstract: We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the use of subtype-bounded quantification to capture a new and more direct rendering of MyType polymorphism, and a uniform treatment for other features that were accounted for via different systems in subsequent extensions [7, 6] of [16]. The new system provides for (i) appropriate type specialization of inherited methods, (ii) static detection of errors, (iii) width subtyping compatible with object extension, and (iv) sound typing for partially specified objects.
Keywords: Objects, Type System, Subtyping, Type Soundness
DOI: 10.3233/FI-1999-38401
Citation: Fundamenta Informaticae, vol. 38, no. 4, pp. 325-364, 1999