通用模型的机器验证形式化：非交互式与交互式算法解析

### 通用模型的机器验证形式化：非交互式与交互式算法解析 #### 1. 多项式定义现状 多项式有多种可能的定义。在Coq开发中，不同的形式化方法采用了不同的多项式表示。例如，Geuvers等人对代数基本定理（FTA）的形式化使用了单变量多项式的霍纳表示；Théry对Buchberger算法的形式化使用了单项式的顺序来避免单项式的重复项；Pottier对代数结构的形式化使用了多项式表达式的归纳定义。最近，Grégoire和Mahboubi探索了多元多项式的替代表示，以实现高效的自反策略。然而，目前缺乏一个标准且全面的多项式库。为了为通用模型（GM）和随机预言机模型（ROM）的进一步工作提供坚实基础，开发这样一个库是很有必要的，或许可以利用多项式不同表示之间的同构性。 #### 2. 非交互式通用算法 ##### 2.1 非形式化描述 设$G$是一个以$g$为生成元、素数阶为$q$的循环群。通用算法$A$在$G$上的定义如下： - **输入**：$l_1, \ldots, l_{t'}\in\mathbb{Z}_q$，这些输入依赖于一组秘密，通常是秘密密钥，例如$s_1, \ldots, s_k\in\mathbb{Z}_q$。后续定义算法的群输入$f_1, \ldots, f_{t'}\in G$，其中$f_k = g^{l_k}$。 - **运行**：即一系列$t$步。每一步可以是输入步骤或多元指数运算（mex）步骤。输入步骤从群输入中读取一些输入，为简单起见，假设所有输入在开始时恰好读取一次，对于$1\leq i\leq t'$，算法在第$i$步从群输入中读取$f_i$。对于$t' < i\leq t$，假设算法在第$i$步执行mex步骤，即任意选择$a_{i1}, \ldots, a_{it'}\in\mathbb{Z}_q$并计算$f_i = \prod_{1\leq j\leq t'} f_j^{a_{ij}}$。 通用算法$A$的输出是列表$f_1, \ldots, f_t$。进一步定义碰撞为$f_j = f_{j'}$（$1\leq j < j'\leq t$），如果碰撞$f_j = f_{j'}$以概率1成立，即对于所有秘密数据的选择都成立，则称该碰撞为平凡碰撞。如果算法$A$发现非平凡碰撞，则记为$CO(A)$。 通用模型将攻击者视为通用算法$A$，攻击者试图通过测试输出之间的等式（即非平凡碰撞，平凡碰撞不揭示任何关于秘密的信息）来获取秘密信息，如果第一种方法失败，则对秘密进行随机猜测。因此，算法$A$找到秘密$s_j$的概率可以从算法发现非平凡碰撞的概率$ProbColl(A)$推导得出，即$CO(A)$成立的概率。为了给出$ProbColl(A)$的上界，通用模型依赖于Schwartz引理。为此，通用模型假设$A$是一个通用算法，其群输入$f_j$的形式为$g^{m_j(s_1, \ldots, s_k)}$，其中$m_j(x_1, \ldots, x_k)$是关于秘密参数集合$X = \{x_1, \ldots, x_k\}$的多元单项式，$s_1, \ldots, s_k$是实际的秘密。 **示例1：离散对数问题** 算法的输入是群生成元$g\in G$和公钥$h = g^r\in G$，输出是对$\log_g h = r$的猜测$y$。任何非平凡碰撞都能揭示$r$的值，因为每个$f_i$的形式为$g^{a_i}(g^r)^{a_i'} = g^{(a_i + r a_i')}$。因此，对于任何碰撞$f_i = f_j$，有$g^{(a_i + r a_i')} = g^{(a_j + r a_j')}$，所以$r(a_i' - a_j') \equiv a_j - a_i \pmod{q}$。如果碰撞是非平凡的，则$a_i' - a_j' \neq 0$，可以推导出$r$的值。在这个例子中，只有一个秘密$r$，形式输入是单项式$1 = r^0$和$r$。 **示例2：判定性Diffie - Hellman问题** 算法的输入是群生成元$g\in G$、群元素$g^x$和$g^y$，以及随机顺序的群元素$g^{xy}$和$g^z$，其中$x, y, z$是$\mathbb{Z}_q$中的随机数，输出是对$g^{xy}$的猜测（或等效地，对$g^{xy}$和$g^z$顺序的猜测）。在这个例子中，有三个秘密$x$、$y$和$z$，形式输入是单项式$1$、$x$、$y$、$xy$和$z$。 ##### 2.2 形式化描述 形式化通用算法的主要困难在于正式捕捉秘密的概念。通过引入形式秘密参数类型$Sec$和解释函数$\sigma: Sec\rightarrow\mathbb{Z}_q$，将形式秘密输入映射到实际秘密。 进一步假设给定一个长度为$t'$的非重复单项式列表$input: listmonSec$，设$m_1, \ldots, m_{t'}$是$input$的元素。这些单项式构成算法的形式输入，实际输入可以定义为$map (Evalmon \sigma) input: list\mathbb{Z}_q$。 通用算法的类型定义为记录类型： ```plaintext GA = {run : listlistZq ; ok : ... } ``` 其中，$run$是算法在每一步选择的指数列表（指数本身也聚集在一个列表中），$ok$是一个谓词，保证$run$具有一些合适的属性，特别是： - $run$的所有元素长度也为$t'$。 - 对于$1\leq j\leq t'$，$run$的第$j$个元素是第$j$个元素为$1$，其余元素为$0$的列表。 - $run$是一个非重复列表，以避免平凡碰撞。 通用算法的输出通过以下方式获得：从指数$a_{i1}, \ldots, a_{it'}$计算多项式$p_i = \sum_{1\leq j\leq t'} a_{ij} m_j$，然后用$\sigma$评估每个多项式$p_i$，最终得到$\mathbb{Z}_q$中的元素$f_i$（与非形式化描述相比，将输出视为$\mathbb{Z}_q$中的元素更方便，因为$\mathbb{Z}_q$和$G$是同构的）。 形式上，通用算法的输出建模为： ```plaintext output : listZq := map (eval pol σ) (map (λl. zip l input) run) ``` 其中，$zip$是类型为$\forall A, B : Type. listA\rightarrow listB\rightarrow list(A\times B)$的函数。 然后，$CO(A)$定义为$doubles output$，其中$doubles$是一个布尔值函数，用于检查列表中是否有重复项。注意，碰撞发生当且仅当存在两两不同的$i$和$i'$，使得$eval pol \sigma p_i =_{\mathbb{Z}_q} eval pol \sigma p_{i