比特幣(BTC)後量子安全實驗 程式碼結合機器驗證推出「概念驗證」

比特幣(BTC)開發者公開了用於後量子簽章研究的函式庫「libshrincs」。這並非直接套用在比特幣主網的更新，而是一項概念驗證，將以C語言撰寫的程式碼與安全性證明一併交由機器驗證來檢查。

Blockstream研究員喬納斯·尼克（Jonas Nick）與開發者remix7531於12日（南韓時間）在Delving Bitcoin論壇上公開了libshrincs。這套函式庫以C語言實作了SHRINCS的一次性簽章元件WOTS+C，SHRINCS是外界提出用於比特幣的後量子簽章方案之一。

開發團隊使用Rocq Prover與SSProve將安全性證明形式化，再透過VST驗證C語言實作是否符合Rocq規格書的定義，證明過程中有相當比重借助大型語言模型(LLM)完成。

此次公開的重點並非提出新的密碼學方案，而是更貼近運用AI輔助的證明研究延伸至比特幣密碼學證明與實作驗證的一次嘗試。

GitHub儲存庫將libshrincs定位為「概念驗證(proof-of-concept)」，並註明C語言程式碼與VST合約仍屬暫定狀態，未來可能變動。

實作與驗證工具依角色分工：實作採用C語言，安全性證明使用Rocq 9.0搭配SSProve、MathComp，功能驗證則使用Rocq 9.0搭配VST、CompCert。「make audit」指令的設計目的，是以表格方式僅檢查獲允許的假設。

libshrincs所依據的SHRINCS，是一套考量區塊鏈儲存空間有限而設計的雜湊式後量子簽章方案。所謂後量子密碼學，是指即使面對量子電腦攻擊仍能維持安全的加密技術。

Blockstream說明，SHRINCS在有狀態(stateful)模式下產生的簽章大小為324位元組；當簽章狀態毀損或遺失時，可改用替代的無狀態(stateless)路徑，其簽章大小則為3至8KB。Blockstream表示，這種方式所需的簽章資料量，比NIST標準替代方案節省97%的區塊空間。

喬納斯·尼克此前曾提出將後量子簽章導入比特幣的構想：在Taproot樹中另外設置一條支出路徑，平時使用既有的Schnorr簽章，需要時再開啟後量子簽章路徑。

Taproot能將多種支出條件納入樹狀結構，只公開實際使用的條件。不過，若要在比特幣主網新增簽章驗證功能，仍需要修改共識規則，並經過比特幣改進提案(BIP)討論。

目前這項研究的侷限也很明確。開發團隊表示，他們整理出的證明尚未提供完整的QROM後量子安全保證，採用的安全性概念也弱於實際部署環境的要求，這正是libshrincs不能被視為已納入比特幣核心(Bitcoin Core)程式碼的原因。

有狀態簽章必須妥善保存同一把金鑰的使用紀錄。一旦備份重複使用，或裝置狀態遭到重置，簽章的安全性就可能被削弱，因此硬體錢包與韌體如何管理狀態，被視為關鍵課題。

在Delving Bitcoin的討論中，將平時低手續費路徑與復原用的無狀態路徑並存的設計獲得正面評價。但也有人提出裝置狀態重置錯誤、備份重複使用、斷電等實際使用過程中可能出現的營運風險。

喬納斯·尼克說明，匯入種子(seed)的裝置應該只使用無狀態路徑。他也表示，要判斷硬體錢包能否安全維持狀態，仍需要錢包開發者提供實務回饋。

remix7531在個人部落格中指出，LLM雖然能加快證明完成速度，但也可能讓寫錯的規格更快通過驗證。因此libshrincs的設計方向，並非增加複雜證明，而是盡量減少需要人工檢查的規格與假設。