(补充)SPAN+AVISPA for Verifying Cryptographic Protocols
本文是对视频教程的重学习。整理自己的理解。
入侵者(I)先验知识:
{A,B,Ka,Kb,Ki,Ki-1}
I 能 获取每次信息传递的全部内容。(能不能推导出来看设计的如何了)
达到的目标:
1.信息的机密性。公钥加密,私钥解密 保证信息的机密性。
2.认证
消息认证:如果A知道是谁创建的消息m,则称A能认证m。电子签名:私钥加密、公钥解密。(ID,{ID}K-1) 比较ID是否一样。
agent认证:如果一次成功的协议会话后,A知道他和B在通过协议交互。则代理A能认证代理B
3.freshness:在协议会话期间message是新鲜的
协议解读(实现B给A传消息)
protocol 0
B -> A : B,s
显然,入侵者,能够容易的得到s
protocol 1
B -> A : {B,s}Ka
Ka是公钥,I 能够伪装成B
protocol 2
B -> A : B,{s}Kb-1
达成:消息认证
但 I 知道B的公钥,可以推导出s
protocol 3
B -> A : {B,s,{s}Kb-1}Ka
达成:信息的机密性;消息认证
但是没有freshness
I 能获得{B,s,{s}Kb-1}Ka 全部信息,等2000年后再发给A
agent 认证 未达成
protocol 4
Na :fresh number
- A -> B : {A,B,Na}Kb
- B -> A : {A,B,Na,s}Ka
达成:信息的机密性、新鲜性、A知道s是B建立的(Na只有B的私钥能推导出来)、会话成功后A认证B。
protocol 5(使用对称密钥)
- A -> B : {A,B,Na}Kab
- B -> A : {A,B,Na,s}Kab
DY模型:
- 加密是安全的
- 入侵者有对整个网络的控制权
安全目标属性:
可参考文章:形式化分析工具AVISPA(三)学习User micro-manual of AVISPA 1.5 声明安全属性
secret(information,identifier,agents-set)
witness(X,Y,identifier,information)
request(Y,X,identifier,information)
secret()infor 是 agents 保密的信息 标签为identifier
wrequest() Y想验证 infor 是X构建的,标签为identifier
witness() X希望infor能够被认证
参考:
设计一个交换协议
A----------------------------T----------------------------B
方案1:
- A -> T : {Kab}_Kat
- T -> B : {Kab}_Kbt
入侵流程:
- A -> T : {Kab}_Kat 被 I 监听
- I(A) -> T : {Kab}_Kat
- T -> I : {Kab}_Kit I可推导出Kab
方案5(达成安全及相互认证):
- A -> T : {A,B,Kab,Na}_Kat
- T -> B : {B,A,Kab,Na}_Kbt
- B -> A : {A,B,Na,Nb}_Kab
- A -> B : {A,B,Nb}_Kab
方案6(对5的优化):
- A -> T : {B,Kab}_Kat
- T -> B : {A,Kab}_Kbt
- B -> A : {B,Nb}_Kab
- A -> B : {Nb}_Kab
- 从高的角度看自动化测试
- Django中请求的生命周期
- 程序猿python学习AIphaZero,TensorFlow强化学习AI游戏,100行代码运行看看!
- awk中NF的使用
- tar.gz 解压
- Python&机器学习之项目实践
- JAVA CDI 学习(5) - 如何向RESTFul Service中注入EJB实例
- mysql5.7 column cannot be null
- 区块链大热 价值近20万的Matrix.io被启用
- 比特币科普之什么是区块高度?
- 如何正确并快速理解MapReduce
- mysqldump的简单使用
- mac:在当前文件夹打开terminal终端
- 斯诺登研发黑客警报App上架 监测功能引发争议
- JavaScript 教程
- JavaScript 编辑工具
- JavaScript 与HTML
- JavaScript 与Java
- JavaScript 数据结构
- JavaScript 基本数据类型
- JavaScript 特殊数据类型
- JavaScript 运算符
- JavaScript typeof 运算符
- JavaScript 表达式
- JavaScript 类型转换
- JavaScript 基本语法
- JavaScript 注释
- Javascript 基本处理流程
- Javascript 选择结构
- Javascript if 语句
- Javascript if 语句的嵌套
- Javascript switch 语句
- Javascript 循环结构
- Javascript 循环结构实例
- Javascript 跳转语句
- Javascript 控制语句总结
- Javascript 函数介绍
- Javascript 函数的定义
- Javascript 函数调用
- Javascript 几种特殊的函数
- JavaScript 内置函数简介
- Javascript eval() 函数
- Javascript isFinite() 函数
- Javascript isNaN() 函数
- parseInt() 与 parseFloat()
- escape() 与 unescape()
- Javascript 字符串介绍
- Javascript length属性
- javascript 字符串函数
- Javascript 日期对象简介
- Javascript 日期对象用途
- Date 对象属性和方法
- Javascript 数组是什么
- Javascript 创建数组
- Javascript 数组赋值与取值
- Javascript 数组属性和方法
- 详说C#中的结构struct
- c#结构体总结
- 跨域问题(CORS / Access-Control-Allow-Origin)
- C#中的结构体与类的区别
- c#结构体与类的区别,及使用技巧 C#中的结构体与类的区别
- hikvision SDK使用(转)
- 《Scikit-Learn与TensorFlow机器学习实用指南》 第11章 训练深度神经网络(上)
- 海康SDK开发步骤
- 《Scikit-Learn与TensorFlow机器学习实用指南》 第11章 训练深度神经网络(下)
- applet跨域访问的安全性问题(java.security.AccessControlException:access denied)
- JSON解析问题:net.sf.json.JSONException: There is a cycle in the hierarchy!
- 海康相机SDK联合c++标定
- 开发一个Node命令行小玩具全过程--高颜统计工具
- 消息未读之点不完的小红点(Node+Websocket)
- pkg版本规范管理自动化最佳实践