Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by HASLab

2025

Private Computation of Boolean Functions Using Single Qubits

Authors
Rahmani, Z; Pinto, AN; Barbosa, LS;

Publication
PARALLEL PROCESSING AND APPLIED MATHEMATICS, PPAM 2024, PT II

Abstract
Secure Multiparty Computation (SMC) facilitates secure collaboration among multiple parties while safeguarding the privacy of their confidential data. This paper introduces a two-party quantum SMC protocol designed for evaluating binary Boolean functions using single qubits. Complexity analyses demonstrate a reduction of 66.7% in required quantum resources, achieved by utilizing single qubits instead of multi-particle entangled states. However, the quantum communication cost has increased by 40% due to the amplified exchange of qubits among participants. Furthermore, we bolster security by performing additional quantum operations along the y-axis of the Bloch sphere, effectively hiding the output from potential adversaries. We design the corresponding quantum circuit and implement the proposed protocol on the IBM Qiskit platform, yielding reliable outcomes.

2025

Paraconsistency for the Working Software Engineer (Extended Abstract)

Authors
Barbosa, LS;

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2024

Abstract
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. This lecture summarises recent joint work with Juliana Cunha, Alexandre Madeira and Ana Cruz on a variant of transition systems endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values. Such structures are called paraconsistent transition systems, the qualifier stressing a connection to paraconsistent logic, a logic taking inconsistent information as potentially informative. A coalgebraic perspective on this family of structures is also discussed.

2025

Specification of paraconsistent transition systems, revisited

Authors
Cunha, J; Madeira, A; Barbosa, LS;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
The need for more flexible and robust models to reason about systems in the presence of conflicting information is becoming more and more relevant in different contexts. This has prompted the introduction of paraconsistent transition systems, where transitions are characterized by two pairs of weights: one representing the evidence that the transition effectively occurs and the other its absence. Such a pair of weights can express scenarios of vagueness and inconsistency. . This paper establishes a foundation for a compositional and structured specification approach of paraconsistent transition systems, framed as paraconsistent institution. . The proposed methodology follows the stepwise implementation process outlined by Sannella and Tarlecki.

2025

Formally Verified Correctness Bounds for Lattice-Based Cryptography

Authors
Barbosa, M; Kannwischer, MJ; Lim, TH; Schwabe, P; Strub, PY;

Publication
CCS

Abstract
Decryption errors play a crucial role in the security of KEMs based on Fujisaki-Okamoto because the concrete security guarantees provided by this transformation directly depend on the probability of such an event being bounded by a small real number. In this paper we present an approach to formally verify the claims of statistical probabilistic bounds for incorrect decryption in lattice-based KEM constructions. Our main motivating example is the PKE encryption scheme underlying ML-KEM. We formalize the statistical event that is used in the literature to heuristically approximate ML-KEM decryption errors and confirm that the upper bounds given in the literature for this event are correct. We consider FrodoKEM as an additional example, to demonstrate the wider applicability of the approach and the verification of a correctness bound without heuristic approximations. We also discuss other (non-approximate) approaches to bounding the probability of ML-KEM decryption. © 2025 Copyright held by the owner/author(s).

2025

Privacy and Security of FIDO2 Revisited

Authors
Barbosa, M; Boldyreva, A; Chen, S; Cheng, K; Esquível, L;

Publication
Proc. Priv. Enhancing Technol.

Abstract

2025

Tempo: ML-KEM to PAKE Compiler Resilient to Timing Attacks

Authors
Arriaga, A; Barbosa, M; Jarecki, S;

Publication
IACR Cryptol. ePrint Arch.

Abstract

  • 8
  • 266