摘要:智能合约是运行在区块链上的计算机协议，被广泛应用在各个领域中，但是其安全问题层出不穷，因此在智能合约部署到区块链上之前，需要对其进行安全审计.然而，传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言（MSVL）和命题投影时序逻辑（PPTL）对智能合约进行建模和验证：首先介绍了MSVL与PPTL的理论基础；之后，通过分析和对比Solidity与MSVL语言的特性，开发了能够将Solidity程序转换为MSVL程序的SOL2M转换器，并详细介绍了SOL2M转换器的设计思路；最终，通过投票智能合约和银行转账智能合约两个实例，给出了SOL2M转换器的执行结果.使用PPTL从功能一致性、逻辑正确性以及合约完备性这3个方面描述了合约的性质，给出了使用统一模型检测器（UMC4M）对合约进行验证的过程.

摘要:总结了安全协议的20年研究进展情况,指出形式化方法在安全协议的设计与分析中的重要应用.对安全协议的若干热点研究方向进行了归纳和展望.

摘要:加密协议的分析需要形式化的方法和工具.该文定义了加密协议描述语言PEP (principals+environment=protocol),并说明对于一类加密协议,其PEP描述可以转化为有穷的基本CCS进程,由此可以在基于CCS的CWB(concurrency workbench)工具中分析加密协议的性质.此方法的优点在于隐式地刻画攻击者的行为,试图通过模型检查(model checking)发现协议潜在的安全漏洞,找到攻击协议的途径.

摘要:在软件方法学中，形式方法越来越受到人们的重视，并已被应用于软件开发．Z是一种基于数学表示的软件规格说明方法．前置条件的简化是Z规格说明方法中一种标准的检查，本文讨论了Z规格说明中关于操作的前置条件及其计算．提出了简化过程的终止条件，给出了一个用于简化前置条件的算法，该算法可自动产生简化过程的证据．