形式化分析--模型检测

一、形式化分析：模态逻辑技术+模型检测技术+定理证实技术

     模型检验是一种自动验证技术，它被成功地应用于验证电脑硬件，并也开始被用于验证电脑软件。

    模型检验技术包括有限状态机、Petri网和通讯进程演算。

 

二、模型检测技术

  参考1--科学网文章：模型检验和维数灾难（Model Checking and the Curse of Dimensionality） 

     2007年图灵奖  Edmund M.Clarke是卡耐基梅隆大学计算机科学学院FORE荣誉教授、电气和计算机工程教授

     http://blog.sciencenet.cn/blog-1225851-762490.html

     

    参考2--Model Checking Methods for Security Protocols

         Model checking, also known as finite-state analysis, involves using verification tools to exhaustively search all execution sequences for desired properties in a protocol specification. 

        This method has been successfully applied to a number of security protocols developed by the IEEE, IETF Working Groups, and others. Many of the examples below make use of the Murphi verification system。

The following paper and set of slides provides an overview of this work. For further details, please read the other papers included below.

【1】J. C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Murphi, Proceedings of the 1997 IEEE Symposium on Security and Privacy, May 1997, Pages 141-151. [ Paper ]
【2】J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]

     http://seclab.stanford.edu/pcl/mc/mc.html

 

Murphi的下载地址：http://formalverification.cs.utah.edu/Murphi/

Murphi的入门及安装：https://blog.csdn.net/weixin_36869329/article/details/79949914

CMurphi须要自行编译可执行版本。编译环境要求： 
 Linux系统 
 g++ 
 LEX词法分析器生成器，通常使用flex 
 YACC语法分析器生成器，通常使用byacc 
 GNU make 
如上准备就绪后，进入CMurphi的src目录，运行命令 
 make或者make mu，生成可执行文件 
 make clean，清理编译过程当中产生的中间文件 
 make cleanall，清理全部中间文件，包括LEX和YACC所生成的文件 
编译成功后，该目录便可出现可执行文件mu，可根据须要将CMurphi的安装目录添加到环境变量中。

   

PReach
Preach is an industrial strength distributed explicit state model checker based on Murphi. 
https://bitbucket.org/jderick/preach/wiki/Home

三、Formal Methods for the Analysis of Wireless Network Protocols-牛津大学博士论文2011   （注：E:\文章\Paper\形式化文章）