Tag Archives: Security and Privacy

20/11/2013 – Talk by Wilayat Khan

Title:  Automatic and Robust Client-Side Protection for Cookie-Based Sessions
Time: 11:00
Location: Meeting room
Type: Research Result
Speaker: Wilayat Khan
Abstract:
Abstract: Session cookies constitute one of the primary attack targets
against client authentication on the Web, hence modern web browsers
implement native protection mechanisms for them based on the Secure
and HttpOnly flags. While there is a general understanding about the
effectiveness of these defences, no formal result has so far proved about
the security guarantees they convey.

In this work, we have provided the first such result, with a mechanized
proof of non-interference assessing the robustness of the Secure and
HttpOnly cookie flags against both web and network attacks. We have
mechanized the proofs using the interactive theorem prover Coq.
Furthermore, we have developed 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 such cookies. Our solution improves
over existing client-side defences 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.

22.03.2013 – Talk by Pedro Adão

Title: Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Pedro Adão
Abstract:

We show that the recent technique of computationally complete symbolic attackers  proposed by Bana and Comon-Lundh for computationally sound verification of security protocols is powerful enough to verify actual protocols.  In their work,  Bana and Comon-Lundh presented only the general framework, but they did not introduce sufficiently many axioms to actually prove protocols.We present a  set of  axioms—some generic axioms that are computationally sound for all PPT  algorithms, and two specific axioms that are sound for CCA2 secure encryptions—and illustrate the power of this technique by giving the first computationally sound  verification (secrecy and authentication) via symbolic attackers of the  NSL Protocol  that does not need any further restrictive assumptions about the  computational implementation. These axioms are entirely modular, and not particular to the NSL protocol hence can be reused in the proofs of security for many other security protocols.Joint work with Gergei Bana and Hideki Sakurada

Open postdoc fellowship

We are seeking to recruit a post-doc fellow to conduct integrative theoretical and experimental research in modelling principles and analysis techniques for distributed and pervasive systems.

Requirements: Applicants must hold a Ph.D degree in Computer Science or related subject before the application deadline. The successful candidate will submit a scientifically excellent research proposal,  relevant to the topics of the call, and display:

  • Scientific knowledge across the relevant subjects,
  • Technical competence and a strong publication record,
  • Team working skills,
  • Leadership experience,
  • Ability to organize her/him self and others.

Funding: is for one year, renewable, at approximately 24,000 Euro gross, including mobility allowances (that corresponds to around 21,000 Euro net). The fellowship is expected to start in May / June 2013

See this page for full detalis.