资料下载
×
基于定理证明其的有限域及其形式化研究
消耗积分:0 |
格式:rar |
大小:1.38 MB |
2021-04-25
分享资料个
有限域GF（2″）是多种安全关键性算法的基础，包括AES加密算法、椭圆曲线加密和感染函数掩码等。相关资料表明，有限域上的运算因为自身的复杂性而容易出错，从而导致系统问题。基于测试和基于模型检测的验证方法只能在η固定的特定有限域上进行验证，而且计算量往往超出计算机的能力。基于交互式定理证眀器的形式化验证为有限域性质的通用验提供了可能性，但这方面的工作难度较大。已有研究主要针对有服域的抽象性质进行形式化验证，但计算机领域更关心的是有限域的构造性定义及相关性质的验证。针对这些问题，借助定理证明器COQ，建立了有限域GF（2″）并给出了其基本运算的构造性定义，同时对一组与有限城有关的基本性质进行了形式化验证，包括有限域加法基本性质的验证、多项式乘法基本性质的验证等，其中多项式乘法是有限域乘法的基础。这项工作为有限堿的完整的形式化及基于有限堿的算法的形式化验证奠定了基础。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
