One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)

• URL: http://arxiv.org/abs/2505.10316v1
• Date: Thu, 15 May 2025 14:01:30 GMT
• Title: One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version)
• Authors: Xenia Hofmeier, Andrea Raguso, Ralf Sasse, Dennis Jackson, David Basin,
• Abstract summary: BLS aggregate signatures are a popular kind of aggregate signature, deployed by Dfinity, and Cloudflare amongst others.<n> BLS aggregate signatures are difficult to use correctly, with nuanced requirements that must be carefully handled by protocol developers.<n>We design the first models of aggregate signatures that enable formal verification tools, such as Tamarin and ProVerif, to be applied to protocols using these signatures.
• Score: 6.604074204101799
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Aggregate signatures are digital signatures that compress multiple signatures from different parties into a single signature, thereby reducing storage and bandwidth requirements. BLS aggregate signatures are a popular kind of aggregate signature, deployed by Ethereum, Dfinity, and Cloudflare amongst others, currently undergoing standardization at the IETF. However, BLS aggregate signatures are difficult to use correctly, with nuanced requirements that must be carefully handled by protocol developers. In this work, we design the first models of aggregate signatures that enable formal verification tools, such as Tamarin and ProVerif, to be applied to protocols using these signatures. We introduce general models that are based on the cryptographic security definition of generic aggregate signatures, allowing the attacker to exploit protocols where the security requirements are not satisfied. We also introduce a second family of models formalizing BLS aggregate signatures in particular. We demonstrate our approach's practical relevance by modelling and analyzing in Tamarin a device attestation protocol called SANA. Despite SANA's claimed correctness proof, with Tamarin we uncover undocumented assumptions that, when omitted, lead to attacks.

Related papers

• Linearly Homomorphic Ring Signature Scheme over Lattices [7.911831986965765]
  Homomorphic ring signature schemes combine the strong anonymity of ring signatures with the computability of homomorphic signatures.<n>No feasible homomorphic ring signature scheme currently exists.<n>We propose the first lattice-based linearly homomorphic ring signature scheme.
  arXiv  Detail & Related papers  (2025-07-03T03:43:40Z)
• Privacy-Preserving Biometric Verification with Handwritten Random Digit String [49.77172854374479]
  Handwriting verification has stood as a steadfast identity authentication method for decades.<n>However, this technique risks potential privacy breaches due to the inclusion of personal information in handwritten biometrics such as signatures.<n>We propose using the Random Digit String (RDS) for privacy-preserving handwriting verification.
  arXiv  Detail & Related papers  (2025-03-17T03:47:25Z)
• An Undeniable Signature Scheme Utilizing Module Lattices [0.0]
  An undeniable signature scheme is type of digital signature where the signer retains control over the signature's verifiability. We develop a module lattice-based post-quantum undeniable signature system.
  arXiv  Detail & Related papers  (2024-10-25T00:09:29Z)
• Reusable Formal Verification of DAG-based Consensus Protocols [8.277981465630377]
  This paper presents safety-verified specifications for five DAG-based consensus protocols.<n>Four of these protocols -- DAG-Rider, Cordial Miners, Hashgraph, and Eventualous BullShark -- are well-established in the literature.<n>We employ TLA+ for specifying the protocols and writing their proofs, and the TLAPS proof system to automatically check the proofs.
  arXiv  Detail & Related papers  (2024-07-02T11:19:12Z)
• Investigating the Common Authorship of Signatures by Off-Line Automatic Signature Verification Without the Use of Reference Signatures [3.3498759480099856]
  This paper addresses the problem of automatic signature verification when no reference signatures are available. The scenario we explore consists of a set of signatures, which could be signed by the same author or by multiple signers. We discuss three methods which estimate automatically the common authorship of a set of off-line signatures.
  arXiv  Detail & Related papers  (2024-05-23T10:30:48Z)
• Revocable Quantum Digital Signatures [57.25067425963082]
  We define and construct digital signatures with revocable signing keys from the LWE assumption. In this primitive, the signing key is a quantum state which enables a user to sign many messages. Once the key is successfully revoked, we require that the initial recipient of the key loses the ability to sign.
  arXiv  Detail & Related papers  (2023-12-21T04:10:07Z)
• Appeal: Allow Mislabeled Samples the Chance to be Rectified in Partial Label Learning [55.4510979153023]
  In partial label learning (PLL), each instance is associated with a set of candidate labels among which only one is ground-truth. To help these mislabeled samples "appeal," we propose the first appeal-based framework.
  arXiv  Detail & Related papers  (2023-12-18T09:09:52Z)
• MProto: Multi-Prototype Network with Denoised Optimal Transport for Distantly Supervised Named Entity Recognition [75.87566793111066]
  We propose a noise-robust prototype network named MProto for the DS-NER task. MProto represents each entity type with multiple prototypes to characterize the intra-class variance. To mitigate the noise from incomplete labeling, we propose a novel denoised optimal transport (DOT) algorithm.
  arXiv  Detail & Related papers  (2023-10-12T13:02:34Z)
• Securing Deep Generative Models with Universal Adversarial Signature [69.51685424016055]
  Deep generative models pose threats to society due to their potential misuse. In this paper, we propose to inject a universal adversarial signature into an arbitrary pre-trained generative model. The proposed method is validated on the FFHQ and ImageNet datasets with various state-of-the-art generative models.
  arXiv  Detail & Related papers  (2023-05-25T17:59:01Z)
• FedSOV: Federated Model Secure Ownership Verification with Unforgeable Signature [60.99054146321459]
  Federated learning allows multiple parties to collaborate in learning a global model without revealing private data. We propose a cryptographic signature-based federated learning model ownership verification scheme named FedSOV.
  arXiv  Detail & Related papers  (2023-05-10T12:10:02Z)
• Secure access system using signature verification over tablet PC [62.21072852729544]
  We describe a highly versatile and scalable prototype for Web-based secure access using signature verification. The proposed architecture can be easily extended to work with different kinds of sensors and large-scale databases.
  arXiv  Detail & Related papers  (2023-01-11T11:05:47Z)
• Quotable Signatures for Authenticating Shared Quotes [0.8875650122536799]
  Quotable signature schemes are digital signature schemes with the additional property that from the signature for a message, any party can extract signatures for (allowable) quotes from the message. We define a notion of security for quotable signature schemes and construct a concrete example of a quotable signature scheme. We consider both how quotable signatures can be used, and why using them could help mitigate the effects of fake news.
  arXiv  Detail & Related papers  (2022-12-21T12:07:46Z)
• Offline Signature Verification on Real-World Documents [9.271640666465363]
  Signatures extracted from formal documents may contain different types of occlusions, for example, stamps, company seals, ruling lines, and signature boxes. In this paper, we address a real-world writer independent offline signature verification problem, in which, a bank's customers' transaction request documents that contain their occluded signatures are compared with their clean reference signatures. Our proposed method consists of two main components, a stamp cleaning method based on CycleGAN and signature representation based on CNNs.
  arXiv  Detail & Related papers  (2020-04-25T10:28:03Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.