【proverif】proverif的语法-各种密码原语的介绍和具体编码

news2024/11/25 12:38:59

proverif-系列文章目录

  1. 【proverif】proverif的下载安装和初使用
  2. 【proverif】proverif的语法-解决中间人攻击-代码详解
  3. 【proverif】proverif的语法2-各种密码原语的编码 (本文)

文章目录

  • proverif-系列文章目录
  • 前言
  • 铺垫知识
  • 一、对称加密
  • 二、非对称加密
  • 三、Diffie-Hellman密钥协议
  • 四、HASH function
  • 五、数字签名
    • 5.1 带消息恢复的签名
    • 5.2 带消息恢复的概率签名
  • 六、消息验证码(MAC)
  • 总结


前言

在官方文档中,给出了部分密码原语(例如:对称加密、非对称加密等)的详细编码例子,接下来我们可以通过学习官方例子代码,从而进行仿写并编写出自己需要的协议编码。
官网页数很多,而纵观全网关于proverif的相关学习资料很少,这看似是一块很难啃的骨头,但是没关系,再多的讲解资料都不如官方的使用手册来的详细。所以现在我们已经拿到寻宝图的真经,跟着本博客猪一起遨游proverif的知识海。


铺垫知识

  1. 宏机制:包含不止一个构造函数或析构函数应用程序的术语会重复多次。ProVerif提供了一种宏机制,以便定义表示该术语的函数符号并避免重复。
  2. or fail: 每个参数的类型之后,允许用户在某些参数失败的情况下控制函数宏的行为。果存在or fail并且参数失败,则将失败值传递给函数宏,该函数宏可能会捕获它并返回一些非失败结果。
letfun f(x1:t1 [or fail]...,xj:tj [or fail])=M.
  1. 宏机制的应用:非对称加密
type skey.
type pkey.
type coins.
(*格式:fun 函数名(参赛类型):输出参数的类型*)
fun pk(skey):pkey.*公钥生成*)
fun internal_aenc(bitstring,pkey,coins):bitstring. (*加密函数*)

reduc 
	forall m:bitstring,k:skey,r:coins;*参数名:类型*adec(internal_aenc(m,pk(k),r),k)=m. (*析构函数:解密函数*)

(*宏:每次加密时必须重新选择随机硬币r,为了避免在每次加密时都编写这段代码,我们可以定义一个函数宏aenc。*)
letfun aenc(x:bitstring,y:pkey)=new r:coins;intternal_aenc(x,y,r).

好消息:官方手册中明确表明,由于为加密原语定义正确的模型是困难的,我们建议重用现有的定义,例如本手册中给出的定义。
在这里插入图片描述
因此,我将手册中直接给出的密码原语建模列出来,并且我将用图文对相应的加密操作进行原理解释。

一、对称加密

和上一篇proverif语法介绍给出的对称加密不同之处在于,本代码使用了概率生成密钥进而形成加密函数internal_senc() :

type key.
type coins.

fun internal_senc(bitstring,key,coins):bitstring.

reduc 
	forall m:bitstring,k:key;
	sdnc(internal_senc(m,k,r),k)=m.
(*宏:重定义函数。格式:letfun 函数名称(参数名称:类型)=new 参数名称:类型;构造函数(参数名称)*)	
letfun senc(x:bitstring,y:key)=new r:coins;internal_senc(x,y,r).

二、非对称加密

于宏机制的应用中给出的非对称加密编码不同的是,下面的代码使用概率种子seed生成密钥对。

type seed.
type pkey.
type skey.

fun pk(seed):pkey.
fun sk(seed):skey.

fun aenc(bitstring,pkey):bitstring.
reduc
	forall m:bitstring,k:seed; 
	adec(aenc(m,pk(k)),sk(k))=m.

三、Diffie-Hellman密钥协议

在这里插入图片描述
原理:DH算法的基本原理就是通过共享的参数协商一个对称秘钥,然后用这个对称秘钥加密后面的通信。这里用到了离散对数函数,这样即使中间人截获了公钥,也无法计算出各自的私钥。具体的公式如官网描述所示:
在这里插入图片描述
建模代码:

(*声明类型*)
type G.
type exponent. (*指数类型*)
(*定义常量g是G类型的数组*)
const g:G[data].
fun exp(G,exponent):G.(*G的exponent次方*)
equation forall x:exponent,y:exponent;exp(exp(g,x),y)=exp(exp(g,y),x).

四、HASH function

(*Hash func*)
fun h(bitstring):bitstring.

五、数字签名

原理:签名方用自己的私钥签名,验证方用签名方的公钥验证。

在这里插入图片描述
在这里插入图片描述
分两种:

5.1 带消息恢复的签名

(* Digital signatures *)

type sskey.
type spkey.

fun spk(sskey): spkey. (*公钥生成函数*)
fun sign(bitstring, sskey): bitstring. (*私钥签名*)

(*不需要私钥就可以将签名的信息恢复成明文*)
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.

(*通过公钥进行验证sign*)
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.

5.2 带消息恢复的概率签名

(* Digital signatures *)

type sskey.
type spkey.
type scoins.

fun spk(sskey): spkey. (*公钥生成函数*)
fun internal_sign(bitstring, sskey,scoins): bitstring. (*概率性私钥签名*)

(*不需要私钥就可以将签名的信息恢复成明文*)
reduc 
	forall m: bitstring, k: sskey,r:scoins;
	getmess(internal_sign(m,k,r)) = m.

reduc 
	forall m: bitstring, k: sskey,r: scions;
	checksign(internal_sign(m,k,r),spk(k)) = m. (*通过公钥进行验证sign*)
(*宏定义:每次使用签名的时候都要新建一个概率,避免重复编写,使用宏定义。*)
letfun sign(m:bitstring,k:sskey)=new r:scoins;internal_sign(m,k,r).

六、消息验证码(MAC)

工作原理:
消息认证码的输入为任意长度的消息和一个发送者与接收者之间共享的密钥,它可以输出固定长度的数据,这个数据称为MAC 值。

根据任意长度的消息输出固定长度的数据,这一点和单向散列函数很类似。但由于计算 MAC 值必须持有共享密钥,没有共享密钥的人就无法计算 MAC 值,因此消息认证码利用这一性质来完成认证。
此外,消息认证码和单向散列函数一样具有雪崩效应,哪怕消息中发生 1 比特的变化,也会导致 MAC 值发生不可区分的改变。

扩展:基于哈希的消息认证代码(HMAC)
一种消息认证代码,它使用加密哈希函数创建消息的摘要(或“消息认证代码”)。摘要可用于验证消息的真实性。HMAC是一种MAC,除了消息外,还使用密钥来生成摘要。

详细讲解:消息认证码(MAC)_简书

type mkey.
fun mac(bitstring,mkey):bitstring.

总结

提示:这里对文章进行总结:

例如:以上就是今天要讲的内容,本文仅仅简单介绍了pandas的使用,而pandas提供了大量能使我们快速便捷地处理数据的函数和方法。

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.coloradmin.cn/o/1219739.html

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈,一经查实,立即删除!

相关文章

java架构师禁止在项目中使用继承,合理吗?

java架构师禁止在项目中使用继承,合理吗? 如果建议用组合替代继承,非必要不用继承,这个很合理的建议的。 在非必要的情况下不用继承,用组合替代有几个优势:最近很多小伙伴找我,说想要一些 Jav…

音视频转换软件Permute mac中文板特点介绍

Permute mac是一款Mac平台上的媒体格式转换软件,由Chaotic Software开发。它可以帮助用户快速地将各种音频、视频和图像文件转换成所需格式,并提供了一些常用工具以便于用户进行编辑和处理。 Permute mac软件特点 - 支持大量格式:支持几乎所…

【强化学习】时间循环最优决策:原理与Python实战

Python 如何在时间循环里最优决策?时间旅行和平行宇宙时间旅行引发的悖论强化学习策略梯度算法代码案例代码推荐阅读理论完备:实战性强:配套丰富: 如何在时间循环里最优决策? 时间循环是一类热门的影视题材&#xff0…

Unity减少发布打包文件的体积(二)——设置WebGL发布时每张图片的压缩方式

一个项目在发布成WebGL后,其体积至关重要,体积太大,用户加载会经历一个漫长的等待…轻则骂娘,重则用脚把电脑踢烂(扣质保金)… 那么如何减少发布后的体积呢,本文从图片的压缩开始入手。 前传回顾: Unity减…

语雀 P0 事故复盘,这 9 个字亮了!

大家好,我是鱼皮。 最近语雀不是出了个号称 “载入史册” 的 P0 级事故嘛 —— 连续宕机 7 个多小时无法使用,作为一个大厂知名产品,这个修复速度属实让人无法理解。要命的是我们公司的知识库也是放在语雀上的,导致那天下午大家摸…

【C语法学习】26 - strcat()函数

文章目录 1 函数原型2 参数3 返回值4 使用说明5 示例5.1 示例1 1 函数原型 strcat():将src指向的字符串拼接在dest指向的字符串末尾,函数原型如下: char *strcat(char *dest, const char *src);2 参数 strcat()函数有两个参数src和dest&am…

现货黄金休市时间长不长?科普一下交易时间

先告诉你答案,现货黄金市场每天的交易时间很长,因为它全天的盘面是由亚洲、欧洲和北美时间无缝地连接而成,无论投资者身处何方,通过哪里的平台入市,每天基本上都可以享受到连续20多个小时的行情。 只要投资者有足够的精…

如何下载到正确版本的Steam?正确使用实现多开搬砖不被封号

各位游戏玩家们,你们是否也曾因为无法在Steam平台上正常下载游戏而感到烦恼呢?盗版问题已经严重影响了Steam的用户体验,也给玩家们带来了不必要的经济损失。但是,作为玩家,我们需要更多的方法来区分正版和盗版&#xf…

【送书活动】阿里云经历的历史级的大故障,能给我们什么启迪?

作为一个淘系出来的人,参加过声势浩大的S11、S2大促;也和阿里云数据库团队、内核团队等并肩作战过;更是手握过六七百万的预算支持阿里云的服务,更是他们的至尊群用户,得知此次重大故障后,也甚是惊讶。 从阿…

【23真题】难!985难度第一梯队!

今天分享的是23年华南理工大学811的信号与系统试题及解析 本套试卷难度分析:22年华南理工大学811考研真题,我也发布过,若有需要,戳这里自取!本套试题难度中等偏上,只有十道大题,考察大家的综合…

MyBatis整合Spring Boot扫描Mapper相关配置

MyBatis是一款 Java 平台的优秀数据库映射框架,支持 XML 定义或注解,免除了几乎所有的 JDBC 代码以及设置参数和获取结果集的工作。 针对 Spring 提供 Mapper 扫描注解: 集成 Spring Boot 时,可以通过 MapperScan 注解&#xff0…

纯前端模板文件下载如何精确控制下载的文件名字

在写项目的时候,遇到了一个需要把给定的文件放到页面中,然后用户点击下载按钮将这个文件下载下来,我将其存入了云服务之中(这个云服务是不会清空的,内存又不值几个钱),但是当我下载的时候,下载的文件名是存…

Java读取本地文件

import java.io.BufferedReader; import java.io.File; import java.io.FileReader; import java.io.IOException;public class Main {public static void main(String[] args) {String filePath "C:/Users/admin/Desktop/知识点记录.md";// 创建一个文件对象File f…

【MySQL8】1130 - Host *** is not allowed to connect to this MySOL server

问题描述 使用 Navicat 连接 MySQL8 报错: 1130 - Host *** is not allowed to connect to this MySOL server解决方案 use mysql;select host ,user from user; -- 将 root 用户的主机(host)值修改为 %,即允许从任何主机连接 …

navigator.geolocation.getCurrentPosition在谷歌浏览器不执行的问题

/*** 获取我的位置*/getNavigatorLocation: function () {navigator.geolocation.getCurrentPosition(function (success) {console.log(inner>>>, success);if (success && success.coords) {var data success.coords;var point "POINT(" data.…

Web前后端漏洞分析与防御

第1章 课程介绍 试看2 节 | 15分钟 介绍安全问题在web开发中的重要性,并对课程整体进行介绍 收起列表 视频: 1-1 Web安全课程介绍 (09:24) 试看 视频: 1-2 项目总览 (04:47) 第2章 环境搭建2 节 | 26分钟 本章节我们会搭建项目所需要的环境 …

两种常用的找到现货白银目标位的方法

在现货白银交易中,会买的不算厉害,会卖的人才能让利润真正的落袋为安。这里的“买”和“卖”指的不是买入和卖出,而是开仓和平仓。今天我们就来讨论一下,我们怎么样才能懂得“卖”,应该在哪里设置“卖”,也…

freeRTOS--软件定时器

一、什么是定时器: 简单可以理解为闹钟,到达指定一段时间后,就会响铃。STM32 芯片自带硬件定时器,精度较高、达到定时时间后会触发中断,也可以生成 PWM 、输入捕获、输出比较,等等,功能强大&am…

STM32GPIO——上拉下拉电阻、施密特触发器、P-MOS/N-MOS管

图1和图2 两种版本的GPIO基本结构图 如上两个图所示,标号2都为上拉、下拉电阻部分,阻值约为30k~50k欧,通过对应开关进行控制,开关由寄存器控制。 当引脚外部的器件没有干扰引脚的电压时,即没有外部的上、下拉电压&a…