53 results

  • Anonymous Server-Aided Verification

    • March 30, 2018

    • Inria Center of the University of Rennes - -Petri/Turing room

    Speaker : par Elena Pagnin (Chalmers University of Technology, Sweden)

    Server-Aided Verification (SAV) is a method that can be employed to speed up the process of verifying signatures by letting the verifier outsource part of its computation load to a third party. Achieving fast and reliable verification under the presence of an untrusted server is an attractive goal in cloud computing and internet of things scenarios.In this talk I will describe a simple and[…]
  • Automated verification of privacy-type properties for security protocols

    • March 16, 2018

    • Inria Center of the University of Rennes - -Petri/Turing room

    Speaker : Ivan Gazeau (LORIA, Inria Nancy)

    The applied pi-calculus is a powerful framework to model protocols and to define security properties. In this symbolic model, it is possible to verify automatically complex security properties such as strong secrecy, anonymity and unlinkability properties which are based on equivalence of processes.In this talk, we will see an overview of a verification method used by a tool, Akiss. The tool is[…]
  • The Internet of Backdoors

    • March 07, 2018

    • Inria Center of the University of Rennes - -Petri/Turing room

    Speaker : par Sam L. Thomas (University of Birmingham, UK)

    Complex embedded devices are becoming ever prevalent in our everyday lives, yet only a tiny amount of people consider the potential security and privacy implications of attaching such devices to our home, business and government networks. As demonstrated through recent publications from academia and blog posts from numerous industry figures, these devices are plagued by poor design choices[…]
  • When Good Components Go Bad: Formally Secure CompilationDespite Dynamic Compromise

    • February 05, 2018

    • Inria Center of the University of Rennes - -Petri/Turing room

    Speaker : Catalin Hritcu (Inria Paris)

    We propose a new formal criterion for secure compilation, providing strong end-to-end security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others until it becomes[…]
  • Breaking and fixing HB+DB: A Short Tale of Provable vs Experimental Security and Lightweight Designs

    • February 02, 2018

    • Inria Center of the University of Rennes - -Petri/Turing room

    Speaker : Ioana Boureanu (University of Surrey)

    HB+ is a well-know authentication scheme purposely designed to be lightweight. However, HB+ is vulnerable to a key-recovery, man-in-the-middle (MiM) attack dubbed GRS. To this end, at WiSec2015, the HB+DB protocol added a distance-bounding dimension to HB+, which was experimentally shown to counteract the GRS attack.In this talk, we will exhibit however a number of security flaws in the HB+DB[…]