Showing 1–2 of 2 results for author: Rollshausen, N

PairSonic: Helping Groups Securely Exchange Contact Information

Authors: Florentin Putz, Steffen Haesler, Thomas Völkl, Maximilian Gehring, Nils Rollshausen, Matthias Hollick

Abstract: Securely exchanging contact information is essential for establishing trustworthy communication channels that facilitate effective online collaboration. However, current methods are neither user-friendly nor scalable for large groups of users. In response, we introduce PairSonic, a novel group pairing protocol that extends trust from physical encounters to online communication. PairSonic simplifie… ▽ More Securely exchanging contact information is essential for establishing trustworthy communication channels that facilitate effective online collaboration. However, current methods are neither user-friendly nor scalable for large groups of users. In response, we introduce PairSonic, a novel group pairing protocol that extends trust from physical encounters to online communication. PairSonic simplifies the pairing process by automating the tedious verification tasks of previous methods through an acoustic out-of-band channel using smartphones' built-in hardware. Our protocol not only facilitates connecting users for computer-supported collaboration, but also provides a more user-friendly and scalable solution to the authentication ceremonies currently used in end-to-end encrypted messengers like Signal or WhatsApp. PairSonic is available as open-source software: https://github.com/seemoo-lab/pairsonic △ Less

Submitted 20 November, 2024; originally announced November 2024.

Comments: 3 pages, 1 figure, the source code is available at https://github.com/seemoo-lab/pairsonic and a demo video is available at https://www.youtube.com/watch?v=e1AMYDLWN0E and further project information is at https://fputz.net/pairsonic

Journal ref: ACM CSCW 2024

Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects

Authors: Eduard Kamburjan, Marco Scaletta, Nils Rollshausen

Abstract: We present the Crowbar tool, a deductive verification system for the ABS language. ABS models distributed systems with the Active Object concurrency model. Crowbar implements behavioral symbolic execution: each method is symbolically executed, but specification and prior static analyses influence the shape of the symbolic execution tree. User interaction is realized through guided counterexamples,… ▽ More We present the Crowbar tool, a deductive verification system for the ABS language. ABS models distributed systems with the Active Object concurrency model. Crowbar implements behavioral symbolic execution: each method is symbolically executed, but specification and prior static analyses influence the shape of the symbolic execution tree. User interaction is realized through guided counterexamples, which present failed proof branches in terms of the input program. Crowbar has a clear interface to implement new specification languages and verification calculi in the Behavioral Program Logic and has been applied for the biggest verification case study of Active Objects. △ Less

Submitted 11 February, 2022; v1 submitted 19 February, 2021; originally announced February 2021.