International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News

Here you can see all recent updates to the IACR webpage. These updates are also available:

email icon
via email
RSS symbol icon
via RSS feed

14 December 2022

SnT, University of Luxembourg
Job Posting Job Posting
We are hiring Ph.D. holders in applied cryptography, information security, privacy and blockchains. The successful candidate will join the CryptoLux team led by Prof. Alex Biryukov. He or she will contribute to a research project "Advanced Cryptography for Finance and Privacy (CryptoFin)", which is funded by FNR. The project is in collaboration with Stanford University and Ethereum Foundation's cryptography teams. Candidates with research interests in one or more of the following areas are welcome to apply:
  • applied or symmetric cryptography
  • cryptofinance, cryptoeconomics, blockchains
  • anonymity and privacy on the Internet
Role The main responsibility of the successful candidate would be to:
  • Conduct, publish and present research results at conferences
  • Provide guidance to the two Ph.D. students of the project
  • Attract funding in cooperation with academic and industrial partners
Your Profile
  • A Ph.D. degree in Computer Science, Applied Mathematics or a related field
  • Competitive research record in applied cryptography or information security (at least one paper in top 10 IT security/crypto conferences)
  • Strong mathematical and algorithmic CS background, economics/finance - a plus
  • Good skills in programming and scripting languages
  • Fluent written/verbal communication skills in English
We offer a 1+2-year contract, highly competitive salaries and is an equal opportunity employer.

Application Applications, written in English, should be submitted online and should include:

  • A brief cover letter explaining the candidate's motivation and research interests
  • Curriculum Vitae (including photo, education/research/work, publications, interests, contributions to open-source projects, participation in research competitions, olympiads, CTFs, etc.)
  • Contact information of 3 referees
Deadline for applications: January 15, 2023. Applications will be considered on receipt therefore applying before the deadline is encouraged.

Closing date for applications:

Contact: Prof. Alex Biryukov (e-mail: first name dot family name (at) uni.lu)

More information: https://www.cryptolux.org/index.php/Vacancies

Expand
Queen's University Belfast
Job Posting Job Posting
The School of Electronics, Electrical Engineering & Computer Science (EEECS) at Queen’s University Belfast, is currently seeking to appoint an exceptional candidate to the post of Research Fellow. The successful candidate will conduct research into intrinsic physical unclonable function (PUF) designs for resource-constrained devices, such as approximate computing-based applications. This research is an EPSRC New Investigator Award funded project to develop secure intrinsic PUF designs on a RISC-V platform. The post holder will be based at the Centre of Secure Information Technology (CSIT) at the Institute of Electronics, Communication and Information Technologies (ECIT), Queen’s University Belfast. The post is a critical role, and as such, successful applicants will have responsibilities in independent research, supervision, planning, collaborations, and outreach.

The successful candidate must have, and your application should clearly demonstrate you have:

  • A 2:1 Honours degree in Electrical and Electronic Engineering/Computer Science/Mathematics (or related discipline).
  • Obtained, or be about to obtain, a PhD in a relevant subject.
  • At least 3 years’ relevant research experience in hardware security, embedded systems design, hardware design and/or hardware/software co-design.
  • Evidence of a strong publication record commensurate with career stage and experience.

    Duration: This is a fixed term contact for 30 months, or available until 30/09/2025, whichever is sooner. Fixed term contract posts are available for the stated period in the first instance but in particular circumstances may be renewed or made permanent subject to availability of funding.

    Application Deadline: 9 Jan 2023

    Application details: https://www.jobs.ac.uk/job/CVV449/research-fellow-in-hardware-security

    Closing date for applications:

    Contact: Dr. Chongyan Gu (c.gu@qub.ac.uk)

    More information: https://www.jobs.ac.uk/job/CVV449/research-fellow-in-hardware-security

  • Expand
    University of Central Florida
    Job Posting Job Posting
    The Department of Computer Science (CS) and the Department of Mathematics (Math) at the University of Central Florida (UCF) are seeking three full-time, 9-month faculty positions at the rank of assistant professor (tenure-earning), associate professor or professor (tenured) in the area of cyber security and privacy, with concentrations in one of the areas described below. The anticipated start date is August 8, 2023. • Area A (Math): Cryptography, applied cryptography, and intersection of algorithm and cryptography (e.g., quantum cryptography, post-quantum crypto, etc.). One faculty position is anticipated for this area. • Area B (Computer Science): Cloud, Edge, and IoT security (e.g., serverless computing, container security, etc.), system software, software supply chain security, and the security of Cyber Physical System, etc. Two faculty positions are anticipated for this area. These positions will be expected to strengthen both the tenure home department (Math or CS, as applicable), as well as the Cyber Security and Privacy Cluster and may include a combination of secondary joint appointments. The ideal candidates will be in the rank of assistant professor, but exceptional candidates at the rank of associate professor or professor will be considered. The ideal candidates will have a strong background in the areas listed.

    Closing date for applications:

    Contact: Questions regarding this search may be directed to Dr. Yan Solihin (yan.solihin@ucf.edu) or Dr. Paul Gazzillo (paul.gazzillo@ucf.edu).

    More information: https://ucf.wd1.myworkdayjobs.com/careers/job/Orlando-FL-Main-Campus/Assistant-Professor--Associate-Professor--or-Professor--Cyber-Security-and-Privacy-Areas--Computer-Science-or-Mathematics-_R103069

    Expand
    Helsinki Institute for Information Technology, Helsinki, Finland
    Job Posting Job Posting

    The Helsinki Institute for Information Technology (HIIT) invites applications for Postdoctoral Fellows and Research Fellows. HIIT offers a HIIT Postdoctoral Fellow position up to three years. For more senior candidates, HIIT offers a HIIT Research Fellow position up to five years. The length of the contract as well as the starting and ending dates are negotiable.

    All excellent researchers in any area of ICT can be considered, but priority is given to candidates who support one (or more) of the HIIT strategic focus areas:

    • Artificial Intelligence
    • Computational Health
    • Cybersecurity
    • Data Science
    • Foundations of Computing

    The deadline for applications is January 8th, 2023 at 11:59 PM (23:59 UTC+02:00). By applying to this call, organized by Helsinki Institute for Information Technology HIIT, you use one application to apply to positions for both of our hosting institutions, Aalto University and the University of Helsinki. Aalto University and the University of Helsinki are the two leading universities in Finland in computer science and information technology. Both are located in the Helsinki Metropolitan area, and the employing university will be determined by the supervising professor. Aalto University and the University of Helsinki are both committed to fostering an inclusive environment with people from diverse backgrounds, and researchers from underrepresented groups are particularly encouraged to apply.

    Closing date for applications:

    Contact:

    For any question regarding the electronic application system, please contact Maaria Ilanko (firstname.lastname@aalto.fi)

    For questions regarding these positions, please contact the HIIT coordinator at coordinator@hiit.fi

    More information: https://www.hiit.fi/hiit-postdoctoral-and-research-fellow-positions/

    Expand
    Fortanix
    Job Posting Job Posting

    Fortanix is hiring a Sr. Software Engineer, Cryptography. Join a passionate team that will highly appreciate your contributions.

    You will
    • Implement and maintain production-ready cryptography code in Rust and C/C++, including post-quantum algorithms and secure cryptography APIs.
    • Analyze state-of-the-art attacks and implement side-channel mitigations.
    • Participate in peer code review, educate.
    • Help deploy, monitor, and tune the performance of our software.
    • Analyze existing internal and partner security designs.

    Requirements: A Master's degree or PhD in Cryptography or a related field, or equivalent training or work experience. Uncompromising integrity, outstanding attention to detail, programming experience.

    We can offer: competitive salary, relocation support, 25 holidays and travel expense remuneration.

    Closing date for applications:

    Contact: francisco.vialprado@fortanix.com

    Expand
    University of Amsterdam
    Job Posting Job Posting
    We are seeking two PhD candidates interested in interdisciplinary research on the development, efficient implementation (hardware and software), use, orchestration, and improvement of privacy-preserving and data anonymization techniques.

    What are you going to do?

    • Carry out original research in the field of implementation and applications of privacy preserving technologies for data analytics in healthcare
    • Be active in the fundamental and/or applied research area, publishing in high level international journals and presenting at leading conferences
    • Take part in ongoing educational activities, such as assisting in a course and guiding student thesis projects, at the BSc or MSc level
    • Collaborate with other groups, institutes and/or companies by contributing expertise to joint research projects
    • Contribute to activities and deliverables of the SECURED Horizon Europe Project
    What do you have to offer?

    • An MSc degree in Computer Science, Computer Engineering, or Electrical Engineering (or a related discipline)
    • Strong analytical and technical skills; Good problem-solving skills
    • An interdisciplinary mindset and an open and proactive personality in interacting with researchers from different disciplines
    • A strong scientific interest in security and privacy, in particular in at least one of the following two fields:
    • efficient implementation of cryptographic and privacy preserving primitives, both in hardware and in software
    • application, orchestration, and improvement of privacy-preserving techniques to achieve given data protection objectives
    • The willingness to work in a highly international research team;
    • Fluency in oral and written English and good presentation skills
    • Ability to assess practical implementation of privacy preserving techniques
    More information and application form:

    https://vacatures.uva.nl/UvA/job/Two-PhD-Positions-on-Efficient-Privacy-preserving-Techniques-for-Data-Analysis-and-Machine/760571702/

    Closing date for applications:

    Contact: Francesco Regazzoni

    More information: https://tinyurl.com/4s4kzwn6

    Expand
    Chen-Da Liu-Zhang, Christian Matt, Søren Eller Thomsen
    ePrint Report ePrint Report
    Messages in large-scale networks such as blockchain systems are typically disseminated using flooding protocols, in which parties send the message to a random set of peers until it reaches all parties. Optimizing the communication complexity of such protocols and, in particular, the per-party communication complexity is of primary interest since nodes in a network are often subject to bandwidth constraints. Previous flooding protocols incur a communication complexity of $\Omega(l\cdot n \cdot (\log(n) + \kappa))$ bits to disseminate an $l$-bit message among $n$ parties with security parameter $\kappa$. In this work, we present the first flooding protocols with optimal total communication complexity of $O(l\cdot n)$ bits and per-party communication of $O(l)$ bits. We further show how our protocols can be instantiated provably securely in proof-of-stake blockchains. To demonstrate that one of our new protocols is not only asymptotically optimal but also practical, we perform several probabilistic simulations to estimate the concrete complexity for given parameters. Our simulations show that our protocol significantly improves the per-party communication complexity over the state-of-the-art for practical parameters. Hence, for given bandwidth constraints, our results allow to, e.g., increase the block size, improving the overall throughput of the blockchain.
    Expand
    Michael Walter
    ePrint Report ePrint Report
    The recent work of Chaturvedi et al. (ePrint 2022/685) claims to observe leakage about secret information in a ciphertext of TFHE through a timing side-channel on the (untrusted) server. In (Chaturvedi et al., ePrint 2022/1563) this is combined with an active attack against TFHE and FHEW. The claims in (Chaturvedi et al., ePrint 2022/685) about the non-trivial leakage from a ciphertext would have far-reaching implications, since the server does not have any secret inputs. In particular, this would mean a weakening of LWE in general, since an adversary could always simulate a server on which there is side channel leakage.

    In this short note, we show that the claims made in the two aforementioned works with regards to the leakage through the timing side channel are false. We demonstrate that the active attack, a standard attack against IND-CPA secure LWE-based encryption, can be mounted just as efficiently without the "side channel information".
    Expand

    13 December 2022

    Giulia Scaffino, Lukas Aumayr, Zeta Avarikioti, Matteo Maffei
    ePrint Report ePrint Report
    Cross-chain communication is instrumental in unleashing the full potential of blockchain technologies, as it allows users and developers to exploit the unique design features and the profit opportunities of different existing blockchains. Solutions based on trusted third parties (TTPs) suffer from security and scalability drawbacks; hence, increasing attention has recently been given to decentralized solutions. Lock contracts (e.g., HTLCs and adaptor signatures) and chain relays emerged as the two most prominent attempts to achieve cross-chain communication without TTPs. Lock contracts enable efficient synchronization of single transactions over different chains but are limited in expressiveness as they only support the development of a restricted class of applications (e.g., atomic swaps). On the other hand, chain relays enable the development of arbitrary cross-chain applications but are extremely expensive to operate in practice because they need to synchronize every on-chain transaction, besides assuming a quasi Turing-complete scripting language, which makes them incompatible with Bitcoin-based and scriptless blockchains.

    We introduce Glimpse, a novel on-demand cross-chain synchronization primitive, which is both efficient in terms of on-chain costs and computational overhead, and expressive in terms of applications it supports. The key idea of Glimpse is to synchronize transactions on-demand, i.e., only those relevant to realize the cross-chain application of interest. We present a concrete instantiation which is compatible with blockchains featuring a limited scripting language (e.g., Bitcoin-based chains like Liquid), and, yet, can be used as a building block for the design of DeFi applications such as lending, pegs, wrapping/unwrapping of tokens, Proof-of-Burn, and verification of multiple oracle attestations. We formally define and prove Glimpse security in the Universal Composability (UC) framework and conduct an economical security analysis to identify the secure parameter space in the rational setting. Finally, we evaluate the cost of Glimpse for Bitcoin-like chains, showing that verifying a simple transaction has at most 700 bytes of on-chain overhead, resulting in a one-time fee of 3$, only twice as much as a basic Bitcoin transaction.
    Expand
    Endres Puschner, Thorben Moos, Steffen Becker, Christian Kison, Amir Moradi, Christof Paar
    ePrint Report ePrint Report
    Verifying the absence of maliciously inserted Trojans in ICs is a crucial task – especially for security-enabled products. Depending on the concrete threat model, different techniques can be applied for this purpose. Assuming that the original IC layout is benign and free of backdoors, the primary security threats are usually identified as the outsourced manufacturing and transportation. To ensure the absence of Trojans in commissioned chips, one straightforward solution is to compare the received semiconductor devices to the design files that were initially submitted to the foundry. Clearly, conducting such a comparison requires advanced laboratory equipment and qualified experts. Nevertheless, the fundamental techniques to detect Trojans which require evident changes to the silicon layout are nowadays well-understood. Despite this, there is a glaring lack of public case studies describing the process in its entirety while making the underlying datasets publicly available. In this work, we aim to improve upon this state of the art by presenting a public and open hardware Trojan detection case study based on four different digital ICs using a Red Team vs. Blue Team approach. Hereby, the Red Team creates small changes acting as surrogates for inserted Trojans in the layouts of 90 nm, 65 nm, 40 nm, and 28 nm ICs. The quest of the Blue Team is to detect all differences between digital layout and manufactured device by means of a GDSII–vs–SEM-image comparison. Can the Blue Team perform this task efficiently? Our results spark optimism for the Trojan seekers and answer common questions about the efficiency of such techniques for relevant IC sizes. Further, they allow to draw conclusions about the impact of technology scaling on the detection performance.
    Expand
    Behzad Abdolmaleki, Saikrishna Badrinarayanan, Rex Fernando, Giulio Malavolta, Ahmadreza Rahimi, Amit Sahai
    ePrint Report ePrint Report
    Secure computation is a cornerstone of modern cryptography and a rich body of research is devoted to understanding its round complexity. In this work, we consider two-party computation (2PC) protocols (where both parties receive output) that remain secure in the realistic setting where many instances of the protocol are executed in parallel (concurrent security). We obtain a two-round concurrent-secure 2PC protocol based on a single, standard, post-quantum assumption: The subexponential hardness of the learning-with-errors (LWE) problem. Our protocol is in the plain model, i.e., it has no trusted setup, and it is secure in the super-polynomial simulation framework of Pass (EUROCRYPT 2003). Since two rounds are minimal for (concurrent) 2PC, this work resolves the round complexity of concurrent 2PC from standard assumptions. As immediate applications, our work establishes feasibility results for interesting cryptographic primitives such as The first two-round password authentication key exchange (PAKE) protocol in the plain model and the first two-round concurrent secure computation protocol for quantum circuits (2PQC).
    Expand
    Yuejun Wang, Baocang Wang, Qiqi Lai, Yu Zhan
    ePrint Report ePrint Report
    An Identity-based matchmaking encryption (IB-ME) scheme proposed at CRYPTO 2019 supports anonymous but authenticated communications in a way that communication parties can both specify the senders or receivers on the fly. IB-ME is easy to be used in several network applications requiring privacy-preserving for its efficient implementation and special syntax. In the literature, IB-ME schemes are built from the variants of Diffie-Hellman assumption and all fail to retain security for quantum attackers. Despite the rigorous security proofs in previous security models, the existing schemes are still possibly vulnerable to some potential neglected attacks. Aiming at the above problems, we provide stronger security definitions considering new attacks to fit real-world scenarios and then propose a generic construction of IB-ME satisfying the new model. Inspired by the prior IB-ME construction of Chen et al., the proposed scheme is constructed by combining 2-level anonymous hierarchical IBE (HIBE) and identity-based signature (IBS) schemes. In order to upgrade lattice-based IB-ME with better efficiency, we additionally improve a lattice IBS, as an independent technical contribution, to shorten its signature and thus reduce the final IB-ME ciphertext size. By combining the improved IBS and any 2-level adaptively-secure lattice-based HIBE with anonymity, we finally obtain the first IB-ME from lattices.
    Expand
    Trevor Miller
    ePrint Report ePrint Report
    As digital tokens on blockchains such as non-fungible tokens (NFTs) increase in popularity and scale, the existing interfaces (ERC-721, ERC-20, and many more) are being exposed for being expensive and not scalable. As a result, tokens are being forced to be implemented on alternative blockchains where it is cheaper but less secure. To offer a solution without making security tradeoffs, we propose using joint cryptographic accumulators (e.g. joint Merkle trees). We propose a method of creating such joint accumulators in a decentralized fashion which is secured by the same set of validating nodes as existing blockchains. Such accumulators allow the tokens for certain applications to be implemented using up to 99.99% less of the blockchain’s resources by outsourcing most of the storage and computational requirements to the users creating the tokens. This is done without sacrificing permanence and verifiability of these tokens. This system achieves optimizations mainly by allowing certain storage of a blockchain to be used in a cross-application manner, instead of a per-application manner. Additionally, we show how it can be beneficial in other areas like privacy-preserving timestamps or shortening file hashes
    Expand
    Safiullah Khan, Wai-Kong Lee, Angshuman Karmakar, Jose Maria Bermudo Mera, Abdul Majeed, Seong Oun Hwang
    ePrint Report ePrint Report
    To mitigate cybersecurity breaches, secure communication is crucial for the Internet of Things (IoT) environment. Data integrity is one of the most significant characteristics of security, which can be achieved by employing cryptographic hash functions. In view of the demand from IoT applications, the National Institute of Standards and Technology (NIST) initiated a standardization process for lightweight hash functions. This work presents field-programmable gate array (FPGA) implementations and carefully worked out optimizations of four Round-3 finalists in the NIST standardization process. A novel compact PHOTON-Beetle implementation is proposed wherein the underlying matrix multiplication is executed in serialized fashion to achieve a small hardware footprint. SPARKLE implementations are carried out by implementing the ARX-box in serialized, parallelized, and hybrid approaches. For Ascon and XOODYAK, the proposed implementations compute certain permutation rounds in one clock cycle in order to explore the trade-off between computation time and hardware area. As a result, this work achieves the smallest hardware footprint for PHOTON-Beetle consuming an area 3.4× smaller than state-of-the-art implementations. Ascon and XOODYAK are implemented in a flexible manner that achieves throughput-to-area (TP/A) ratios 1.8× and 3.9× higher, respectively, compared to implementations found in the literature. In addition, we propose the first FPGA implementations for the SPARKLE hash function. These efficient implementations provide guidelines for choosing a suitable architecture for applications in demand that can be employed in the IoT environment to achieve data integrity for various applications.
    Expand
    Freja Elbro, Christian Majenz
    ePrint Report ePrint Report
    We present an algebraic attack on a McEliece-like scheme based on BCH codes (BCH-McEliece), where the Goppa code is replaced by a suitably permuted BCH code. Our attack continues the line of work devising attacks against McEliece-like schemes with Goppa-like codes, with the goal of getting a better understanding of why Goppa codes are so intractable. Our starting point is the work of Faugère, Perret and Portzamparc (Asiacrypt 2014). We take their algebraic model and adapt and improve their attack algorithm so that it can handle BCH-McEliece. We implement the attack and exhibit a parameter range where our attack is practical while generic attacks suggest cryptographic security.
    Expand
    Lingyue Qin, Jialiang Hua, Xiaoyang Dong, Hailun Yan, Xiaoyun Wang
    ePrint Report ePrint Report
    The Meet-in-the-Middle (MitM) attack has been widely applied to preimage attacks on Merkle-Damg{\aa}rd (MD) hashing. In this paper, we introduce a generic framework of the MitM attack on sponge-based hashing. We find certain bit conditions can significantly reduce the diffusion of the unknown bits and lead to longer MitM characteristic. To find good or optimal configurations of MitM attacks, e.g., the bit conditions, the neutral sets, and the matching points, we introduce the bit-level MILP-based automatic tools on Keccak, Ascon and Xoodyak. To reduce the scale of bit-level models and make them solvable in reasonable time, a series of properties of the targeted hashing are considered in the modelling, such as the linear structure and CP-kernel for Keccak, the Boolean expression of Sbox for Ascon. Finally, we give an improved 4-round preimage attack on Keccak-512/SHA3, and break a nearly 10 years’ cryptanalysis record. We also give the first preimage attacks on 3-/4-round Ascon-XOF and 3-round Xoodyak-XOF.
    Expand
    Elena Dubrova, Kalle Ngo, Joel Gärtner
    ePrint Report ePrint Report
    CRYSTALS-Kyber has been selected by the NIST as a public-key encryption and key encapsulation mechanism to be standardized. It is also included in the NSA's suite of cryptographic algorithms recommended for national security systems. This makes it important to evaluate the resistance of CRYSTALS-Kyber's implementations to side-channel attacks. The unprotected and first-order masked software implementations have been already analysed. In this paper, we present deep learning-based message recovery attacks on the $\omega$-order masked implementations of CRYSTALS-Kyber in ARM Cortex-M4 CPU for $\omega \leq 5$. The main contribution is a new neural network training method called recursive learning. In the attack on an $\omega$-order masked implementation, we start training from an artificially constructed neural network $M^{\omega}$ whose weights are partly copied from a model $M^{\omega-1}$ trained on the $(\omega-1)$-order masked implementation, and then extended to one more share. Such a method allows us to train neural networks that can recover a message bit with the probability above 99% from high-order masked implementations.
    Expand

    10 December 2022

    Ruben Gonzalez, Thom Wiggers
    ePrint Report ePrint Report
    TLS is ubiquitous in modern computer networks. It secures transport for high-end desktops and low-end embedded devices alike. However, the public key cryptosystems currently used within TLS may soon be obsolete as large-scale quantum computers, once realized, would be able to break them. This threat has led to the development of post-quantum cryptography (PQC). The U.S. standardization body NIST is currently in the process of concluding a multi-year search for promising post-quantum signature schemes and key encapsulation mechanisms (KEMs). With the first PQC standards around the corner, TLS will have to be updated soon. However, especially for small microcontrollers, it appears the current NIST post-quantum signature finalists pose a challenge. Dilithium suffers from very large public keys and signatures; while Falcon has significant hardware requirements for efficient implementations.

    KEMTLS is a proposal for an alternative TLS handshake protocol that avoids authentication through signatures in the TLS handshake. Instead, it authenticates the peers through long-term KEM keys held in the certificates. The KEMs considered for standardization are more efficient in terms of computation and/or bandwidth than the post-quantum signature schemes.

    In this work, we compare KEMTLS to TLS 1.3 in an embedded setting. To gain meaningful results, we present implementations of KEMTLS and TLS 1.3 on a Cortex-M4-based platform. These implementations are based on the popular WolfSSL embedded TLS library and hence share a majority of their code. In our experiments, we consider both protocols with the remaining NIST finalist signature schemes and KEMs, except for Classic McEliece which has too large public keys. Both protocols are benchmarked and compared in terms of run-time, memory usage, traffic volume and code size. The benchmarks are performed in network settings relevant to the Internet of Things, namely low-latency broadband, LTE-M and Narrowband IoT. Our results show that KEMTLS can reduce handshake time by up to 38%, can lower peak memory consumption and can save traffic volume compared to TLS 1.3.
    Expand
    Seth Hoffert
    ePrint Report ePrint Report
    Nonces are a fact of life for achieving semantic security. Generating a uniformly random nonce can be costly and may not always be feasible. Using anything other than uniformly random bits can result in information leakage; e.g., a timestamp can deanonymize a communication and a counter can leak the quantity of transmitted messages. Ideally, we would like to be able to efficiently encrypt the nonce to 1) avoid needing uniformly random bits and 2) avoid information leakage. This paper presents two new authenticated encryption modes built on top of Farfalle that perfectly achieve these goals.
    Expand
    Cas Cremers, Charlie Jacomme, Aurora Naska
    ePrint Report ePrint Report
    The building blocks for secure messaging apps, such as Signal's X3DH and Double Ratchet (DR) protocols, have received a lot of attention from the research community. They have notably been proved to meet strong security properties even in the case of compromise such as Forward Secrecy (FS) and Post-Compromise Security (PCS). However, there is a lack of formal study of these properties at the application level. Whereas the research works have studied such properties in the context of a single ratcheting chain, a conversation between two persons in a messaging application can in fact be the result of merging multiple ratcheting chains. In this work, we initiate the formal analysis of secure messaging taking the session-handling layer into account, and apply our approach to Sesame, Signal's session management. We first experimentally show practical scenarios in which PCS can be violated in Signal by a clone attacker, despite its use of the Double Ratchet. We identify exactly how this is enabled by Signal's session-handling layer. We then design a formal model of the session-handling layer of Signal that is tractable for automated verification with the Tamarin prover, and use this model to rediscover the PCS violation and propose two provably secure fixes to offer stronger guarantees.
    Expand
    ◄ Previous Next ►