Abstracts
- Speaker: Thomas Haines
- Title: Verified Verifiers for Verifiable Elections
- Abstract: Verifiable electronic voting promises to secure elections even in the presence of corrupted devices, malign participants, and compromised or dishonest authorities. The theoretical study of verifiable electronic voting has made significant progress; however, the implementation of these techniques has proven to be an incredible error prone process. This talk will cover the ongoing work to reduce the gap between theory and practice by formally verifying the implementations to satisfy the required cryptographic properties.
- Speaker: Ruba Abu-Salma
- Title: Users Do Not Bite: Exploring the Adoption and Use of Encrypted Communication Tools
- Abstract: Computer security and privacy experts have always advocated the widespread adoption and use of secure communication tools. However, it remains unclear if users understand what protection these tools offer. Unlike prior work, we take a user-centered approach to evaluating the user experience, and improving the design, of secure (mainly end-to-end encrypted) communication tools.
Prior studies have shown poor usability primarily hampers the adoption of secure communication tools. However, we found – by conducting five qualitative (n=102) and two quantitative (n=425) user studies – that, in addition to poor usability, lack of utility and incorrect user mental models of secure communications are primary obstacles to adoption.
Users will not adopt a communication tool that is both usable and secure, but lacks utility (due to, e.g., the tool’s small userbase). Further, most users do not know what it means for a usable and secure tool that is widely-adopted and offers utility (e.g., WhatsApp) to be end-to-end encrypted. Incorrect mental models of encryption lead people to use less secure channels that they incorrectly perceive as more secure than end-to-end encrypted tools.
Thus, we argue the key user-related challenge for secure communications is no longer fostering adoption, but emphasizing appropriate use – by helping people who already use secure tools avoid sending sensitive information over less secure channels. By employing participatory design, we take a user-centered approach to designing effective descriptions that explain the security properties of end-to-end encrypted communications.
- Speaker: Matteo Acclavio
- Title: Logic Beyond Formulas
- Abstract: Logic and proof theory provide methods and tools used in areas such as formal verification and logic programming.
However, the formula-as-process interpretation is not as well investigated as
the formulas-as-property, formula-as-program or formula-as-type interpretations.
In fact, when we model processes as formulas, formulas are not expressive enough:
they can model some processes, e.g. those who admit a series-parallel decomposition, but not the more general cases.
To overcome this limitation and develop new proof-theoretical tools for process analysis,
in this talk I present a proof system based on unoriented graphs instead of formulas.
After proving some basic properties of the system, I show how this system can find applications in process analysis.
- Speaker: Dov Gabbay
- Title: Argumentation-based Semantics for Attack and Defense Trees
- Abstract: This paper connects between the areas and communities of Abstract Argumentation and the Attack and Defense Trees in the area of Security.
Both areas deal with attacks and defense/support and both areas rely on human applications dealing with human aggressive activities.
Our idea is to examine the different points of view of these two communities and come up with new unifying ideas
which can solve existing problems in each area.
- Speaker: James Wright
- Title: On the Use of Queuing Networks to Test the Robustness of Security Protocols
- Abstract: James will be presenting an overview of a probabilistic formal method that he has been developing over the past four years,
based on M/M/c/K queuing networks. The method was developed to fill a gap in assurances
that can be given by symbolic methods about the security of a protocol
when it comes to attacks against robustness. The methodology looks at whether a protocol can guarantee
the availability and synchronisation of state between devices.
James will explain why attacks against robustness require the development of a new class of adversary models
that is distinct from the Dolev-Yao model to be able generate nuanced attacks against robustness,
and how he encapsulated them in his methodology.
He will finally present some of the attacks that he has discovered using his methodology in the IEC61850 substation automation standard.
- Speaker: Georges-Axel Jaloyan
- Title: The ABC of Next-Gen Shellcoding
- Abstract: Shellcodes are short executable stubs that are used in various attack scenarios, whenever code execution is possible. After briefly recalling how they work in general and what interesting things they can do, besides obviously running a reverse-shell, we'll have to deal with the reality that shellcodes are usually not particularly stealthy, due in part to the very suspicious presence of non-printable characters. In a tutorial-like fashion, we'll address increasingly more complex constraints starting from basic alphanumeric shellcodes on x86, up to English looking-text shellcodes, straying into unconventional architectures like ARMv8 or even the new and trendy RISC-V.
- Speaker: Sofía Celi
- Title: The state of secure messaging: the case of OTRv4
- Abstract: OTRv4 is the newest version of the Off-The-Record messaging protocol. As
a Privacy Enhancing Technology and cryptographic work, it is a protocol
where the newest academic research intertwines with real-world
implementations, which can take different forms. This new version asks
us to revisit definitions around deniability (participation, message,
online and offline); forward and post-compromise secrecy; how to best
implement a protocol; and how important security and privacy properties
are to the world.
In this talk, we will examine the key security properties that secure
messaging protocols and applications should have and provide; how they
are implemented; and what challenges lies ahead for the secure messaging
sphere. We will explore how these properties are achieved in OTRv4, in
particular, and why they are needed in today’s world.
- Speaker: Mohamed Bourennane
- Title: Quantum Secure Communication
- Abstract: The banking, financial, and defence sectors crucially depend on communication through channels that cannot be intercepted by unauthorized people. Today, different types of sensitive information are sent within and between companies. All of these users employ cryptography to keep their data secret. Today’s cryptographic protocols rely on RSA or so-called elliptical curves methods. Unfortunately, there is no guarantee that these methods will remain safe in the near future, especially having in mind the potential growth of the computation power. Fortunately, quantum mechanics makes it possible to solve the key transfer problem in a new and proven safe manner. Unlike RSA and similar methods, it is nature’s laws that guarantee the security of quantum cryptography. In this talk, I will introduce and review our research in quantum secure communication and also the worldwide effort in quantum technologies.
- Speaker: Cheng-Te Li
- Title: Learning Sleep Quality from Daily Logs
- Abstract: Precision psychiatry is a new research field that uses advanced data mining over a wide range of neural,
behavioral, psychological, and physiological data sources for classification of mental health conditions.
In this talk, I will present a computational framework for predicting sleep efficiency of insomnia sufferers.
We predict sleep efficiency of individual users with a proposed interpretable LSTM-Attention (LA Block) neural network model.
We also propose a model, Pairwise Learning-based Ranking Generation (PLRG), to rank users with high insomnia potential in the next day.
Our computational framework can be used for other applications that analyze and handle noisy and
incomplete time-series human activity data in the domain of precision psychiatry.
Back to SRM presentations.
Contact
For questions and comments contact
Jun or
Peter
.
