基于CompCert内存模型的智能合约中间语言的可信编译

1

作者 许颖 张亚丰 +5 位作者 许晶航 康跃馨 夏清 袁峰 左春 李玉成 《信息安全学报》 2026年第1期22-36,共15页

智能合约是区块链技术的重要组成部分之一,具有不可篡改、自动执行等特点,为去中心化应用提供了丰富的编程基础。近年来相关安全漏洞事件频发,使得智能合约的安全性研究逐渐成为热点。其中,智能合约编译器的误编译问题会令源代码编译产... 智能合约是区块链技术的重要组成部分之一,具有不可篡改、自动执行等特点,为去中心化应用提供了丰富的编程基础。近年来相关安全漏洞事件频发,使得智能合约的安全性研究逐渐成为热点。其中,智能合约编译器的误编译问题会令源代码编译产生不符合开发者原本预期的目标代码,导致部署在区块链上的代码存在安全隐患,然而现有工作较少考虑到这一问题。因此,首先从避免合约安全漏洞的原则出发,设计一种非图灵完备的智能合约领域专用语言isCL。作为可信编译的源语言,它支持复合数据类型与内置函数,以便于开发人员编写合约;然后设计可信编译器i2c的整体架构,实现以C语言子集Clight语言为目标语言的完整翻译过程;再针对基于CompCert内存模型的智能合约中间语言的翻译阶段,定义消除复合类型、出参入参合并、生成Clight三个翻译阶段的相关语法、语义,并给出语义保持性的证明思路;最后通过服装供应链分账应用实例和Solidity、Rust的编译漏洞案例来分别说明isCL语言的实用性与智能合约可信编译的有效性。本文工作为智能合约的可信编译提供了研究思路,有利于促进智能合约开发的安全性研究,为实现更加安全可信的区块链应用提供有力支撑。 展开更多

关键词 区块链 智能合约语言 领域专用语言 形式化验证 经过验证的编译器

在线阅读 下载PDF 职称材料

基于下推自动机的同步数据流语言可信编译 被引量：1

2

作者 于涛 王珊珊 +6 位作者 徐芊卉 董晓晗 胡代金 罗杰 杨溢龙 吕江花 马殿富 《软件学报》 北大核心 2025年第8期3554-3569,共16页

同步数据流语言Lustre是安全关键系统开发中常用的开发语言,其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证,对用户也处于黑盒状态.近年来,通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法... 同步数据流语言Lustre是安全关键系统开发中常用的开发语言,其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证,对用户也处于黑盒状态.近年来,通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法被证明是成功的.基于下推自动机的编译方法和基于语义一致性的验证方法,提出Lustre语言可信编译方法,能够将Lustre语言转换为C语言并进行形式化验证以保证编译的正确性,并使用Isabelle对翻译转换过程进行严格的正确性证明. 展开更多

关键词 同步数据流语言 经过验证的编译器 形式化验证 Lustre语言

在线阅读 下载PDF 职称材料

同步数据流语言可信编译器的构造 被引量：18

3

作者 石刚 王生原 +6 位作者 董渊 嵇智源 甘元科 张玲波 张煜承 王蕾 杨斐 《软件学报》 EI CSCD 北大核心 2014年第2期341-356,共16页

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解... 同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作. 展开更多

关键词 同步数据流语言 经过验证的编译器 形式化验证 形式语义 定理证明

在线阅读 下载PDF 职称材料

可信编译器L2C的核心翻译步骤及其设计与实现 被引量：14

4

作者 尚书 甘元科 +2 位作者 石刚 王生原 董渊 《软件学报》 EI CSCD 北大核心 2017年第5期1233-1246,共14页

同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现... 同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好"误编译"问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如Comp Cert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(Comp Cert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验. 展开更多

关键词 经过验证的编译器 同步数据流语言 L2C Coq证明辅助器 核心翻译步骤

在线阅读 下载PDF 职称材料

一种用于指针程序验证的指针逻辑 被引量：6

5

作者 陈意云 李兆鹏 +1 位作者 王志芳 华保健 《软件学报》 EI CSCD 北大核心 2010年第3期415-426,共12页

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便... 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合. 展开更多

关键词 软件安全 HOARE逻辑 指针逻辑 携带证明的代码 出具证明的编译器

在线阅读 下载PDF 职称材料

一种汇编程序的形式验证框架 被引量：3

6

作者 李兆鹏 陈意云 +1 位作者 葛琳 华保健 《计算机研究与发展》 EI CSCD 北大核心 2008年第5期825-833,共9页

在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关... 在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查. 展开更多

关键词 软件安全 出具证明编译器 指针逻辑 HOARE逻辑 携带证明的汇编程序

在线阅读 下载PDF 职称材料

一个C语言安全子集的可信编译器 被引量：3

7

作者 王蕾 石刚 +2 位作者 董渊 白晓颖 王生原 《计算机科学》 CSCD 北大核心 2013年第9期30-34,共5页

以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全... 以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器。然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估。之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器。最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率。 展开更多

关键词 可信计算 CompCert C安全子集 经过验证的编译器

在线阅读 下载PDF 职称材料

汇编代码验证中的形式规范自动生成 被引量：3

8

作者 葛琳 陈意云 +2 位作者 华保健 李兆鹏 刘诚 《小型微型计算机系统》 CSCD 北大核心 2008年第7期1219-1224,共6页

与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明... 与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明的编译器自动生成汇编级形式规范,从而减轻程序员的负担.使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力.文章主要描述该方法在出具证明编译器中的实现. 展开更多

关键词 出具证明编译器 汇编代码验证 形式规范Hoare逻辑 前(后)条件

在线阅读 下载PDF 职称材料

同步数据流语言可信编译器的研究进展 被引量：5

9

作者 杨萍 王生原 《计算机科学》 CSCD 北大核心 2019年第5期21-28,共8页

同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。... 同步数据流语言(如Lustre,Signal)近年来在航空、高铁、核电等安全关键领域得到了广泛应用,因此与这类语言相关的开发工具本身的安全性问题受到高度关注。同步数据流语言到串行命令式语言的可信编译器是此类工具的典型代表(如Scade)。构造可信编译器的途径可分为两大类:一类是传统的方法,例如通过大量测试和严格的过程管理等手段来实现;另一类是通过形式化方法,例如直接对编译器本身进行形式化证明,采用翻译确认的方法等。近年来,形式化方法作为构造和验证可信编译器的关键途径而得到广泛的重视,有望最大限度地解决"误编译"问题,因而成为新的研究热点。文章在介绍可信编译器的形式化构造和验证方法的基础上,特别聚焦于同步数据流语言可信编译器的相关研究工作,对其现状进行综述和分析。 展开更多

关键词 同步数据流语言 经过验证的编译器 翻译确认 LUSTRE SIGNAL

在线阅读 下载PDF 职称材料

基于ECC的自认证广义指定验证者签密 被引量：2

10

作者 俞惠芳 王彩芬 王之仓 《计算机工程》 CAS CSCD 北大核心 2010年第16期124-125,共2页

广义指定验证者签名允许签名的持有者指定签名给指定的验证者,但仅有指定的验证者能够验证这个签名,针对该问题,利用椭圆曲线密码体制(ECC)和自认证签密的特点,提出一个基于ECC的自认证广义指定验证者签密。该方案不仅消除了证书存在问... 广义指定验证者签名允许签名的持有者指定签名给指定的验证者,但仅有指定的验证者能够验证这个签名,针对该问题,利用椭圆曲线密码体制(ECC)和自认证签密的特点,提出一个基于ECC的自认证广义指定验证者签密。该方案不仅消除了证书存在问题和密钥托管问题,而且具有算法复杂度低、处理速度快、存储空间占用小等特点,适合应用于电子投票、电子拍卖等领域。 展开更多

关键词 自认证签密 广义指定验证者签名 椭圆曲线密码体制

在线阅读 下载PDF 职称材料

自认证广义指定验证者签密方案 被引量：3

11

作者 俞惠芳 王彩芬 +1 位作者 王之仓 李艳霞 《计算机工程与应用》 CSCD 北大核心 2010年第34期89-91,共3页

基于自认证签密和广义指定验证者签名的思想,一个新的自认证广义指定验证者签密方案被提出,在椭圆曲线离散对数问题和双线性Diffie-Hellman问题的困难性假设下,该方案被证明是安全的。该方案允许签密的持有者指定签密给指定的验证者,仅... 基于自认证签密和广义指定验证者签名的思想,一个新的自认证广义指定验证者签密方案被提出,在椭圆曲线离散对数问题和双线性Diffie-Hellman问题的困难性假设下,该方案被证明是安全的。该方案允许签密的持有者指定签密给指定的验证者,仅仅只有指定的验证者能够验证这个签密,不存在证书管理问题和密钥托管问题,具有存储量小、安全性强等优点,在电子商务和电子政务中具有很实用的价值。 展开更多

关键词 自认证签密 广义指定验证者签名 椭圆曲线离散对数问题 双线性DIFFIE-HELLMAN问题

在线阅读 下载PDF 职称材料

CompCert编译器目标代码生成机制分析 被引量：2

12

作者 杨萍 王生原 《计算机科学》 CSCD 北大核心 2020年第9期17-23,共7页

CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其... CompCert是著名的C语言可信编译器,是经过形式化验证的编译器的杰出代表,近年来被广泛应用于学术界和工业界的许多研发工作中。CompCert编译器的当前版本支持多种目标机结构。文中对CompCert编译器目标代码生成机制进行剖析,主要介绍其设计逻辑、翻译过程、语义保持性以及代码结构,并给出了CompCert编译器重定向设计的要点。文中工作有助于实现CompCert重定向,比如实现面向重要国产处理器的后端。 展开更多

关键词 CompCert 形式化验证的编译器 目标代码生成 编译器重定向

在线阅读 下载PDF 职称材料

基于DLP的自认证代理签密方案 被引量：1

13

作者 俞惠芳 赵海兴 +1 位作者 王之仓 王小红 《计算机科学》 CSCD 北大核心 2010年第5期66-67,71,共3页

自认证密码体制可以实现无公钥证书和密钥托管,代理签密是将代理签名和签密相结合的一种方案。在已有研究的基础上,集成自认证密码体制和代理签密,提出了一种新的基于DLP的自认证代理签密方案,并在有限域上离散对数问题的难解性下,给出... 自认证密码体制可以实现无公钥证书和密钥托管,代理签密是将代理签名和签密相结合的一种方案。在已有研究的基础上,集成自认证密码体制和代理签密,提出了一种新的基于DLP的自认证代理签密方案,并在有限域上离散对数问题的难解性下,给出了其正确性和安全性证明。 展开更多

关键词 有限域上离散对数问题 代理签密 可公开验证 自认证密码体制

在线阅读 下载PDF 职称材料

基于类型注解的认证编译器设计与实现 被引量：1

14

作者 胡荣贵 陈意云 +1 位作者 郭帆 张昱 《计算机研究与发展》 EI CSCD 北大核心 2004年第1期28-33,共6页

基于类型注解的认证编译器是安全策略系统的核心部件 ,它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intelx86 /linux汇编语言程序 ,而且还可以根据类型安全策略的要求产生带注解的汇编程序 实验结果表明 ,新设计的认证编译... 基于类型注解的认证编译器是安全策略系统的核心部件 ,它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intelx86 /linux汇编语言程序 ,而且还可以根据类型安全策略的要求产生带注解的汇编程序 实验结果表明 ,新设计的认证编译器可实现 :①类型安全的C语言子集的编译 ;②许多标准的局部优化 ;③可以对数组运行时越界操作进行检查 由于安全策略系统的证明是建立在含注解的代码基础之上的 ,因此 。 展开更多

关键词 认证编译器 扩展的控制流图 携带证明的代码 类型安全

在线阅读 下载PDF 职称材料

基于扩展逻辑变换系统_μTS证明循环优化正确性 被引量：2

15

作者 王昌晶 《计算机研究与发展》 EI CSCD 北大核心 2012年第9期1863-1873,共11页

循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代... 循环优化对于提高Cache性能、发掘程序的并行性以及减少执行循环的开销都有着重要的作用,证明带循环优化功能的现代编译器的正确性已成为可信编译的一个挑战性的问题.形式化证明一个羽翼丰满的优化编译器本质上是不可行的,可以使用替代的方法,即不是证明优化编译器本身,而是形式化证明每一次循环变换前后编译对象的正确性.提出一种新颖的基于扩展逻辑变换系统μTS来证明循环优化正确性的方法.系统μTS在逻辑变换系统TS的基础上扩展了若干条派生规则,经谓词抽象将源程序与目标程序转换为形式化Radl语言后,使用μTS的派生规则能证明常见循环变换的正确性,如循环融合、循环分配、循环交换、循环反转、循环分裂、循环脱皮、循环调整、循环展开、循环铺盖、循环判断外提、循环不变代码外提等.循环优化可以看作一系列循环变换的组合,从而系统μTS能证明循环优化的正确性.为了支持自动化证明循环优化的正确性并出示证据,进一步提出了一个辅助证明算法.最后通过一个典型实例对这一方法进行了详细的阐述,实际效果表明了该方法的有效性.该方法对设计高可信优化编译器具有重要的指导意义. 展开更多

关键词 循环优化 可信编译 扩展逻辑变换系统 循环变换 辅助证明算法

在线阅读 下载PDF 职称材料

论钱谦益与明史的修撰与考证 被引量：2

16

作者 杨绪敏 《徐州师范大学学报（哲学社会科学版）》 北大核心 2012年第2期102-106,共5页

钱谦益在明清两朝均担任过史职,因此他始终以修国史为己任。早在天启初年他参与编纂《神宗实录》时就十分留心相关史料的搜集。他计划编纂一部纪传体《明史》,准备先作长编和事略,后作本纪和列传,并已纂修明史百卷,另编次明代文集百余卷... 钱谦益在明清两朝均担任过史职,因此他始终以修国史为己任。早在天启初年他参与编纂《神宗实录》时就十分留心相关史料的搜集。他计划编纂一部纪传体《明史》,准备先作长编和事略,后作本纪和列传,并已纂修明史百卷,另编次明代文集百余卷,可惜毁于绛云楼一炬。流传下来的《国初群雄事略》、《太祖实录辨证》两书,在客观保存元明之际的史料及考订史料真伪、弥补前史记载的缺漏、订正前史内容的错误等方面具有重要作用,并颇具特色。钱谦益对元末明初史事的编纂和考证,反映了他实事求是的治史精神。他考证史事,严格遵循言必有据的原则,其考史的成果多被清修《明史》所采纳。他所采用的考史方法对清初乃至乾嘉考据学都产生了一定的影响。 展开更多

关键词 钱谦益 明史 修纂 考证

在线阅读 下载PDF 职称材料

20世纪80年代以来国内李益诗歌研究述评 被引量：1

17

作者 沈文凡 张巍 《衡阳师范学院学报》 2007年第1期100-108,共9页

李益是中唐前期的著名诗人,近20年来李益研究逐渐深入。学界在李益生平事迹的考证、诗集的整理、作品真伪考辨以及李益诗歌的题材内容、艺术特色等方面取得了丰富的成果。同时,李益研究也存在着考证结论缺乏确凿证据,部分研究建立在前... 李益是中唐前期的著名诗人,近20年来李益研究逐渐深入。学界在李益生平事迹的考证、诗集的整理、作品真伪考辨以及李益诗歌的题材内容、艺术特色等方面取得了丰富的成果。同时,李益研究也存在着考证结论缺乏确凿证据,部分研究建立在前人颇多瑕疵的结论之上,选题立论及论述单一重复,部分领域无人涉及等问题。李益研究拥有广阔的前景,有待于学者去挖掘和探索。 展开更多

关键词 李益 中唐前期 诗集的整理 生平事迹 真伪考辨

在线阅读 下载PDF 职称材料

PCC中数组边界检查的优化和生成

18

作者 胡荣贵 陈意云 +1 位作者 郭帆 张昱 《小型微型计算机系统》 CSCD 北大核心 2003年第12期2278-2282,共5页

PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围 ,而造成拒绝执行一些安全的移动代码等问题 .本文给出的一种数组边界检查的优化及生成算法 ,不仅能够比较好地解决了这一问题 ,同时还生成了循环不变式注解中的条件谓... PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围 ,而造成拒绝执行一些安全的移动代码等问题 .本文给出的一种数组边界检查的优化及生成算法 ,不仅能够比较好地解决了这一问题 ,同时还生成了循环不变式注解中的条件谓词 .我们设计的编译器———认证编译器———已经实现了这些算法 ,并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86 /linux汇编语言程序的编译过程 .由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的 ,因此该认证编译器中实现的算法在移动代码安全检查中非常有用 . 展开更多

关键词 PCC 数组边界检查 认证编译器 控制流图 注解 移动代码 语言安全策略系统

在线阅读 下载PDF 职称材料

基于DLP的自认证广义指定验证者密签方案

19

作者 俞惠芳 赵海兴 +1 位作者 王之仓 杨林 《微电子学与计算机》 CSCD 北大核心 2010年第9期49-51,共3页

有机集成广义指定验证者签名和自认证签密的思想,提出了一个基于DLP的自认证广义指定验证者签密方案,方案的困难性基于有限域上的离散对数问题.所提方案不仅能够保护签密持有者的隐私,而且消除了证书存在问题和密钥托管问题.由于新方案... 有机集成广义指定验证者签名和自认证签密的思想,提出了一个基于DLP的自认证广义指定验证者签密方案,方案的困难性基于有限域上的离散对数问题.所提方案不仅能够保护签密持有者的隐私,而且消除了证书存在问题和密钥托管问题.由于新方案具有通信代价低、计算量少和安全性强等优点,在电子商务和电子政务活动中将具有重要应用. 展开更多

关键词 自认证签密 广义指定验证者签名 有限域上离散对数问题 强安全性

在线阅读 下载PDF 职称材料

使用双线性对的指定验证人代理签密

20

作者 俞惠芳 王彩芬 《计算机工程与应用》 CSCD 北大核心 2010年第18期125-127,共3页

指定验证人代理签密要求代理签密人只能对发给指定验证人的信息代理原始签密人签密,而其他人则不能代理原始签密人签密。基于指定验证人代理签密和自认证密码系统的理论,一个使用双线性对的指定验证人代理签密被提出。该方案具有以下特... 指定验证人代理签密要求代理签密人只能对发给指定验证人的信息代理原始签密人签密,而其他人则不能代理原始签密人签密。基于指定验证人代理签密和自认证密码系统的理论,一个使用双线性对的指定验证人代理签密被提出。该方案具有以下特点:在传送代理签密时,没有必要传送消息,因为指定验证人能从代理签密中正确恢复出消息;能够在逻辑单步内同时验证代理签密的有效性和公钥的真伪;克服了密钥托管问题;不需要对公钥显式认证。与已有方案相比,新方案仅仅需要2次pairings运算,效率很高。 展开更多

关键词 双线性对 指定验证人代理签密 自认证密码系统

在线阅读 下载PDF 职称材料