Verified Security of BLT Signature Scheme
summary
Formalizes and mechanically verifies that a BLT-style signature scheme becomes existentially unforgeable when a forward‑resistant tagging primitive combines with a backdating‑resistant timestamp repository, using EasyCrypt's probabilistic relational logic. Builds a concrete reduction: forgery probability is bounded by hash collision resistance when the repo stores plain (message,tag) pairs, and by tagging forward‑resistance when the adversary can append entries. Notes the proof uncovers subtle binding choices that change security assumptions and that the tagging primitive itself is assumed, not yet machine‑verified.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:42Motivation
- 1:35What are hash functions
- 3:32Quantum attacks
- 5:01Formal verification
- 8:42Collision resistance theorem
- 10:42Signature scheme
- 12:02Nonrepudiation property
- 13:37Timestamping
- 16:39Results
- 19:30Future work
- 21:33Interaction
- 22:48Blockchain
related talks
34mProvably Secure Blockchain Protocols and Applications to Secure Computation
31mOn the Adaptive Security of Key-Unique Threshold Signatures
40mPost-Quantum
20mCryptographic Signatures: A Building Block Not A Panacea
01h 34mHow to Build Digital Signatures From Hash Functions
39mWhen Is a Proof Actually Not?
41mFormally Verifying Everybody's Cryptography
18mSecure Software Distribution in an Adversarial World