tamarin manual总结笔记1(安装)

2023-12-20 16:52

本文主要是介绍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支持文件,您需要自己保持文件的最新状态

  1. 创建~ /. 目录,是$VIMRUNTIME 2的典型位置。
  2. 将etc/vim目录的内容拷贝到~/.Vim/,包括文件夹

Sublime text3editor- Sublime是为Sublime text3编辑器开发的插件。该插件具有以下功能:-基本语法-理论,规则,限制和引理的片段
editor-sublime 有两种安装方式:
第一种也是首选的方法是使用 PackageControl.io。现在可以通过 sublime 软件包管理器安装 editor-sublime。请参阅安装和使用文档,然后搜索并安装 TamarinProver
或者,它也可以从源代码安装。对于Linux / macOS,可以遵循此过程。我们假设您已经安装了git工具。

  1. 将目录更改为Sublime Text packages目录:
macOS: cd ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/
Linux: cd ~/.config/sublime-text-3/Packages/
  1. 将该目录克隆到Packages文件夹中
 SSH: git clone git.com:tamarin-prover/editor-sublime.gitHTTPS: git clone https://github.com/tamarin-prover/editor-sublime.git
  1. 关闭并重新打开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(安装)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/516753

相关文章

Python中win32包的安装及常见用途介绍

《Python中win32包的安装及常见用途介绍》在Windows环境下,PythonWin32模块通常随Python安装包一起安装,:本文主要介绍Python中win32包的安装及常见用途的相关... 目录前言主要组件安装方法常见用途1. 操作Windows注册表2. 操作Windows服务3. 窗口操作

JavaSE正则表达式用法总结大全

《JavaSE正则表达式用法总结大全》正则表达式就是由一些特定的字符组成,代表的是一个规则,:本文主要介绍JavaSE正则表达式用法的相关资料,文中通过代码介绍的非常详细,需要的朋友可以参考下... 目录常用的正则表达式匹配符正则表China编程达式常用的类Pattern类Matcher类PatternSynta

gitlab安装及邮箱配置和常用使用方式

《gitlab安装及邮箱配置和常用使用方式》:本文主要介绍gitlab安装及邮箱配置和常用使用方式,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录1.安装GitLab2.配置GitLab邮件服务3.GitLab的账号注册邮箱验证及其分组4.gitlab分支和标签的

MySQL MCP 服务器安装配置最佳实践

《MySQLMCP服务器安装配置最佳实践》本文介绍MySQLMCP服务器的安装配置方法,本文结合实例代码给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,需要的朋友参考下... 目录mysql MCP 服务器安装配置指南简介功能特点安装方法数据库配置使用MCP Inspector进行调试开发指

在Windows上使用qemu安装ubuntu24.04服务器的详细指南

《在Windows上使用qemu安装ubuntu24.04服务器的详细指南》本文介绍了在Windows上使用QEMU安装Ubuntu24.04的全流程:安装QEMU、准备ISO镜像、创建虚拟磁盘、配置... 目录1. 安装QEMU环境2. 准备Ubuntu 24.04镜像3. 启动QEMU安装Ubuntu4

Python UV安装、升级、卸载详细步骤记录

《PythonUV安装、升级、卸载详细步骤记录》:本文主要介绍PythonUV安装、升级、卸载的详细步骤,uv是Astral推出的下一代Python包与项目管理器,主打单一可执行文件、极致性能... 目录安装检查升级设置自动补全卸载UV 命令总结 官方文档详见:https://docs.astral.sh/

Nexus安装和启动的实现教程

《Nexus安装和启动的实现教程》:本文主要介绍Nexus安装和启动的实现教程,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一、Nexus下载二、Nexus安装和启动三、关闭Nexus总结一、Nexus下载官方下载链接:DownloadWindows系统根

SQL中JOIN操作的条件使用总结与实践

《SQL中JOIN操作的条件使用总结与实践》在SQL查询中,JOIN操作是多表关联的核心工具,本文将从原理,场景和最佳实践三个方面总结JOIN条件的使用规则,希望可以帮助开发者精准控制查询逻辑... 目录一、ON与WHERE的本质区别二、场景化条件使用规则三、最佳实践建议1.优先使用ON条件2.WHERE用

Java SWT库详解与安装指南(最新推荐)

《JavaSWT库详解与安装指南(最新推荐)》:本文主要介绍JavaSWT库详解与安装指南,在本章中,我们介绍了如何下载、安装SWTJAR包,并详述了在Eclipse以及命令行环境中配置Java... 目录1. Java SWT类库概述2. SWT与AWT和Swing的区别2.1 历史背景与设计理念2.1.

安装centos8设置基础软件仓库时出错的解决方案

《安装centos8设置基础软件仓库时出错的解决方案》:本文主要介绍安装centos8设置基础软件仓库时出错的解决方案,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐... 目录安装Centos8设置基础软件仓库时出错版本 8版本 8.2.200android4版本 javas