CPN Tools 只能建模简单逻辑性结构协议

Posted 2021-03-18 xinxianquan

我觉得有必要将CPN Tools中的 ML关于函数的定义的部分单独拿出来做一个博客写。 因为CPN Tools中的函数 只能表示逻辑关系，不能表示协议中算法相关的性质。比方加解密函数，对称以及非对称函数。

首先我们对CPN Tools中出现的函数做一个介绍，看看具体都有哪些函数定义：

      CPN ML函数实现了标准的逻辑控制结构编程语言   if   ------case -------else   的功能。基于ML构成的函数语言功能最大的功能就是递归作用。

       fun id pat1= exp1 | id pat2=exp2   |.......| id patn=expn;

 从pat1 到 patn , 以及从表达式 exp1到expn  都时相同的类型，表达式的意思是 ，在某种情况下确实有参数满足 pat1 或者patn，那么对用的函数计算的值为 表达式 exp1或者 expn .

    下面的函数定义了阶乘 关系：

     fun fact(0)=1 | fact(i)=i * fact(i- 1);

除了上面的额一种函数表达之外还有 if -then -else 函数表达控制结构，描述如下：

      if bool-exp   then  exp1 else exp2;   这其中 表达式 exp1和 exp2有相同的类型

      case  exp of

          pat1=>exp1 | pat2=> exp2 |...| patn=> expn    其中 exp1 ....expn有相同的类型， 

 let结构允许在函数内部定义局部变量。

       let   val pat1=exp1

              val  pat2=exp2

              val patn=expn

       in

               exp

         end;

   举例： 定义一毫米为单位计算的换算过程使用ML 函数表达：

     fun  metr(x)=

          let

                   val mminm=1000;

           in

             x div mminm

            end;

最常见的是随机数函数 ，随机数函数有自己规定的表达式，有的人在协议形式化中将协议中的随机数 写成 colset Nonce=with 1.n。 其实按照协议本身严格语义来说这就是错误的，甚至有人将随机数 在ML中颜色集定义中写成  colset Nonce:int 。这个基本上就是没有理解协议和CPN Tools ML。 那么随机数在CPN tools 中如何实现，具体看下面：

       单纯就ML 语言来说 随机数的颜色集定义有三种： 新鲜值变量方法、函数 ran 方法、特殊随机分布函数。 先吃饭.....