tamarin manual总结笔记2（tamarin实例）

最初的例子

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

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。

theory FirstExample
begin

在关键字begin之后，我们首先声明协议使用的加密原语。之后，我们声明对协议建模的多集重写规则，最后我们编写要证明的属性(在Tamarin框架中称为引理)，它指定协议所需的安全属性。请注意，我们还插入了注释来构建理论。

接下来我们将详细解释协议模型。

加密原语

我们在一个安全协议的象征性模型中工作。这意味着我们将消息建模为术语，从满足描述其属性的基本方程理论的函数中构建。

这将在加密消息部分中详细解释。

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

builtins: hashing, asymmetric-encryption

这些内置的函数给了我们以下信息：

• 一元函数h，表示加密散列函数;
• 二元函数aenc，表示非对称加密算法;
• 二元函数adec，表示非对称解密算法;
• 一元函数pk，表示与私钥对应的公钥。

此外，内置还指定使用正确的私钥对密文进行解密将返回初始明文，即adec(aenc(m, pk(sk))， sk)被简化为m

对公钥基础设施进行建模

在Tamarin中，使用多集重写规则对协议及其环境进行建模。规则对系统状态进行操作，系统状态表示为事实的多集(即一个包)。事实可以看作是存储状态信息的谓词。例如，事实Out(h(k))模型表示协议在公共通道上发送消息h(k)，事实In(x)模型表示协议在公共通道上接收消息x。
以PKI (public key infrastructure)模型为例。同样，我们使用事实来存储关于他们的论点给出的状态的信息。规则有一个前提和一个结论，用箭头符号——>分开。执行该规则要求前提中的所有事实都以当前状态存在，并且作为执行的结果，结论中的事实将被添加到状态中，而前提被删除。现在考虑第一条规则，对公钥的注册进行建模:

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

这里唯一的前提是事实的一个实例。Fr事实是一个内置事实，表示新生成的名称。该机制用于对随机数(如随机数或键)进行建模(详细信息请参阅模型规范)
在 Tamarin 中，变量的排序用前缀表示：

• ~x 表示 x:fresh（x是新鲜的）
• $x 表示 x:pub（x是公开的）
• %x 表示 x:nat
• #i 表示 i:temporal（i是暂时的）
• m 表示 m:msg（m表示明文）

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

补：当使用默认的Tamarin设置时，只有一个公共通道对攻击者控制的网络进行建模，即攻击者从Out()事实接收所有消息，并在in()事实中生成协议的输入。如果需要，可以添加私有通道，详细信息请参见通道模型。

因此，上述规则可读作如下。首先，生成一个新名称 ~ltk（排序为 fresh），即新的私钥，并为我们要生成密钥对的代理非确定地选择一个公钥名称 A。然后，生成事实 !Ltk($A，~ltk)（感叹号 ! 表示事实是持久的，即可以任意频繁地使用），表示代理 A 与其私钥 ~ltk 之间的关联，并生成事实！Pk($A, pk(~ltk))，表示代理A与其公钥pk（~ltk）之间的关联。

在本例中，我们允许攻击者使用以下规则检索任何公钥。本质上，它读取一个公钥数据库条目，并使用内置的事实Out将公钥发送到网络，这表示向网络发送消息(有关更多信息，请参阅Model Specification一节)

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

我们使用以下规则对长期私钥的动态妥协进行建模。直观地说，它读取一个私钥数据库条目并将其发送给攻击者。该规则有一个可观察的LtkReveal动作，表明代理A的长期密钥被泄露。行为事实就像事实一样，但与其他事实不同的是，事实不出现在状态中，而只出现在痕迹上。安全属性是在跟踪中指定的，下面使用LtkReveal操作来确定哪些代理受到威胁。这个规则现在在箭头中包含了前提、结论和行动事实。
–[ ACTIONFACT ]->:

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

协议建模

回想一下我们要建模的协议的Alice-and-Bob表示法:

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

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

// Start a new thread executing the client role, choosing the server
// non-deterministically.（启动一个新线程，执行客户端角色，非确定地选择服务器。）
rule Client_1:
    [ Fr(~k)         // choose fresh key（选择新鲜的密钥）
    , !Pk($S, pkS)   // lookup public-key of server（查找服务器的公钥）
    ]
  -->
    [ Client_1( $S, ~k )    // Store server and key for next step of thread（为下一步线程存储服务器和密钥）
    , Out( aenc(~k, pkS) )  // Send the encrypted session key to the server（向服务器发送加密会话密钥）
    ]

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'（说明会话密钥 "k "是与服务器 "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.（返回已解密请求的哈希值）

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

有几种解释是合理的。首先，Tamarin使用c风格的注释，因此/和/之间或//后面的所有内容都是注释。其次，我们使用一个操作记录服务器收到的会话密钥设置请求，以便稍后为客户端形式化身份验证属性。

安全属性建模

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

我们要计算两个性质。在Tamarin框架中，要评估的属性由引理表示。第一个问题是从客户端的角度讨论会话密钥保密的保密性。引理Client_session_key_secrecy表示，除非攻击者在服务器S上执行长期密钥泄露，否则客户机不可能与服务器S建立会话密钥k，而攻击者知道该密钥k。第二个引理Client_auth指定客户端身份验证。这是一种声明，对于客户端与服务器S设置的所有会话密钥k，必须有一个服务器已经响应了请求，或者攻击者之前已经在S上执行了长期密钥泄露。

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' 客户机与服务器'S'设置了会话密钥'k'。*/
        SessKeyC(S, k) @ #i
        /* and the adversary knows 'k' 而对手知道'k'*/
      & K(k) @ #j
        /* without having performed a long-term key reveal on 'S'. 而没有对 "S "进行长期按键揭示。*/
      & not(Ex #r. LtkReveal(S) @ r)
    )
  "

lemma Client_auth:
  " /* For all session keys 'k' setup by clients with a server 'S' 对于客户与服务器 "S "设置的所有会话密钥 "k*/
    ( 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. 或对手在密钥设置之前对'S'进行了长期密钥揭示*/
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

注意，我们还可以将authentication属性增强为一个内射身份验证的版本。

我们的公式比注入认证的标准公式更强，因为它基于唯一性而不是计数。对于大多数保证内射身份验证的协议，也可以证明这种唯一性声明，因为它们同意适当的新数据。这在引理Client_auth_injective中显示。

lemma Client_auth_injective:
  " /* For all session keys 'k' setup by clients with a server 'S'  对于客户与服务器 "S "设置的所有会话密钥 "k*/
    ( 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.或者对手在“S”上进行了长期密钥揭示
在设置密钥之前 */
       | (Ex #r. LtkReveal(S) @ r & r < i)
       )
    )
  "

为了确保我们的引理不会因为模型不可执行而空洞地保持，我们还包括一个可执行引理，表明模型可以运行到完成。

这是一个常规引理，但是使用exists-trace关键字，如下面的引理client_session_key_honest_setup所示。这个关键字表明，如果存在一条迹，该引理为真；这与之前的引理相反，我们要求公式保持所有的迹。在对协议建模时，这种存在性证明是有用的完整性检查。

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

图形用户界面

你现在如何证明你的引理是正确的?如果执行命令行

tamarin-prover interactive FirstExample.spthy

然后，您将在命令行上看到以下输出:

GraphViz tool: 'dot'
 checking version: dot - graphviz version 2.39.20150613.2112 (20150613.2112). OK.
maude tool: 'maude'
 checking version: 2.7. OK.
 checking installation: OK.

The server is starting up on port 3001.
Browse to http://127.0.0.1:3001 once the server is ready.

Loading the security protocol theories './*.spthy' ...
Finished loading theories ... server ready at 

    http://127.0.0.1:3001

21/Jun/2016:09:16:01 +0200 [Info#yesod-core] Application launched @(yesod_83PxojfItaB8w9Rj9nFdZm:Yesod.Core.Dispatch ./Yesod/Core/Dispatch.hs:157:11)

此时，如果存在任何语法或格式良好性错误(例如，如果将相同的事实用不同的方式使用，则会显示错误)，则会显示它们。有关如何处理此类错误的详细信息，请参阅建模问题部分。

然而，在我们的示例中没有这样的错误，因此上面的命令将启动一个web服务器，它将加载FirstExample.spthy所在目录下的所有安全协议理论。将浏览器指向http://localhost:3001

您将看到以下欢迎屏幕:
中间的表格显示了所有加载的理论。你可以点击一个理论来探索它并证明你的安全属性，或者使用底部的上传表单上传更多的理论。请注意，如果您以这种方式使用GUI来加载进一步的理论，则不会显示任何警告，因此我们建议在适当的目录下从命令行启动Tamarin。
如果你点击加载理论表中的“FirstExample”条目，你应该看到以下内容:
在左侧，您可以看到理论:指向描述对手的消息理论的链接，描述您的协议的多集重写规则和限制，以及原始和精炼的源，后面是您想要证明的引理。我们将在下面逐一解释。

在右侧，您可以快速总结可用的命令和键盘快捷键，您可以使用它们在理论中导航。在右上角有一些链接:索引（Index）可以回到欢迎页面，下载（Download）允许您下载当前理论(包括部分证明，如果他们存在的话)，操作（Actions）和子项目（Show source）符号显示源代码显示理论的源代码，选项（Options）允许您配置图形可视化的细节级别(参见下面的示例)。

如果单击左侧的Message theory，应该会看到以下内容:
在右边，您现在可以看到消息理论，从所谓的签名开始，它由所有的函数和方程组成。这些可以是用户定义的，也可以是使用内置的导入，如我们的示例所示。请注意，Tamarin会自动添加一个函数对来创建一对，并将函数fst和snd与两个方程一起使用，以访问一对的第一部分和第二部分。有一种使用<和>的对的简写方式，例如这里使用的是 fst(<x.1,x.2>)。

下面是构造规则。这些规则描述了对手可以应用的功能。例如，考虑以下规则:

rule (modulo AC) ch:
 [ !KU( x ) ] --[ !KU( h(x) ) ]-> [ !KU( h(x) ) ]

直观地说，这条规则表示，如果对手知道x(由前提中的事实!KU(x)表示)，那么他可以计算出h(x)(由结论中的事实!KU(h(x)表示)，即x的哈希值。标签中的行为事实!KU(h(x))也记录了这一点，用于推理。

最后是解构规则。这些规则描述了对手可以通过应用函数从更大的项中提取哪些项。例如考虑以下规则:

rule (modulo AC) dfst:
 [ !KD( <x.1, x.2> ) ] --> [ !KD( x.1 ) ]

简而言之，这条规则是说，如果对手知道一对 <x.1，x.2>（用事实 !KD( <x.1, x.2> ) 表示），那么他就可以从中提取第一个值 x.1（用事实 !KD( x.1 ) 表示）。这是将 fst 应用于数据对，然后使用方程 fst(<x.1, x.2>) = x.1 的结果。!KD( ) 和 !KU( ) 之间的确切区别目前并不重要，下文将对此进行解释。作为第一近似值，两者都代表了对手的知识，区别只是为了让工具的推理更有效率。

现在单击左侧的Multiset重写规则
在屏幕的右侧是协议的重写规则，以及两个额外的规则:isend和irecv2。这两个额外的规则在协议的输出和输入以及对手的推断之间提供了一个接口。规则isend接受一个事实!KU(x)，即攻击者知道的值x，并将其传递给协议输入In(x)。规则irecv接受协议输出Out(x)，并将其传递给对手知识，由!KD(x)事实表示。注意，协议中的规则Serv_1有两个变体(对AC取模)。它的确切含义现在并不重要(它源于Tamarin处理方程的方式)，将在加密消息一节中解释。

现在点击Refined sources(10个案例，解构完成)，可以看到以下内容:
为了提高其内部推理的效率，Tamarin预先计算了案例区分。案例区分给出了一个事实的所有可能来源，即产生这个事实的所有规则(或规则组合)，然后可以在Tamarin的向后搜索中使用。使用这些区分大小写的方法是为了避免重复计算相同的东西。右边是我们的第一个例子理论的预计算结果。

例如，这里Tamarin告诉我们，事实有一个可能的来源!Ltk(t.1, t.2)，即规则Register_pk。该图像显示了表示执行的(不完整的)图表。

绿色的方框代表Register_pk规则的实例，底部的梯形代表Ltk(t.1, t.2)事实的“sink”。这里的案例区分仅由一个规则实例组成，但是可能存在多个规则实例，并且案例区分中存在多个案例，如下图所示。

图像下面给出的技术信息现在不重要，它提供了如何计算情况区分的细节，以及是否有其他约束，如方程或替换，仍然必须解决。
在这里，事实 !KU( ~t.1 ) 有三个来源，第一个是规则 Reveal_ltk，它需要规则 Register_pk 的实例来创建必要的 !Ltk 事实。其他两个来源如下

现在我们将看到如何在交互模式下证明引理。为此，点击左框第一个引理后的sorry(表示还没有开始证明)，得到如下画面:
Tamarin用约束解法证明引理。也就是说，它精炼它所拥有的关于属性和协议的知识(称为约束系统)，直到它可以得出结论，该属性在所有可能的情况下都成立，或者直到它找到引理的反例。

在右边，我们现在在顶部有可能的证明步骤，而约束系统的当前状态就在下面(它是空的，因为我们还没有开始证明)。证明总是从简化步骤(1)开始。简化是将引理转换为需要解决的初始约束系统，或归纳设置步骤(2)。归纳，它生成必要的约束来证明引理，使用对轨迹长度的归纳法。这里我们使用默认策略，即通过单击1来简化步骤。简化后，得到以下画面:
Tamarin现在把这个引理转化成了一个约束系统。由于Tamarin查找引理的反例，因此它查找包含SessKeyC(S, k)和K (k)操作的协议执行，但不使用LtkReveal(S)。如下图所示。
获得SessKeyC(S, k)操作的唯一方法是在左侧使用Client_2规则的实例，而K(k)规则在右侧使用圆框表示(对手推理总是使用圆框进行可视化)。在图的下面是公式

formulas:  #r. (LtkReveal( S ) @ #r)  

现在声明，任何LtkReveal(S)的出现都会导致矛盾。

为了完成证明，我们可以通过选择下一步要解决的约束，或者调用autoprove命令，该命令根据启发式选择下一步。这里我们有两个约束需要解决:Client_1(S, k)和KU(k)，它们都是未完成的当前约束系统中规则的前提。

请注意，GUI中的证明方法是按照autoprove命令使用的启发式排序的。通过始终选择第一个证明方法找到的任何证明都将与autoprove命令构造的证明相同。然而，由于一般问题是不确定的，算法可能不会对每个协议和属性都终止。

在本例中，通过多次单击第一个约束或使用自动证明器，我们都以下面最终状态结束，其中构建的图导致矛盾，因为它包含LtkReveal(S):

这个引理现在用绿色表示，因为它被成功证明了。如果我们找到了一个反例，它就会被涂成红色。你可以用同样的方法证明其他引理。

在命令行上运行Tamarin

调用

tamarin-prover FirstExample.spthy

解析FirstExample.Spthy文件，检查其格式是否正确，并对理论进行漂亮的打印。签名的声明和方程式可以在这个漂亮的印刷理论的顶部找到。

使用自动证明器证明理论中包含的所有引理就像添加标志一样简单——证明调用;也就是说

tamarin-prover FirstExample.spthy --prove

这将首先从约束求解器输出一些日志，然后输出FirstExample安全协议理论，其中包含引理和它们附加的(非)证明

summary of summaries:

analyzed: FirstExample.spthy

  Client_session_key_secrecy (all-traces): verified (5 steps)
  Client_auth (all-traces): verified (11 steps)
  Client_auth_injective (all-traces): verified (15 steps)
  Client_session_key_honest_setup (exists-trace): verified (5 steps)

可以通过具有多个——prove标志并指定一个通用前缀后跟通配符来选择引理，例如，——prove=Client_auth*。注意:在大多数shell中，*需要转义为\*。

警告退出

正如在“图形用户界面”中提到的，在较大的模型中，人们可能会错过格式良好性错误(当编写Tamarin文件时，以及当运行Tamarin证明程序时):在许多情况下，web服务器正常启动，使得很难注意到规则或引理中的某些内容不正确。

为了确保提供的.spthy文件没有任何错误或警告(并在出现错误的情况下停止预处理和其他计算)，在命令行中使用——quit-on-warning标志可能是一个好主意。例如

tamarin-prover interactive FirstExample.spthy --quit-on-warning

这将阻止Tamarin的计算继续进行，并在终端上留下导致Tamarin停止的错误或警告。

完整的示例

/*
Initial Example for the Tamarin Manual
======================================

Authors:    Simon Meier, Benedikt Schmidt
Updated by:     Jannik Dreier, Ralf Sasse
Date:           June 2016

This file is documented in the Tamarin user manual.

*/

theory FirstExample
begin

builtins: hashing, asymmetric-encryption

// Registering a public key
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) ]

// Start a new thread executing the client role, choosing the server
// non-deterministically.
rule Client_1:
    [ Fr(~k)         // choose fresh key
    , !Pk($S, pkS)   // lookup public-key of server
    ]
  -->
    [ Client_1( $S, ~k )    // Store server and key for next step of thread
    , Out( aenc(~k, pkS) )  // Send the encrypted session key to the server
    ]

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