本文主要是介绍tamarin manual总结笔记1（安装），希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！
Tamarin power 是一种功能强大的工具，用于对安全协议进行符号建模和分析。
安装
在macOS或Linux上安装
在 macOS 或 Linux 上安装 Tamarin 的最简单方法是使用 Homebrew：
brew install tamarin-prover/tap/tamarin-prover
它单独打包用于
Arch Linux：pacman -S tamarin-prover
NIxpkgs:nix-env -i tamarin-prover
NixOS:将tamarin-prover添加到你的environment.systemPackages中。
或者也可以直接从GitHub下载二进制文件，然后自己动手安装依赖项，或从源代码编译
Windows 10安装
您可以使用 Windows Subsystem for Linux（WSL）在 Windows 10 下安装 Tamarin（带图形用户界面）。出于性能和兼容性考虑，我们建议使用 WSL2 和 Ubuntu。安装好 WSL 和 Ubuntu 后，启动 Ubuntu 应用程序，按照上述 Linux 安装说明安装 Tamarin。然后就可以在 Ubuntu 应用程序中使用常规命令运行 Tamarin。要使用交互式模式，请在应用程序内启动 Tamarin，并将常用的 Windows 浏览器连接到 http://127.0.0.1:3001。在 Ubuntu 应用程序中，您可以通过 /mnt/c 访问 Windows 文件。
从源代码编译
您不需要从源代码编译Tamarin，除非您正在为它开发一个新特性或者您想要使用一个未发布的特性。但是，如果你想从源代码安装它:
手动安装依赖项
Tamarin需要Haskell Stack来构建，GraphViz和Maude 2.7.1(或更新版本)才能运行。安装这些最简单的方法是
brew install tamarin-prover/tap/maude graphviz haskell-stack
或者，你也可以直接安装
- Haskell Stack遵循Stack的安装页面给出的说明。如果你在软件包管理器中安装stack(特别是在Ubuntu上)，你必须在之后运行stack升级，因为那个版本的stack通常是过时的。
- Graphviz Graphviz应该使用您的标准包管理器，或直接从http://www.graphviz.org/获取
- Maude您可以使用您的包管理器安装Maude。但是，如果您的包管理器安装了Maude 2.6，那么您必须直接从http://maude.cs.illinois.edu/安装2.7.1版本，Core Maude 2.7.1。在这种情况下，您应该确保您的PATH包含安装路径，以便调用maude时启动2.7.1版本。注意，尽管Maude可执行文件是可移动的，但prelude.maude文件必须在启动maude的同一文件夹中。
编译
查看源代码
git clone https://github.com/tamarin-prover/tamarin-prover.git
您已经为编译准备好了当前的开发版本。如果你想使用主版本，只需运行git checkout master。
在任何一种情况下，你都可以在新目录下运行make default，它将为你的系统安装一个适当的GHC(格拉斯哥Haskell编译器)，包括所有依赖项。tamarin-prover可执行文件将被复制到**~/.local/bin/tamarin-prover**。注意，这个过程需要30到60分钟，因为所有依赖项(大约120分钟)都是从头编译的。
在远程机器上运行Tamarin
如果您有更快的桌面或服务器，但更喜欢在笔记本电脑上使用Tamarin，您可以这样做。然后，该工具的cpu/内存密集型推理部分将在更快的机器上运行，而您只需在本地运行GUI，即您选择的web浏览器。为此，使用以下命令将端口3001转发到服务器的端口3001，并适当地替换SERVERNAME。
ssh -L 3001:localhost:3001 SERVERNAME
如果您这样做，我们建议您在屏幕环境中的服务器上运行Tamarin实例，即使网络断开了您的连接，它也将继续运行，因为您可以稍后重新连接到它。否则，任何网络故障都可能要求您重新启动Tamarin并重新开始验证。
Tamarin代码编译器
在Tamarin Prover项目的etc文件夹下，可以使用VIM、Sublime Text 3、Emacs和notepad++的插件。下面我们详细介绍安装首选插件所需的步骤
VIM
使用Vim插件管理器，本例将使用Vundle直接从这个存储库安装插件。下面的说明应该可以翻译成其他插件管理器
- 确保你已经安装了Vundle(或者你喜欢的插件管理器)。
- 在.vimrc中放入以下指令或同等指令:
Plugin 'tamarin-prover/editors'
- 重新启动Vim或重新加载配置。
- 运行Vim命令:PluginInstall(或同等功能)
手动安装(不推荐)如果使用这种方法安装Vim支持文件，您需要自己保持文件的最新状态
- 创建~ /. 目录，是$VIMRUNTIME 2的典型位置。
- 将etc/vim目录的内容拷贝到~/.Vim/，包括文件夹
Sublime text3editor- Sublime是为Sublime text3编辑器开发的插件。该插件具有以下功能：-基本语法-理论，规则，限制和引理的片段
editor-sublime 有两种安装方式：
第一种也是首选的方法是使用 PackageControl.io。现在可以通过 sublime 软件包管理器安装 editor-sublime。请参阅安装和使用文档，然后搜索并安装 TamarinProver
或者，它也可以从源代码安装。对于Linux / macOS，可以遵循此过程。我们假设您已经安装了git工具。
- 将目录更改为Sublime Text packages目录:
macOS: cd ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/
Linux: cd ~/.config/sublime-text-3/Packages/
- 将该目录克隆到Packages文件夹中
SSH: git clone git.com:tamarin-prover/editor-sublime.gitHTTPS: git clone https://github.com/tamarin-prover/editor-sublime.git
- 关闭并重新打开Sublime，在右下方的语法列表中应该有“Tamarin”。
请注意，这个插件正在积极开发中，因此，一些功能仍然以原型的方式实现。如果您遇到任何问题或对运行插件的任何部分有任何疑问，请访问项目GitHub页面.
Notepad++
使用notepad_plus_plus_spthy.xml文件遵循notepad++ Wiki中的步骤。
Emacs
spthy.el实现了SPTHY主模式。您可以使用M-x load-file加载它，或者以您喜欢的方式将它添加到.emacs中
Atom
language-tamarin包为Atom提供Tamarin语法高亮显示。要安装它，请运行apm install language-tamarin
FAQ
如何使用自制软件卸载Tamarin ?要卸载(并“untap”Tamarin自制程序):
brew uninstall tamarin-prover
brew untap tamarin-prover/tap
这个homebrew-science tap是怎么回事？
Tamarin 以前是在现已关闭的homebrew-science tap（homebrew-science tap）中发布的。如果你已经通过 Homebrew 安装了它，可能需要先卸载并取消该版本：
• brew uninstall tamarin-prover
• brew untap homebrew/science
更新/拉动/释放后，Tamarin 不再编译。尝试运行堆栈升级和堆栈更新。过期的堆栈版本可能导致虚假的编译错误。
这篇关于tamarin manual总结笔记1（安装）的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！
