抱歉，您的浏览器无法访问本站
本页面需要浏览器支持（启用）JavaScript
了解详情 >

协议安全性验证（Tamarin Prover详细学习 ）

字数：8k 字

时长：32 分钟
其他

发布于：2024年5月1日

一、安装Tamarin Prover

1 安装Linuxbrew

1
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

2 添加 Linuxbrew 到 PATH

1
2
3
4
test -d ~/.linuxbrew && eval $(~/.linuxbrew/bin/brew shellenv)
test -d /home/linuxbrew/.linuxbrew && eval $(/home/linuxbrew/.linuxbrew/bin/brew shellenv)
test -r ~/.bash_profile && echo "eval \$($(brew --prefix)/bin/brew shellenv)" >>~/.bash_profile
echo "eval \$($(brew --prefix)/bin/brew shellenv)" >>~/.profile

Tips：这一步结束后最好重启一下。

重启以后测试一下

1
brew install hello

3 安装

1
brew install tamarin-prover/tap/tamarin-prover

二、Tamatin 语言学习

参考

https://github.com/tamarin-prover/teaching

1 初始样例解析

在 Tamarin-Prover 中，规则（rule）和引理（lemma）是协议模型的两个主要组 成部分。其中规则（rule）定义了系统中可能发生的事件或行为。一个规则由一 个前提和一个结论组成。前提描述了规则被触发的条件，这可能包括某些状态和 消息的存在。结论描述了在满足前提条件的情况下会发生什么，包括新状态的生 成和/或新消息的发送。规则在定义安全协议的操作步骤方面发挥着重要作用。

初始示例

我们将从一个仅由两条消息组成的协议的简单示例开始，在这里用所谓的Alice和Bob表示法编写：

1
2
C -> S: aenc(k, pkS)
C <- S: h(k)

在该协议中，客户端C生成新的对称密钥k，用服务器S的公钥pkS对其进行加密（aenc代表非对称加密），并将其发送给S。服务器通过将密钥的哈希发送回客户端来确认密钥的接收。

这个简单的协议是人为的，只满足非常弱的安全保证。我们将用它来说明Tamarin的一般工作流程，证明从客户的角度来看，只要服务器没有受到威胁，新生成的密钥是秘密的。默认情况下，对手是控制网络的Dolev -Yao对手，可以删除、注入、修改和拦截网络上的消息。

该协议的Tamarin模型及其安全属性在文件FirstExample.spthy（.spthy代表安全协议理论）中给出，该文件可以在本教程的github存储库中的文件夹代码中找到(https://github.com/tamarin-prover/manual)。Tamarin文件以理论开头，然后是该理论的名称，这里是FirstExample。

我们后面一点一点解析一下这个简单的协议
FirstExample.spthy

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

theory FirstExample
begin
builtins: hashing, asymmetric-encryption

// 注册一个公钥
rule Register_pk:
    [ Fr(~ltk) ]
  -->
    [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

rule Get_pk:
    [ !Pk(A, pubkey) ]
  -->
    [ Out(pubkey) ]

rule Reveal_ltk:
    [ !Ltk(A, ltk) ]
  --[ LtkReveal(A) ]->
    [ Out(ltk) ]

// 开始一个新的线程，执行客户端角色，并选择服务器。
rule Client_1:
    [ Fr(~k)         // 选择一个新鲜的秘钥
    , !Pk($S, pkS)   // 查找服务器的公钥。
    ]
  -->
    [ Client_1( $S, ~k )    // 存储服务器和密钥以供线程的下一步使用。
    , Out( aenc(~k, pkS) )  // 将加密的会话密钥发送给服务器。
    ]

rule Client_2:
    [ Client_1(S, k)   // Retrieve server and session key from previous step
    , In( h(k) )       // Receive hashed session key from network
    ]
  --[ SessKeyC( S, k ) ]-> // State that the session key 'k'
    []                     // was setup with server 'S'

// A server thread answering in one-step to a session-key setup request from
// some client.
rule Serv_1:
    [ !Ltk($S, ~ltkS)                             // lookup the private-key
    , In( request )                               // receive a request
    ]
  --[ AnswerRequest($S, adec(request, ~ltkS)) ]-> // Explanation below
    [ Out( h(adec(request, ~ltkS)) ) ]            // Return the hash of the
                                                  // decrypted request.

lemma Client_session_key_secrecy:
  " /* It cannot be that a  */
    not(
      Ex S k #i #j.
        /* client has set up a session key 'k' with a server'S' */
        SessKeyC(S, k) @ #i
        /* and the adversary knows 'k' */
      & K(k) @ #j
        /* without having performed a long-term key reveal on 'S'. */
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "

lemma Client_auth:
  " /* For all session keys 'k' setup by clients with a server 'S' */
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. AnswerRequest(S, k) @ a)
         /* or the adversary performed a long-term key reveal on 'S'
            before the key was setup. */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

lemma Client_auth_injective:
  " /* For all session keys 'k' setup by clients with a server 'S' */
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. AnswerRequest(S, k) @ a
           /* and there is no other client that had the same request */
           & (All #j. SessKeyC(S, k) @ #j ==> #i = #j)
       )
         /* or the adversary performed a long-term key reveal on 'S'
            before the key was setup. */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

lemma Client_session_key_honest_setup:
  exists-trace
  " Ex S k #i.
        SessKeyC(S, k) @ #i
      & not(Ex #r. LtkReveal(S) @ r)
  "

end

a 更多密码学原语

在本例中，我们使用Tamarin的内置函数进行哈希和非对称加密，声明如下：

1
builtins: hashing, asymmetric-encryption

这些内置组件给了我们:

  • 一元函数h，表示密码散列函数
  • aenc表示非对称加密算法的二进制函数
  • adec表示非对称解密算法的二进制函数，以及
  • 一元函数pk，其表示与私钥相对应的公钥。

此外，内置还指定使用正确的私钥对密文进行解密会返回初始明文，即

1
adec（aenc（m，pk（sk）），sk）

被缩减为m。

理解：表示一些冗余的加解密语句会被消除，比如对m进行加密又解密，那么这个语句就是m

我们完成了头的定义和原语的定义

FirstExample.spthy

1
2
3
4
5
6
7

theory FirstExample
begin
builtins: hashing, asymmetric-encryption
......

end

b 公钥基础设施建模

在Tamarin中，使用多集重写规则对协议及其环境进行建模。规则对系统的状态进行操作，系统的状态表示为多组事实。事实可以看作是存储状态信息的谓词。例如，事实Out(h(x))对协议在公共信道上发送消息h(k),并且In(x)的事实对协议在公共信道上接收消息x进行了建模。

该示例从公钥基础设施（PKI）的模型开始。同样，我们使用事实来存储关于它们的论点所给出的状态的信息。规则有一个前提和一个结论，由箭头符号–>分隔。执行规则要求前提中的所有事实都以当前状态存在，并且由于执行，结论中的事实将添加到状态中，而前提将被删除。现在考虑第一条规则，对公钥的注册进行建模：

1
2
3
4
rule Register_pk:
       [ Fr(~ltk) ]
-->
       [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

这里唯一的前提是Fr事实的一个例子。Fr事实是一个内置事实，表示新生成的名称。此机制用于对随机数（如随机数或密钥）进行建模。

这里面的Fr称为(Facts)，同样是facts的函数有

  • In

这个事实被用来建模一个从 Dolev-Yao 对手控制的不可信网络接收消息的方，该消息只能发生在重写规则的左边。

  • Out

这个事实被用来模拟一方向 Dolev-Yao 对手控制的不可信网络发送消息，并且只能发生在重写规则的右侧。

  • Fr

这个事实必须在生成新鲜(随机)值时使用，并且只能出现在重写规则的左侧，其参数是新鲜项。Tamarin 的底层执行模型有一个用于生成 Fr (x)事实实例的内置规则，并且还确保每个实例生成一个不同于其他所有实例的术语(实例化 x)。

在Tamarin中，变量的种类使用前缀表示：

~x表示x：fresh
$x表示x:pub

%x 表示：nat
#i表示i：temporal
m表示m:msg

此外，字符串常量“c”表示pub中的公共名称，它是一个固定的全局常量。我们有一个顶级排序的msg和两个无与伦比的顶级排序的substart fresh和pub。时态排序的时间点变量是不相连的。

因此我们重新理解上述代码

1
2
3
4
5
6
7
8
9
rule Register_pk: //类似于函数的定义，只不过我们在这地定义一个rule，rule的名称为Register_pk
       [ Fr(~ltk) ] //生成了一个新的名字，Fr()表示生成一个用于秘钥的模块，模块的名字是ltk,~表示新鲜
						        //因此上述语句定义了一个 新鲜的 ltk变量，该变量用于秘钥的一些处理
-->
       [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]
       // !表示有持久性，可以经常随意的使用
       // $A ,XXX 表示代理A与XXX的一个关联 $表示pub公共
       // !Ltk($A, ~ltk) 
       // !Pk($A, pk(~ltk)) 代理A与其公钥pk ( ~ ltk )联系起来。

在本例中，我们允许对手使用以下规则检索任何公钥。从本质上讲，它读取公钥数据库条目，并使用内置的事实Out将公钥发送到网络，这表示向网络发送消息）。

1
2
3
4
rule Get_pk: 
       [ !Pk(A, pubkey) ]
-->
       [ Out(pubkey) ]

我们使用以下规则对长期私钥的动态妥协进行建模。直观上，它读取一个私钥数据库条目并发送给对手。该规则有一个可观测的LtkReveal动作，表示代理A的长期密钥被泄露。行为事实与事实一样，但与其他事实不同的是，行为事实并不以状态出现，而只是在痕迹上出现。在迹上指定安全属性，下面使用动作LtkReveal来确定哪些代理被攻破。该规则现在有了一个前提、结论和箭头内的行动事实：–[ ACTIONFACT ]->:

1
2
3
4
5
6
7
rule Reveal_ltk:

       [ !Ltk(A, ltk) ]

     --[ LtkReveal(A) ]->

       [ Out(ltk) ]

FirstExample.spthy

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

theory FirstExample
begin
builtins: hashing, asymmetric-encryption

// 注册一个公钥
rule Register_pk:
    [ Fr(~ltk) ]
  -->
    [ !Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

rule Get_pk:
    [ !Pk(A, pubkey) ]
  -->
    [ Out(pubkey) ]

rule Reveal_ltk:
    [ !Ltk(A, ltk) ]
  --[ LtkReveal(A) ]->
    [ Out(ltk) ]

.....
end

c 协议建模

回想一下我们想要建模的协议的Alice和Bob表示法：

1
2
C -> S: aenc(k, pkS)
C <- S: h(k)

我们使用以下三条规则对其进行建模。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
//启动一个执行客户端角色的新线程，选择服务器
rule Client_1: 
    [ Fr(~k)       // 选择一个新鲜的秘钥
    , !Pk($S, pkS) // 在服务器上查找公钥
    ] 
--> 
    [ Client_1( $S, ~k )   // 存储线程下一步的服务器和密钥
    , Out( aenc(~k, pkS) ) // 将加密的会话密钥发送到服务器
    ] 
 
rule Client_2: 
    [ Client_1(S, k) // 从上一步检索服务器和会话密钥
    , In( h(k) )     //从网络接收哈希会话密钥
    ]
  --[ SessKeyC( S, k ) ]-> // 声明会话密钥 'k'
    []                     // 已与服务器 'S' 建立。
 
// 服务器线程一步到位地响应来自的会话密钥设置请求
// some client. 
 
rule Serv_1: 
     [ !Ltk($S, ~ltkS) // 查找私钥
     , In( request )   // 收到一个回复
     ] 
   --[ AnswerRequest($S, adec(request, ~ltkS)) ]-> // 下面的解释
     [ Out( h(adec(request, ~ltkS)) ) ] // 返回解密的哈希报文

这里，第一个规则对发送消息的客户端进行建模，而第二个规则对接收响应进行建模。第三条规则对服务器进行建模，在一条规则中接收消息并做出响应。

d 安全属性建模

安全属性是在协议执行的动作事实的跟踪上定义的。

我们有两个属性需要评估。在Tamarin框架中，待评估的性质用引理表示。首先从客户端的角度对会话密钥的保密性进行了研究。引理Client_session_key_secrecy表示，除非对手在服务器S上执行了长期密钥揭示，否则客户端不可能与服务器S建立了会话密钥k，并且对手知道了该密钥k。第二引理Client_auth指定客户端身份验证。这是一种声明，对于客户端已经与服务器S建立的所有会话密钥k，必须有一个服务器已经回答了该请求，或者对手之前已经对S执行了长期密钥揭示。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
lemma Client_session_key_secrecy:
  " /* It cannot be that a  */
    not(
      Ex S k #i #j.
        // 客户端已与服务器 'S' 建立了会话密钥 'k'。
        SessKeyC(S, k) @ #i
        // 并且对手知道 'k' 
      & K(k) @ #j
        // 而没有执行对 'S' 的长期密钥揭示。
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "

lemma Client_auth:
  " // 对于由客户端与服务器 'S' 建立的所有会话密钥 'k' 
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         // 存在一个回答请求的服务器 
       ( (Ex #a. AnswerRequest(S, k) @ a)
         // 或者对手在密钥建立之前执行了对 'S' 的长期密钥揭示。
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

请注意，我们还可以将身份验证属性增强为单射身份验证的一个版本。我们的公式比单射认证的标准公式更强，因为它是基于唯一性而不是计数的。对于大多数保证单射身份验证的协议，也可以证明这种唯一性声明，因为它们在适当的新数据上达成一致。这显示在引理Client_auth_injective中。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
lemma Client_auth_injective:
  " /* For all session keys 'k' setup by clients with a server 'S' */
    ( All S k #i.  SessKeyC(S, k) @ #i
       ==>
         /* there is a server that answered the request */
       ( (Ex #a. AnswerRequest(S, k) @ a
           /* and there is no other client that had the same request */
           & (All #j. SessKeyC(S, k) @ #j ==> #i = #j)
       )
         /* or the adversary performed a long-term key reveal on 'S'
            before the key was setup. */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

为了确保我们的引理不会因为模型不可执行而变得空洞，我们还包括了一个可执行引理，它表明模型可以运行到完成。这是作为一个常规引理给出的，但带有exists_trace关键字，如下面的引理Client_session_key_honest_setup中所示。这个关键字说，如果存在一个公式成立的迹，则引理是真的；这与之前的引理形成了对比，在引理中，我们要求公式在所有轨迹上都成立。当对协议建模时，这种存在性证明是有用的健全性检查。

1
2
3
4
5
6
lemma Client_session_key_honest_setup:
  exists-trace
  " Ex S k #i.
        SessKeyC(S, k) @ #i
      & not(Ex #r. LtkReveal(S) @ r)
  "

3 规则补充（进阶）

a 使用let

当对更复杂的协议建模时，一个术语可能在同一规则中出现多次(可能作为子术语)。为了使这些规范更具可读性，Tamarin 提供了 let… in 的支持，如下例所示:

1
2
3
4
5
6
7
rule MyRuleName:
    let foo1 = h(bar)
        foo2 = <'bars', foo1>
        ...
        var5 = pk(~x)
    in
    [ ... ] --[ ... ]-> [ ... ]

这种 let 绑定表达式可用于在规则的上下文中指定本地术语宏。每个宏应该出现在一个单独的行上，并定义一个替换: = 符号的左边必须是一个变量，而右边是一个任意的项。该规则将在替换出现在 let 中的所有变量的右边之后进行解释。如上面的示例所示，宏可以使用早期定义的宏的左侧。

b 全局宏

有时我们希望在多个规则中使用相同的 let 绑定。在这种情况下，我们可以使用宏关键字来定义全局宏，这将应用于所有规则。考虑下面的例子:

1
macros: macro1(x) = h(x), macro2(x, y) = <x, y>, ..., macro7() = $A

这里的宏1是第一个宏的名称，x 是它的参数。第二个宏称为 Macro2，它有两个参数 x 和 y。最后一个宏宏7没有参数。符号右边的术语是宏的输出。它可以是由方程理论中定义的函数和宏观参数构成的任意项。

要在规则中使用宏，我们可以像在术语中使用函数一样使用宏

1
[ In(macro1(~ltk)) ] --[ ... ]-> [ Out(macro2(pkA, pkB)) ]

和下列语句是通用的

1
[ In(h(~ltk)) ] --[ ... ]-> [ Out(<pkA, pkB>) ]

c Facts

它们用于建模与不可信网络的交互，并建模生成唯一的新鲜(随机)值。

  • In

这个事实被用来建模一个从 Dolev-Yao 对手控制的不可信网络接收消息的方，该消息只能发生在重写规则的左边。

  • Out

这个事实被用来模拟一方向 Dolev-Yao 对手控制的不可信网络发送消息，并且只能发生在重写规则的右侧。

  • Fr

这个事实必须在生成新鲜(随机)值时使用，并且只能出现在重写规则的左侧，其参数是新鲜项。Tamarin 的底层执行模型有一个用于生成 Fr (x)事实实例的内置规则，并且还确保每个实例生成一个不同于其他所有实例的术语(实例化 x)。

d PKI 公开密钥基础设施

在Tamarin模式中，没有预先定义的公开密码匙基础设施(PKI)概念。可以通过一个为一方生成一个密钥的单一规则来为每一方具有非对称密钥的预分布式 PKI 建模。然后，当事方的标识和公钥/私钥作为事实存储在状态中，使协议规则能够检索它们。对于公开密钥，我们通常使用 Pk 事实，而对于相应的长期私人密钥，我们使用 Ltd 事实。由于这些事实只会被其他规则用于检索密钥，而不会被更新，因此我们将它们建模为持久事实。我们使用抽象函数 pk (x)来表示与私钥 x 相对应的公钥，由此得出以下规则。请注意，我们还直接向攻击者提供所有公钥，这些公钥由右侧的 Out 建模。

1
2
3
4
5
6
7
rule Generate_key_pair:
  [ Fr(~x) ]
  -->
  [ !Pk($A,pk(~x))
  , Out(pk(~x))
  , !Ltk($A,~x)
  ]

有些协议，比如 Naxos，依赖于密钥对的代数性质。在许多基于 DH 的协议中，公钥是私钥 x 的 g x，这使得能够利用指数的交换性来建立密钥。在这种情况下，我们改为指定以下规则。

1
2
3
4
5
6
7
rule Generate_DH_key_pair:
  [ Fr(~x) ]
  -->
  [ !Pk($A,'g'^~x)
  , Out('g'^~x)
  , !Ltk($A,~x)
  ]

e 为 Naxos 响应者角色建模

这个协议使用了Diffie-Hellman指数，以及两个散列函数 h1和 h2，我们必须声明这两个函数。我们可以使用以下方法建立模型:

1
builtins: diffie-hellman
1
2
functions: h1/1
functions: h2/1

如果没有进一步的等式，以这种方式声明的函数将表现为一个单向函数。

代理 $R 的响应线程每次接收到消息时，都会生成一个新的值 ~ eskR，发送一条响应消息，并计算一个键 kR。我们可以通过在规则的左边指定一个 In 来对接收消息进行建模。为了对生成的新值进行建模，我们要求它由内置的新值规则生成。

最后，该规则依赖于参与者的长期私钥，我们可以从前面提到的 Generate _ DH _ key _ double 规则生成的持久事实中获得这个长期私钥。

响应消息是 g 的幂等于计算散列函数的幂。由于散列函数是一元的(一元性) ，如果我们想在两条消息的串联上调用它，我们将它们建模为一对 < x，y > ，它将用作 h1的单个参数。

因此，这项规则的初步形式如下:

1
2
3
4
5
6
7
8
9
10
rule NaxosR_attempt1:
        [
          In(X),
          Fr(~eskR),
          !Ltk($R, lkR)
        ]
        -->
        [
          Out( 'g'^h1(< ~eskR, lkR >) )
        ]

然而，响应者也计算一个会话密钥 kR。由于会话密钥不影响已发送或接收的消息，因此可以从规则的左侧和右侧忽略它。但是，稍后我们将要对 security 属性中的会话密钥进行声明。因此，我们将计算键添加到操作中:

1
2
3
4
5
6
7
8
9
10
rule NaxosR_attempt2:
        [
          In(X),
          Fr(~eskR),
          !Ltk($R, lkR)
        ]
        --[ SessionKey($R, kR ) ]->
        [
          Out( 'g'^h1(< ~eskR, lkR >) )
        ]

KR 的计算尚未在上文中指定。我们可以通过完全展开来替换上述规则中的 kR，但这会降低可读性。相反，我们使用 let 绑定来避免重复并减少可能的不匹配。此外，对于密钥计算，我们需要通信合作伙伴 $I 的公钥，我们将其绑定到一个唯一的线程标识符 ~ tid; 我们使用结果操作事实来指定安全属性，我们将在下一节中看到。这导致:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
rule NaxosR_attempt3:
  let
      exR = h1(< ~eskR, lkR >)
      hkr = 'g'^exR
      kR  = h2(< pkI^exR, X^lkR, X^exR, $I, $R >)
  in
   [
       In(X),
       Fr( ~eskR ),
       Fr( ~tid ),
       !Ltk($R, lkR),
       !Pk($I, pkI)
   ]
   --[ SessionKey( ~tid, $R, $I, kR ) ]->
   [
       Out( hkr )
   ]

上述规则准确地建模响应者角色，并计算适当的键。

我们注意到一个进一步的优化，帮助 Tamarin 的向后搜索。在 NaxosR _ trying t3中，规则指定 lkR 可以用任何术语实例化，因此也是非新术语。然而，由于密钥生成规则是唯一生成 LTk 事实的规则，并且它总是使用新的密钥值，因此很明显，在系统的任何可达状态下，lkR 只能由新的值实例化。因此，我们可以将 lkR 标记为某种新鲜的，因此用 ~ lkR.1替换它

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
rule NaxosR:
  let 
      exR = h1(< ~eskR, ~lkR >)
      hkr = 'g'^exR
      kR  = h2(< pkI^exR, X^~lkR, X^exR, $I, $R >)
  in
   [
       In(X),
       Fr( ~eskR ),
       Fr( ~tid ),
       !Ltk($R, ~lkR),
       !Pk($I, pkI)
   ]
   --[ SessionKey( ~tid, $R, $I, kR ) ]->
   [
       Out( hkr )
   ]

f 对 Naxos 启动器角色进行建模

Naxos 协议的发起者角色包括发送消息和等待响应。在发起者等待响应时，其他代理也可能执行步骤。因此，我们使用两个规则来模拟引发剂

第一个规则对启动发起者角色的代理进行建模，生成一个新值，并发送适当的消息。与前面一样，我们使用 let 绑定来简化表示，并使用 ~ lkI 代替 lkI，因为我们知道这一点！有关事实只有以新的价值作为第二个论点才能产生。

1
2
3
4
5
6
7
8
rule NaxosI_1_attempt1:
  let exI = h1(<~eskI, ~lkI >)
      hkI = 'g'^exI
  in
   [   Fr( ~eskI ),
       !Ltk( $I, ~lkI ) ]
   -->
   [   Out( hkI ) ]

注意，状态事实有几个参数: 唯一的线程标识符 ~ tid3、代理标识 $I 和 $R、参与者的长期私有密钥 ~ lkI 和私有指数。现在，这使我们能够指定第二个发起者规则。

1
2
3
4
5
6
7
8
9
10
rule NaxosI_2:
  let
      exI = h1(< ~eskI, ~lkI >)
      kI  = h2(< Y^~lkI, pkR^exI, Y^exI, $I, $R >)
  in
   [   Init_1( ~tid, $I, $R, ~lkI , ~eskI),
       !Pk( $R, pkR ),
       In( Y ) ]
   --[ SessionKey( ~tid, $I, $R, kI ) ]->
  []

第二条规则要求从网络接收消息 Y，并且以前生成了发起者事实。然后，该规则使用这个事实，由于协议中没有进一步的步骤，因此不需要输出类似的事实。由于 Init _ 1事实是用相同的参数实例化的，因此第二步将使用相同的代理标识和在第一步中计算的指数 exI。

因此，完整的例子就是:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
theory Naxos
begin

builtins: diffie-hellman

functions: h1/1
functions: h2/1

rule Generate_DH_key_pair:
  [ Fr(~x) ] 
  --> 
  [ !Pk($A,'g'^~x)
  , Out('g'^~x)
  , !Ltk($A,~x)
  ]

rule NaxosR:
  let 
      exR = h1(< ~eskR, ~lkR >)
      hkr = 'g'^exR
      kR  = h2(< pkI^exR, X^~lkR, X^exR, $I, $R >)
  in
   [
       In(X),
       Fr( ~eskR ),
       Fr( ~tid ),
       !Ltk($R, ~lkR),
       !Pk($I, pkI)
   ]
   --[ SessionKey( ~tid, $R, $I, kR ) ]->
   [
       Out( hkr )
   ]

rule NaxosI_1:
  let exI = h1(<~eskI, ~lkI >)
      hkI = 'g'^exI
  in
   [   Fr( ~eskI ),
       Fr( ~tid ),
       !Ltk( $I, ~lkI ) ]
   -->
   [   Init_1( ~tid, $I, $R, ~lkI, ~eskI ),
       Out( hkI ) ]

rule NaxosI_2:
  let
      exI = h1(< ~eskI, ~lkI >)
      kI  = h2(< Y^~lkI, pkR^exI, Y^exI, $I, $R >)
  in
   [   Init_1( ~tid, $I, $R, ~lkI , ~eskI),
       !Pk( $R, pkR ),
       In( Y ) ]
   --[ SessionKey( ~tid, $I, $R, kI ) ]->
  []

end

4 样例分析2

a 简介

b五个rule

（1）规则 setup 表示在系统的初始设定过程中，会生成一个新的长期密钥~K1 和一个新的公开标识符 ~PID，然后使用这些值来初始化用户设备和基站。 即对应方案中的预认证过程，目的基站将终端匿名身份和安全认证参数 K’ 传给目的基站：

1
2
3
4
rule Setup:
	[Fr(~K1),Fr(~PID)]
	--[Setup()]->
	[!Ltk($UE,~K1),ENB_init($UE,~K1,~PID),UE_init($UE,~K1,~PID)]

（2）规则 Reveal_ltk 表示的是一个密钥泄露事件。其含义为如果用户设备（UE） 的长期密钥（LTK）被泄露了，那么这个密钥就会被输出到环境中。这个 规则是在模拟协议中的安全认证参数 K’泄露事件，用于在后续定义引理 中分析中考虑这种情况对协议安全性的影响：

1
2
3
4
rule Reveal_ltk:
	[!Ltk(UE,xN)]
	--[LtkReveal(UE)]->
	[Out(xN)]

(3)规则 UE1 表示终端发送认证请求的过程：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
rule UE1:
let
		k=h(<~K1>)
		mac=h(<~PID,~T,~K1>)
		mac1=~R1 XOR k
in
		[UE_init($UE,~K1,~PID)
		,Fr(~T)
		,Fr(~R1)
		]
--[SendRequest($UE,mac)]->
[UEstore($UE,~R1,~PID,~K1,k)
,Out(<~PID,mac,~T,mac1>)
]

(4)规则 ENB1 表示目的基站接收到终端的认证请求并进行认证响应过程：

1
2
3
4
5
6
7
8
9
10
11
rule ENB1:
let
	k=h(<~K1>)
	m=k XOR mac1
	mac=h(m)
in
	[ENB_init($UE,~K1,~PID)
	,In(<PID1,mac,T,mac1>)
	]
--[RecvRequest($UE,mac),Eq(h(<~PID,T,~K1>),mac),SendConfirm($UE,mac2)]->
	[Out(<mac2>)]

(5)规则 UE2 表示终端接收目的基站的认证响应过程：

1
2
3
4
5
6
7
8
9
rule UE2:
let
	R0=h(<~R1>)
in 
[UEstore($UE,~R1,~PID,~K1,k)
,In(<mac2>)
]
--[Eq(mac2,R0),RecvConfirm($UE,mac2),SecreMsg(~PID)]->
[]

c 两个约束

在 Tamarin Prover 中，”restriction”用于表达某种全局性的约束或限制。这些约 束在所有可能的执行路径中都必须被满足。此代码中包含两个约束：

(1)约束 Equality 用于在密码学有限域中判断 x 和 y 是否相等：

1
2
3
4
restriction Equality:
"
ALL x y #i. Eq(x,y) @i ==> x=y
"

(2)约束 OneSetup 保证了 Setup() 事件只会发生一次。如果 Setup() 事件在 多个不同的时间点上都发生，那么这些时间点就必须是相等的，也就是说， 他们实际上是同一个时间点：

1
2
3
4
restriction OneSetup:
"
ALL #i #j. Setup() @i & Setup() @j ==> #i=#j
"

d 五个引理

引理（lemma）定义了我们希望在协议中成立的性质或属性。这些性质可能包 括诸如机密性、完整性、认证性等安全属性。引理可以使用多种逻辑量词。在 Tamarin-prover 中，存在性量词 “Ex”，表示存在一个或多个满足某个条件的值（例 如，Ex x. P(x) 表示存在一个 x，使得 P(x) 为真）、 全称量词 “All”表示对所有可 能的值都需要满足某个条件（例如，All x. P(x) 表示对所有可能的 x，P(x) 都必 须为真）、符号”@”表示在一个特定的时间点，每一个操作或事件都会在一个特定 的时间点发生，这个时间点用 @ 来标识（例如，P(x) @ i 表示在时间点 i，P(x) 是真的）、符号”#”表示一个时间点，每一个事件都会在一个时间点发生，这个时 间点由 # 开始的标识符表示（例如，在 #i 和 #j 中，i 和 j 就是两个不同的时 间点）。验证一个引理就意味着检查这个属性是否在所有可能的协议执行路径中都成立。该协议验证主要包含以下五个引理：

（1）引理 ExecutableRequest 和引理 ExecutableConfirm 分别表示存在一种可能 的执行路径，使基站能收到终端发送的认证请求和终端能收到基站的认证 响应：

1
2
3
4
5
6
7
lemma ExecutableRequest:
exists-trace
"Ex UE m #i #j. SendRequest(UE,m)@i & RecvRequest(UE,m)@j"

lemma ExecutableConfirm:
exists-trace
"Ex UE mac #i #j. RecvConfirm(UE,mac)@i & SendConfirm(UE,mac)@j"

(2)引理 ENB_auth_UE 表示当用户设备（UE）接收到一条请求时，这个请求 要么是由真正的用户设备发送的，要么是在安全认证参数 K’被泄露之后 发送的。因 为 基 站 在 执 行 RecvRequest 之前已经执行了 Eq(h(<PID,T,K1>),mac)，即终端发送的消息验证码通过了哈希值验证， 如果安全认证参数 K1（即 K’）没有泄露，则可以认证终端身份：

1
2
3
4
5
6
7
lemma ENB_auth_UE:
"
(ALL UE m #i. RecvRequest(UE,m)@ #i
==>
((Ex #a. SendRequest(UE,m)@ a)
|(Ex #r.LtkReveal(UE) @ r & r <i)))
"

(3)引理 UE_auth_ENB 表示当用户设备（UE）接收到一条确认消息时，这个 确认消息要么是由基站（ENB）发送的，要么是在用户设备的私钥被泄露 之后发送的。因为终端在执行 RecvConfirm 之前已经执行了 Eq(mac2,R0)， 而 R0 又是终端认证请求阶段生成随机数 R1 的哈希值，而在安全认证参数 K1（即 K’）没有泄露的情况下，只有目的基站可以通过 H(K’)⊕R1 进而 解出 R1 的值从而回复正确的 H(R1)，则可以完成对目的基站的认证：

1
2
3
4
5
6
7
lemma UE_auth_ENB:
"(All UE mac #i.RecvConfirm(UE,mac) @ #i
==>
((Ex #a. SendRequest(UE,mac)@ a)
|(Ex #r.LtkReveal(UE) @ r & r <i)))
"

(4)引理 Secrecy_message 表示对于所有的消息 n 和时间点 #i，如果在时间 #i 处，n 被标记为 SecretMsg，在密钥未被泄露的情况下敌手无法获得。 在该方案中表示在安全认证参数 K1 未泄露情况下敌手无法获得随机数 R1：

1
2
3
4
lemma Secrecy_message:
"All n #i.SecretMsg(n) @i==>
(not(Ex #j.K(n)@j))|(Ex ENB #k.LtkReveal(ENB) @k)
"

5 总结

存在性量词 “Ex”，表示存在一个或多个满足某个条件的值（例 如，Ex x. P(x) 表示存在一个 x，使得 P(x) 为真）

全称量词 “All”表示对所有可 能的值都需要满足某个条件（例如，All x. P(x) 表示对所有可能的 x，P(x) 都必 须为真）

符号”@”表示在一个特定的时间点，每一个操作或事件都会在一个特定 的时间点发生，这个时间点用 @ 来标识（例如，P(x) @ i 表示在时间点 i，P(x) 是真的）

符号”#”表示一个时间点，每一个事件都会在一个时间点发生，这个时 间点由 # 开始的标识符表示（例如，在 #i 和 #j 中，i 和 j 就是两个不同的时 间点）。

facts的函数有

  • In

这个事实被用来建模一个从 Dolev-Yao 对手控制的不可信网络接收消息的方，该消息只能发生在重写规则的左边。

  • Out

这个事实被用来模拟一方向 Dolev-Yao 对手控制的不可信网络发送消息，并且只能发生在重写规则的右侧。

  • Fr

这个事实必须在生成新鲜(随机)值时使用，并且只能出现在重写规则的左侧，其参数是新鲜项。Tamarin 的底层执行模型有一个用于生成 Fr (x)事实实例的内置规则，并且还确保每个实例生成一个不同于其他所有实例的术语(实例化 x)。

6 图形化界面

a 命令行运行

直接运行

1
tamarin-prover FirstExample.spthy

Untitled

在这一点上，如果存在任何语法或格式错误（例如，如果相同的事实与不同的参数数量一起使用，则将显示错误），则会显示它们。有关如何处理此类错误的详细信息，请参阅建模问题部分。

b 图形化界面

1
tamarin-prover interactive FirstExample.spthy

Untitled

http://localhost:3001

Untitled

中间的表格显示了所有的理论。你可以点击一个理论来探索它并证明你的安全属性，或者使用底部的上传表单上传更多的理论。请注意，如果您以这种方式使用 GUI 来加载进一步的理论，将不会显示任何警告，因此我们建议从适当的目录中的命令行启动 Tamarin。

如果你点击载入理论表中的“ FirstExample”条目，你应该会看到以下内容:

Untitled

在左边，你可以看到这个理论: 描述对手的消息理论的链接，描述协议的多重重写规则和限制，原始的和精炼的源代码，后面跟着你想要证明的引理。我们将在下面解释其中的每一个。

三、报错解决

1 "tamarin-prover: : commitBuffer: invalid argument (invalid character)

https://blog.csdn.net/qq_43348528/article/details/135696177

输入

1
2
locale
export LANG=en_US.UTF-8

更新于：2024年5月22日

字数：8k 字

时长：32 分钟

协议

评论