上周，我们在ASE 2025会议发表了论文“Securing Millions of Decentralized Identities in Alipay Super App with End-to-End Formal Verification”，是关于用形式化方法分析和验证分布式身份协议的。所以，这篇博客，我将介绍一下，形式化验证在协议安全分析方面的应用情况。

最早接触到“协议安全”+“形式化”，是2018读到LTEInspector（NDSS’18）这篇论文，我在以前的博客里写过它，“对LTE INSPECTOR论文的一些解读”。它对接入和寻呼等关键流程进行了形式化建模，用ProVerif进行了验证，发现了若干问题。其他一些我印象深刻的论文还有：David Basin的信用卡支付协议验证[1]；David的苹果的iMessage后量子协议验证[2]；北邮校友冯皓楠的FIDO协议验证[3]。

这些研究都是基于Model Checking技术的，其中应用最广泛的工具有2个，Tamarin和ProVerif，我个人更偏爱Tamarin，因为这个语言写起来更自然更轻松。目前更推荐的方法是，使用SAPIC+语言建模，它可以同时支持多个主流的model checking工具，Tamarin/ProVerif/DeepSec。

另外还有一些协议形式化验证，不是基于model checking的，而是纯手工的形式化建模和证明。比较出名的工作集中在Web protocol方面，比如可以去看看Daniel Fett的工作，这位大佬是个独立研究员，一直活跃在IETF标准组织，同时做安全协议设计和验证工作。他对OAuth协议、OpenID协议等做了很多研究和贡献。说实话，这个流派我不太懂，没认真学习过。我理解，之所以没有用model checking，可能是因为Web协议中的某些行为，model checking工具难以描述，或者即使强行用它描述，也会导致规模太大无法证明。

接下来我们只讨论，基于model checking类的协议形式化验证。回顾一下形式化验证的概念：

形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。

在这个例子中：

  • 对象：DID协议（论文中还做了代码实现的验证，这部分暂不讨论）。
  • 形式化语言：Tamarin
  • 性质：DID协议应具有机密性、完整性、单射性，以及隐私保护等性质。

看一个具体例子

IIFAA DID协议的所有标准，主要在IIFAA官网，这个网站需要企业成员注册权限，不能公开访问标准文档。所以下面以公开访问的w3c cndid社区的文档，来举例。DID协议大致可以分为，凭证颁发，出示凭证等环节。让我们来看一下，凭证出示这个步骤，在标准中的自然语言描述是怎样的。

d. The terminal selects a proper VC based on the configurations, constructs VP content using the SP’s DID and public key, and then signs the VP content with the user’s private key to generate a VP (4).
e. The terminal encrypts the VP with the SP’s public key and then transmits it to the SP (5).

这里的SP = Service Provider, 也就是Verifier。这段自然语言描述的内容，在Tamarin模型中对应的形式化语言是这样的：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
rule SuperAppConstructVPwithDisclosure[color=#6495ED]:
    let 
      C = P ++ D
      credential = <sigJWT, C> 
      payload = <sigJWT, D>
      proof = sign(payload, skH)
      VP = <payload, proof>
      eenvkey = aenc(~envkey, pkV)
      eVP = senc(VP, ~envkey)
      Presentation = <eVP, eenvkey>
    in
    [ JSAPI_In('RequestVP', appid, request_VP) 
    , !SuperApp($UserName, $Number, userid)
    , !TEELTK($Holder, userid, skH)
    , !MPK($Verifier, appid, pkV)
    , !VC(userid, credential)
    , Fr(~envkey) ]
  --[ LHolderPresentVP(userid, appid, VP)
    , VPrequestFrom(appid)
    , CredentialPresent($UserName, Presentation)
    , HolderPresent(userid, Presentation) ]->
    [ JSAPI_Out('PresentVP', appid, <$UserName, Presentation>) ]

Tamarin语言的基本语法结构是：对每个状态都可以写成，[前提]–[事件]->[后续]，这样的结构，称之为 rewrite rule。在上面这个例子中，‘前提’是，

1
2
3
4
5
6
[ JSAPI_In('RequestVP', appid, request_VP) 
    , !SuperApp($UserName, $Number, userid)
    , !TEELTK($Holder, userid, skH)
    , !MPK($Verifier, appid, pkV)
    , !VC(userid, credential)
    , Fr(~envkey) ]

意思是，必须收到一个出示VP的请求，必须有user’s private key,即skH，等等。‘事件’是，CredentialPresent($UserName, Presentation)等等，这些不太重要。‘后续’是，JSAPI_Out(‘PresentVP’, appid, <$UserName, Presentation>)，意思是从JSAPI接口输出一个Presentation（VP）。那么VP是如何构造的呢？在这段代码中，

1
2
3
4
5
6
7
8
9
10
let 
      C = P ++ D
      credential = <sigJWT, C> 
      payload = <sigJWT, D>
      proof = sign(payload, skH)
      VP = <payload, proof>
      eenvkey = aenc(~envkey, pkV)
      eVP = senc(VP, ~envkey)
      Presentation = <eVP, eenvkey>
    in

这里描述了如何签名、加密等等操作。与自然语言版本有些不一致的地方是，1）增加了‘选择性披露’的能力，这部分在标准的其他地方有介绍；2）加密VP时用的是一个对称密钥，eVP = senc(VP, ~envkey)，而不是自然语言版本中的‘SP’s public key’，这是因为代码实现是这样做的，这里与代码对齐。因此，进行formal modeling的过程，就是对标准文本不断的清晰化的过程。

通过把每一个协议步骤建模为rule，就能把整个协议变成一个状态转移系统（Transition System）。然后在这个状态转移系统中，通过算法严格的验证，存在某种路径，或者不存在某种路径。

例如我们看一个安全性质，VC的完整性。在Tamarin代码中，需要验证的性质，用lemma这个关键字表达。

1
2
3
4
5
6
7
8
lemma VCIntegrity[hide_lemma=NonInjectAuthVCIssurance, heuristic={integrity}]:
    "All #i userid data credential.
      SuperAppVC(userid, data, credential)@i
      ==>
        (Ex #j appid.
          IssueVC(appid, credential)@j & #j < #i) 
      | (Ex appid ltk #i. Reaveal(appid, ltk)@i)
    "

这段代码的意思是，对于所有的凭证，如果用户的App中存了一个凭证，那么这个凭证一定是由某个Issuer签发的，或者是由于这个Issuer的签名密钥丢失了。换句话说，这个凭证一定有签名而且能被验签。不存在被篡改，且通过验签的情况。

这一条安全性质，在IIFAA DID标准中对应的自然语言表述是， 5.2 Data Security 部分：

e. Data integrity: Integrity shall be ensured during data transmission to protect data from being tampered with.

它没有说，哪些‘data’需要完整性保护，只是笼统的说要防篡改，要有完整性保护。我们在形式化验证中，挑选了 credential，验证它的完整性。当然你可以用同样方法，逐个验证其它的data。

Tamarin验证方法的信任基础

从上面这个例子，你会发现，Tamarin语言把密码学的操作，都抽象成sign()签名, aenc()非对称加密，senc()对称加密，这样的函数。而且定义了，如adec(aenc(m, pk(sk)),sk) = m，这样的等式，明确了解密和加密之间的关系。这意味着，Tamarin模型，不讨论密码学模块本身的安全漏洞，假设密码学模块都是可信的。

另外，这种验证方法，还需要信任工具本身，也就是信任Tamarin的原理和代码实现是没有错误的。

协议形式化验证的优缺点

为什么形式化验证在协议安全分析方面，应用并不广泛？我认为有以下一些原因：

  • 需求不迫切，很多协议并不要求‘极度安全’。比如支付协议，为了用户体验好、使用便利，是可以容忍支付协议存在风险的，只要实际应用中资损率不太高，都是可以接受的。再比如通信协议，对所有链路都使用高安全的加密和鉴权功能，会大大增加网络设备/终端的成本、功耗、延时等等，因此一定要在安全与成本之间权衡。
  • 需求不多，协议的种类是很少的。协议要实现互联互通，它必须是标准化的、统一的，不能五花八门的。因此大家重点关注的协议，总共就那么几个：TLS、移动网络3GPP中的部分协议、全球通用的信用卡支付协议。如果把区块链、智能合约，也看作一种协议，那么这类协议种类就非常多了，每发行一种币，就产生一个新的协议。所以用形式化方法验证区块链协议，有巨大的市场需求。这个商业模式，已经被市场验证。

当然，形式化方法在协议验证方面，仍然有一定价值。我们在DID这篇论文中，总结了几点：

  • 高效的形式化验证有助于辅助协议设计和实现：现在很多协议更新迭代非常快，比如MCP、A2A这些智能体相关的协议，文档经常更新。LLM可以辅助，把自然语言文本，转换为形式化语言的模型。因此，维护一套，自然语言文档-形式化模型-代码，这样的spec-driven的开发工作流，将是非常高效的协议设计和开发的新模式。

  • 形式化验证有助于澄清协议的‘安全Contract’：虽然由于现实中的协议，并不要求严格的安全，但形式化验证能严谨的表达，什么条件下安全性质是成立的，从而把协议的安全承诺显式表达出来。就像保险条款、手术知情同意书，会详尽的罗列能保障什么，不能保障什么。这对于业务团队，是非常有价值和意义的。

值得研究的方向

  • 从设计到实现的自动代码生成：一边设计，一边顺手把代码生成出来，而且能保证代码的正确性。我们已经看到近期有一些研究工作，比如OwlC（USENIX Security‘25），从协议设计开始，使用形式化语言Owl，然后自动生成协议的Rust代码，用Verus验证工具保证代码逻辑正确性。另外，调用底层密码学模块的时候，使用已被验证的Rust密码库，确保它们是安全的。
  • 引入成本vs风险分析能力：这些形式化工具只能给出，是或否的答案，却不能告诉我们安全的概率有多大，风险的可能性到底有多小。就好像我读完了保险条款，仍然不知道，该不该买保险。如果形式化验证能与成本收益分析结合起来，将有助于业务团队做决策。我个人模糊的觉得，这个方向可能与‘计算经济学’相关。

参考文献

  1. ‘The EMV Standard: Break, Fix, Verify’，https://arxiv.org/abs/2006.08249
  2. ‘A Formal Analysis of Apple’s iMessage PQ3 Protocol’
  3. ‘A Formal Analysis of the FIDO UAF Protocol’
  4. Daniel Fett’s work, https://scholar.google.com/citations?user=o0ViW0UAAAAJ