【摘 要】
：
比特币引入了一种新的P2P(Peer to Peer)交易方法,并依靠其底层协议实现去中心化交易.然而,由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模,比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则,系统地抽象了多协议组合运行考虑下的比特币协议实体交互,完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比,本文更细粒度地建模了比特币协议实体及其相关操作,并全面设计了满足比特币各实体需求的安全属性.此外,本文利用自动化形式化验证系统SmartV
【机 构】
：
安徽工程大学计算机与信息学院,安徽芜湖241000;中国科学技术大学计算机科学与技术学院,安徽合肥230026;中国科学技术大学计算机科学与技术学院,安徽合肥230026;安徽工程大学计算机与信息学院
论文部分内容阅读
比特币引入了一种新的P2P(Peer to Peer)交易方法,并依靠其底层协议实现去中心化交易.然而,由于目前缺乏对比特币各底层协议的细粒度形式化分析和系统建模,比特币安全性并未被保证.本文通过设计多维度的比特币安全模型引理和细粒度的比特币模型规则,系统地抽象了多协议组合运行考虑下的比特币协议实体交互,完成了对比特币的形式化符号建模与自动化安全分析.与以前的工作相比,本文更细粒度地建模了比特币协议实体及其相关操作,并全面设计了满足比特币各实体需求的安全属性.此外,本文利用自动化形式化验证系统SmartVerif实现了无需额外手工推导证明的形式化验证实验,通过将本文所建模的符号模型规则与引理作为SmartVerif的输入,发现了比特币底层协议算力盗取攻击.
其他文献
针对空间能源系统在卫星寿命末期的钝化需求,分析了不同轨道卫星锂电池的温度条件,同时分析了锂电池位置、卫星姿态对其温度的影响.基于上述分析的温度范围,研究了锂电池在钝化后发生热失控的可能性和影响因素,分析得到基于锂电池的空间电源系统钝化需求.在此基础上,提出了4种可行的钝化解决方案,并从受空间环境影响程度、额外增加元器件的情况以及钝化后电路受电流应力情况等方面进行对比,分析结果表明,旁路钝化方案是基于锂离子电池的电源系统钝化的首选方案.
针对毫米波大规模MIMO(Multiple-Input Multiple-Output)系统能量效率低下的问题,提出一种基于混合精度移相器量化的混合预编码设计方法.首先考虑到系统能量效率闭合表达式难以直接求解,通过Dinkelbach方法将能量效率优化问题转换为范数最小化的形式,然后将其进一步解耦为混合预编码矩阵和混合精度移相器量化配比问题,实现非凸能效低范数和的凸优化转化,最后通过引入酉矩阵松弛恒模约束求解混合预编码矩阵,并采用增量搜索算法求解混合量化移相器精度配比向量,从而实现系统能量效率最大化.仿真
为解决传统互补序列集中序列数目受限的问题,近年来有学者提出集间低相关性完全互补码(CCC,Complete Complementary Code)的概念.集间低相关性的完全互补码具有良好的非周期自相关和互相关特性,作为多小区多载波码分多址(MC-CDMA,Multi-Carrier Code Division Multiple Access)通信系统中的扩频码可有效消除小区内的干扰,同时也可以抑制小区间的干扰.该文提出两类具有集间低相关性的完全互补码集的构造方法,得到的序列集具有以下特性:(1)每个码集都
正则语言推断研究从语言的有限信息出发,通过归纳和推理得出正则语言模型.该技术在信息抽取、软件工程、模式识别等领域应用广泛.本文首先阐明了语言的可学习性概念和推断结果的评价准则.然后从推理策略、数据结构、算法复杂性等方面,对被动、主动和基于神经网络的学习算法进行分类归纳与对比,梳理各流派的技术发展脉络.接着分析推断产生的三种泛化效应.最后指出当前研究中不足,对未来研究方向进行展望.
针对冲击噪声下多输入多输出(Multiple-Input Multiple-Output,MIMO)雷达阵列诊断失效问题,对基于二阶矩的传统匹配滤波器进行改进以适应非高斯噪声,并提出一种基于张量分解和K-means聚类的阵列诊断方法.该方法利用MIMO雷达各接收阵元回波信号的高斯核函数值来自适应地调整匹配滤波器的系数,以有效形成虚拟阵列.为挖掘正常和故障阵元的匹配滤波输出数据的多维特征,将虚拟阵列协方差矩阵构建成三阶平行因子(PARAllel FAC-tor,PARAFAC)张量,并通过COMFAC(CO
由于受环境、资源、能耗、异构等因素制约,海上无线技术发展明显滞后于陆地.以低开销、自适应和自主融合为约束,提出一种海上边缘计算云边智能协同服务策略模型(Model of Cloud-Edge Cooperative Service Scheme for Maritime Edge Computing,MCECS-MEC).基于边缘计算构建海上云边智能协同服务网络框架,抽象海上边缘计算节点行为特征,建立具有抑制联合作弊的节点信任和推荐量化综合评价模型,根据其综合属性评价将准盟员节点融合聚类到不同的协同服务池
分布式声传感器阵列在军事侦察、公共安全监控和人机交互等领域应用广泛.但时钟异步、频率响应失配和节点位置未知问题严重影响后续基于分布式声传感器阵列的语音处理算法的性能,因此近年来学者们热衷于研究校准这三类阵列失配问题的方法.首先,本文介绍了导致分布式声传感器网络各类失配问题的原因和三类问题解决的先后顺序.然后,将现有的解决三类问题的方法进行了综述.其中,时钟同步方法主要包括基于时间戳交换和短时傅里叶变换域线性相位漂移的方法,频率响应校准方法主要包括基于声源导向矢量和自适应滤波器的方法,节点位置/位姿校准方法
为了提升粒子群算法的全局寻优与局部精细搜索能力并加快收敛速度,提出了基于直觉模糊熵的混合粒子群优化算法.该算法采用粒子的历史最优解信息构造直觉模糊熵的自适应函数,并将熵值作为扰动因子动态调节惯性权重,同时建立自适应全局最优粒子学习策略对扰动后的粒子进行训练,在保持多样性传播的基础上选择学习对象,使粒子探索更多新区域,实现种群间的协作与并行进化.通过仿真实验,将本文算法与两种衍生算法以及其他改进粒子群算法在11个测试函数上进行比较,结果表明,本算法在求解精度、收敛速度和寻优效率上均有更好表现.
近年来,群体智能作为一项多学科融合的新技术在各领域的研究成果斐然,例如共享出行、蜂群无人机系统、水下多智能体平台等,但与水下场景结合的群体智能技术缺乏系统的归纳,有必要对水下群体智能技术的发展现状和趋势进行讨论和分析.本文对群体智能理论进行了详尽的分析,给出了群体智能的完整概念、具体算法以及应用领域.文中指出,为解决海洋复杂环境对探测、通信等造成的一系列困难,需要将群体智能技术应用于水下场景.本文就国内外水下群体智能技术的研究现状进行了总结,对水下群体智能存在的环境复杂、通信受限、信息获取困难、系统能力不
基于非交换群的抗量子密码体制是密码学的一个研究热点,其群的阶在一定程度上保证了求逆运算的困难性.本文对二元生成的传递置换群的阶这一代数命题进行了研究,给出了传递置换群的充分必要条件,以及二元生成的传递置换群阶的下界估计式.在实例化生成g1,g2使传递置换群的阶满足相应下界值的过程中,给出了一类特殊n阶轮换表成两个n元置换g1,g2乘积的方法,以及相应的二元生成的传递置换群的设计算法.最后,阐述了传递置换群在对称密码体制中的应用.