Z语言学习——基于通讯案例

news2024/10/16 16:31:28

目录

1数据类型

2初始状态

3 Alice的消息发送

4 Bob接收与发送消息

5 Alice接收消息

6消息的增删改查

6.1 删除消息

6.2查询消息

6.3修改/增加消息

7定理证明——重要目的

案例背景:

(1)构建一个交互式的通讯方案;

(2)攻击者控制了所有的通讯信道,可以修改、拦截、转发信息;

(3)诚实主体为了保护个人隐私,所有信息加密;

(4)信息项可以增加、删除、查询、修改。

1数据类型

(1)基于非对称密码保护方案;

(2)包含了各种错误信息和消息项操作信息;

[Messages]

定义一个消息类型。

Agents ::= Alice | Bob | Evil

三个主体, Evil是攻击者

Keys ::= Alice_PK| Bob_PK| Evil_PK | Alice_SK | Bob_SK | Evil_SK | NULL

Alice_PK表示Alice有个公钥,Alice_SK表示Alice有个私钥,NULL表示消息可以明文传送。

Result ::= OK | NoSuchltem

传输结果,操作成功OK,某个消息不存在NoSuchltem

Command := Add | Del |  Query |  Modi

额外的选项,交易项的操作信息:增删改查

Check _M: Agents × Agents × Command × Messages × Keys

→Command × Messages × Keys

额外定义了一个函数,函数的输入是一个五元组(Agents × Agents X Command × Messages × Keys),函数的输出是一个命令,消息,和对应的一个密钥(Command × Messages × Keys

)。

Check_M=O

初始化:是初始化函数,因为所有的都是集合,所以要有初始值。

2初始状态

Evil_Agent攻击者的状态

Adversary_Knowledge:P(Agents × Agents × Command × Messages × Keys)

攻击者的知识集,给他刻画了某一种数据类型,P表示由集合(Agents × Agents × Command × Messages × Keys)产生的密集。

Adversary_Init: Keys→ Agents

输入的Keys,对应的是一个实体,因为函数是多对一的,一个实体可以拥有多个密钥,

Acversary_Init = {(Alice_PK,Alice),(Bob_PK,Bob).(Evil_PK,Evil).(Evil_SK,Evil)}

对于攻击者而言,有3个公钥PK,1个私钥SK。

Alice_Agent

Alice_Knowledge: P Messages

Alice_Init: Keys →Agents

Alice_Init = {(Alice_PK,Alice),(Bob_PK, Bob), (Evil_PK,Evil), (Alice_SK,Alice) }

Alice_Knowledge  = ∅

Bob_Agent(与Alice类似)

Bob_Knowledge: P Messages

Bob_Init: Keys → Agents

Bob_Init = {(Alice_PK,Alice).(Bob_PK. Bob),(Evil_PK.Evil),(Bob_SK,Bob)}

Bob_Knowledge = ∅

Init

Alice_Agent'

Bob_Agent'

Evil_Agent'

Adversary_Knowledge'=∅

得到初始状态,初始状态Alice与Bob之间没有任何消息的传递(Alice_Knowledge  = ∅

,Bob_Knowledge = ∅),所以攻击者得不到任何信息,因此攻击者的知识集目前也是空的(Adversary_Knowledge'=∅)。

注意:Z规格中每一个schema本质上是由多个集合组成,每个集合上必须严格定义数据类型,因此Z规格是一种类型化系统;另外,对数据的操作则构成了多个命题。命题用于说明系统状态,后续将说明前件和后件的使用。

3 Alice的消息发送

Alice_send_Ml

Na: Messages

Na是一个随机数,定义为一个消息

M1!: Agents ×  Agents × Command × Messages ×  Keys

输出是M1

△Alice_Agent

△Evil_Agent

这里△表示如果Alice发送消息M1的话(Alice_send_Ml),会引起Alice_Agent和Evil_Agent的状态变化。

Na ∉ Alice_Knowledge

做一个判断,要发送的随机数Na不能属于Alice已有的知识集

Alice_Knowledge'= Alice_Knowledge ∪ {Na}

更新Alice知识集,增加Na

M1! = (Alice, Bob,Add,Na,Bob_PK)

输出M1用固定的表示(Alice, Bob,Add,Na,Bob_PK)

Adversary_Knowledge'= Adversary_Knowledge ∪  {M1!}

输出以后,攻击者会在知识集中增加M1的信息

4 Bob接收与发送消息

Bob receive Ml _send_M2

Bob收到M1同时发送M2

M1?: Agents × Agents × Command × Messages × Keys

?表示输入

M2!: Agents ×Agents × Command × Messages × Keys

!表示输出

Na,Nb: Messages

△Bob_Agent

△Evil_Agent

M1? ∈ dom Check_M

要检查一下M1是否属于Check_M函数的一个定义,属于证明才能通过。

(Bob_SK,Bob) ∈ Bob_Init

Bob要解密M1,所以需要一个私钥Bob_SK。

Check_M M1? =(Add,Na,Bob_PK)

利用函数Check_M判断M1,输入?是M1,输出是产出的结果判断,增加Add一个消息Na.

Bob_Knowledge'= Bob_Knowledge ∪ {Na,Nb}

接受方Bob知识集增加两个,Na 是Bob从密文中提取的,Nb是Bob自己产生的。

M2!=(Bob,Alice,Add,Nb,Alice_PK)

Adversary_Knowledge'= Adversary_Knowledge ∪ {M24}

5 Alice接收消息

大同小异了

6消息的增删改查

6.1 删除消息

Alice_And_Bob_Del

M?: Agents×Agents × Conmcd × Messcges ×Keys

reply!: Result

状态的反馈

X: Messcges

△Alice_Agent

△Bob_Agent

要求同时更新Alice和Bob两个实体状态。

M? ∈ dom Check_M

 Check_M M?=(Del,X,NULL)

逻辑与符号:可以省略,因为在Z规格中,每一行后面都会隐含一个and。这里只是为了增加可读性。

 X∈ Bob_Knowledge

 X∈Alice_Knowleclge

增加了额外的操作条件,此时前提条件有四个:判断M?属于Check_M定义域、M?中是否包含Del指令、消息X是否属于Alice知识集、消息X是否属于Bob知识集。

Alice_Knowledge'= Alice_Knowledge \ {X}

Bob_Knowledge'= Bob_Knowlecge \ {X}

上面的\就表示删除X

reply! = OK

 reply! = NoSuchItem

逻辑或符号

要写,表示产生了一个错误,当M不属于Check_M函数的定义,就返回没有信息项NoSuchItem

注意:Z规格中,系统的模型通常体现为一个LTS,即标签化的可变迁状态机。每一个状态的变迁有前提条件和后续条件。但是,Z规格的schema中并没有显示地说明哪些是前提条件,哪些是后续条件,需要用户自己甄别。

6.2查询消息

Alice_Or_Bob_Query

M?: Agents × Agents × Commcmnd × Messages × Keys

X: Messcges

resp!: Messcges

reply!: Result

ΞAlice_Agent

ΞBob_Agent

希腊字符Ξ:表示Alice和Bob的状态不会有任何的更改。仅仅是对消息的查询。

M?∈ dom Check_M

 Check_M M?=(Query,X,NULL)

判断M?是否属于Check_M定义域、M?中是否包含Query指令

X∈Alice_KnowledgeX∈ Bob_Knowledge

reply! = OK

resp!=X reply!= NoSuchItem

输出X,或如果输入不在Check_M函数中,输出没有的消息NoSuchItem

6.3修改/增加消息

Alice_Or_Bob_Modify

M_New? : Messciges

M_Old? : Agents × Agents  ×Conmand × Messcges × Keys

对于修改消息,输入有两个,新旧消息项

X: Messages

reply!: Result

△Alice_Agent

△Bob_Agent

M_Old? ∈ dom Check_M Check_M M_Old? =(Modi,X,NULLL)

判断旧消息项是否属于函数定义域,同时输出密文能把X找到。

X∈ Alice_Knowledge

X∈ Bob_Knowlecge

Alice_Knowledge'= Alice_Knowledge \ {X}∪{M_New?}

Bob_Knowleclge'= Bob_Knowledge \ {X}∪{M_New?}

reply! = OK reply! = NoStuchItem

7定理证明——重要目的

第一列Y表示没有语法错误,第二列Y表示没有逻辑错误。

重要目的:证明系统的安全性,或某些功能是否达到要求。

(1)初始状态中是否能够蕴含这三种实体

(2)Alice收到消息M2,是否从上面的系统中蕴含着Alice一定发送了消息M1

(3)Alice是否正确的得到了随机数Na和Nb,如果Alice收到M2,能否推出:

1)Na和Nb属于Alice知识集,2)Alice发送M1,3)Bob收到M1并发送M2

————————后面会学习软件Z-EVES:

Z-EVES 是专门为 Z 规范设计的,这使得它在处理 Z 语言时比一般的定理证明器更高效和精确。例如,支持 Z 规范的语法和语义检查。与其他形式化验证工具相比,Z-EVES 在处理 Z 语言时具有独特的优势和高效性。

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

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

相关文章

计算机编码以及URL转码

目录 一、计算机编码 1.ASCII编码 2. GB2312编码 3.GBK编码 4.UTF-8编码 二、URL转码 1.encodeURI和decodeURI 2.encodeURIComponent 和 decodeURIComponent 三、Base64 一、计算机编码 在计算机中,所有的数据在存储和运算时都要使用二进制数表示&#xf…

开源驰骋低代码-积极拥抱AI时代

开源驰骋AI低代码-积极拥抱AI时代 驰骋AI代码开发平台ccfast通过集成人工智能技术,为开发者提供了一系列强大的辅助功能,极大地提升了开发效率和流程体验。以下是针对您列出的功能的详细解释: 概要说明 驰骋低代码开发平台是一款基于云计算和…

【人工智能,机器学习,统计学习,科学表征】开源商用与研发合作

个体工户linjing-lab托管在Github,现公开招募商用与合作人员,目标人群分为以下几个方向: 数学、信息科学、计算机专业的大学高年级学生,熟悉C和面向对象模型,擅长Pybind11编译算子到Python环境。26岁以下的大学本科毕…

Java学习 (四) 面向对象--类与方法

关于面向对象的知识点 1、 java类 以及类成员 属性 方法 构造器 代码块 内部类 2、面向对象特征 封装 继承 多态 3、 其他关键字使用 this \ super \ package \ import \static \ final\ interface\ abstract …

北方高温来袭!动力煤却不涨反跌的原因分析

内容提要 北方高温而南方降雨偏多的格局或将继续,整体水力发电量增长可能继续明显增长,但火电增幅可能继续缩小。5月重点火电厂的发电量和耗煤量增速均呈现负增长,耗煤量月度同比下降7%,而重点水电同比大增近40%。我国电力行业绿…

Apple Phone Memory

Apple Phone Memory 苹果手机内存查询,哪些应用程序(app)占用内存: 设置 通用 iPhone储存空间 清理下QQ音乐:

灵感互娱U3D笔试题

文章目录 题目1解析 题目2解析 题目3解析 题目4数组链表 题目5解析 题目6解析 题目7解析题目8解析 后话 题目1 以下C#代码的输出顺序是什么 namespace ConsoleApp2 {internal class Program{class A{ public A(string text){Console.WriteLine(text);}}class B{static A a1 …

同城跑腿多合一系统源码小程序支持安卓+IOS+公众号+H5

🚀 同城跑腿多合一小程序:便捷生活新选择 💨 一、引言:走进便捷新纪元 在这个快节奏的现代生活中,时间成了最宝贵的财富。而“同城跑腿多合一小程序”正是为了满足大家对于便捷、高效生活的追求而诞生的。它不仅是一款…

高效设计必选!5款好用的UI动效工具

UI 动态设计是应用程序设计的重要组成部分。随着技术的积累,UI设计中的动态效果遍地开花,UI动态效果可以使我们的页面更时尚、更有趣、更人性化。5G网络的快速发展也使美丽的动态效果几乎无缝地嵌入到UI界面中。今天,毫不夸张地说&#xff0c…

豆瓣电影top250网页爬虫

设计思路 选择技术栈:确定使用Python及其相关库,如requests用于发送网络请求,获取网址,用re(正则表达式)或BeautifulSoup用于页面内容解析。设计流程:规划爬虫的基本流程,包括发起请求、接受响应、解析内容、存储数据等环节。模块…

CCF推荐会议必投攻略:这些顶级会议投完直通录取大门

CCF推荐会议必投攻略:这些顶级会议投完直通录取大门! 会议之眼 快讯 CCF介绍 CCF(China Computer Federation)即中国计算机学会,前身是中国电子学会计算机专业委员会,成立于1962年。这是由从事计算机及相…

容器基本概念_从虚拟化技术_到容器化技术_开通青云服务器_并远程连接_容器安装---分布式云原生部署架构搭建007

这一部分,属于以前都会用到的,会快速过一遍,对于关键技术问题会加以说明 https://www.yuque.com/leifengyang/oncloud文档地址在这里,可以看,有些命令可以复制使用 可以看到容器的出现就是 目的就是,让你做的所有的软件,都可以一键部署启动 打包就是docker build 然后: 对于…

Github生成Personal access tokens及在git中使用

目录 生成Token 使用Token-手工修改 使用Token-自动 生成Token 登录GitHub,在GitHub右上角点击个人资料头像,点击Settings → Developer Settings → Personal access tokens (classic)。 在界面上选择点击【Generate new token】,填写如…

ctfshow web七夕杯

web签到 执行命令没有回显&#xff0c;我们直接写文件就可以了 有字符长度限制 ls />a nl /*>a访问url/api/a下载文件 easy_calc <?phpif(check($code)){eval($result."$code".";");echo($result); }function check(&$code){$num1…

Python-gui开发之Pycharm+pyside6/Pyqt6环境搭建

Python-gui开发之Pycharm+pyside6/Pyqt6环境搭建 软件版本一、软件安装1、Python安装2、Pycharm安装3、pyside6或pyqt6安装①安装pyside6②安装PyQt6和pyqt6-tools二、Pycharm项目配置1、插件安装2、新建项目以及环境配置3、包管理安装三、在Pycharm中配置PySide61、pyside6 Qt…

Redis持久化主从哨兵分片集群

文章目录 1. 单点Redis的问题数据丢失问题并发能力问题故障恢复问题存储能力问题 2. Redis持久化 -> 数据丢失问题RDB持久化linux单机安装Redis步骤RDB持久化与恢复示例RDB机制RDB配置示例RDB的fork原理总结 AOF持久化AOF配置示例AOF文件重写RDB与AOF对比 3. Redis主从 ->…

C/C++ struct stat介绍

目录 前言 struct stat struct stat 使用 参考 共勉 前言 本文详细介绍了stat结构体的成员变量&#xff0c;以及使用案例&#xff0c;希望能够帮到您。 struct stat struct stat 结构体用于表示文件或者文件系统对象信息的一种结构体的声明&#xff0c;通常在POSIX&#x…

Gobject tutorial 八

The GObject base class Object memory management Gobject的内存管理相关的API很复杂&#xff0c;但其目标是提供一个基于引用计数的灵活的内存管理模式。 下面我们来介绍一下&#xff0c;与管理引用计数相关的函数。 Reference Count 函数g_object_ref和g_object_unref的…

基于JSP的个人交友网站系统

开头语&#xff1a; 你好&#xff0c;我是计算机学长猫哥。在这个信息时代&#xff0c;个人交友网站为我们提供了一个便捷的社交平台。如果你对本系统感兴趣或有更多需求&#xff0c;欢迎联系我。 开发语言&#xff1a;Java 数据库&#xff1a;MySQL 技术&#xff1a;JSP技…

多线程(Lock锁,死锁,等待唤醒机制,阻塞队列,线程池)

Lock锁 虽然我们可以理解同步代码块和同步方法的锁对象问题但是我们并没有直接看到在哪里加上了锁&#xff0c;在哪里释放了锁为了更清晰的表达如何加锁和释放锁&#xff0c;JDK5以后提供了一个新的锁对象Lock Lock实现提供比使用synchronized方法和语句可以获得更广泛的锁定操…