专栏首页认证协议的形式化分析(补充)SPAN+AVISPA for Verifying Cryptographic Protocols
原创

(补充)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

  1. A -> B : {A,B,Na}Kb
  2. B -> A : {A,B,Na,s}Ka

达成:信息的机密性、新鲜性、A知道s是B建立的(Na只有B的私钥能推导出来)、会话成功后A认证B。

protocol 5(使用对称密钥)

  1. A -> B : {A,B,Na}Kab
  2. B -> A : {A,B,Na,s}Kab

DY模型:

  1. 加密是安全的
  2. 入侵者有对整个网络的控制权

安全目标属性:

可参考文章:形式化分析工具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:

  1. A -> T : {Kab}_Kat
  2. T -> B : {Kab}_Kbt

入侵流程:

  1. A -> T : {Kab}_Kat 被 I 监听
  2. I(A) -> T : {Kab}_Kat
  3. T -> I : {Kab}_Kit I可推导出Kab

方案5(达成安全及相互认证):

  1. A -> T : {A,B,Kab,Na}_Kat
  2. T -> B : {B,A,Kab,Na}_Kbt
  3. B -> A : {A,B,Na,Nb}_Kab
  4. A -> B : {A,B,Nb}_Kab

方案6(对5的优化):

  1. A -> T : {B,Kab}_Kat
  2. T -> B : {A,Kab}_Kbt
  3. B -> A : {B,Nb}_Kab
  4. A -> B : {Nb}_Kab

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 形式化分析工具(五)使用CAS +语法轻松编写HLPSL规范

    在协议执行的开始,每个主体都需要一些初步的知识来撰写他的消息。知识之后的字段将与每个用户相关联的标识符列表,描述了协议开始之前他所知道的所有数据(names,k...

    春风大魔王
  • 形式化分析工具AVISPA(三)学习User micro-manual of AVISPA

    hlpsl2if:将用HLPSL语言编写的规范转换为IF语言的低级规范的工具。cl-atse:用于分析安全属性的工具

    春风大魔王
  • 形式化分析工具(六):HLPSL Tutorial(Example3)

    示例协议来源为安德鲁安全RPC协议的改编版:该协议用于相互认证双方,然后建立可以用于进一步通信的新共享密钥K1ab(可以作为其它协议的一部分)。此协议的A-B表...

    春风大魔王
  • 盘点那些走向世界的中国项目

    Kylin™是第一个成为Apache顶级开源项目的中国作品。它是一个分布式分析引擎,提供Hadoop之上的SQL查询接口及多维分析(OLAP)能力以支持超大规模...

    IT大咖说
  • 互联网+汽车,一场打破传统的历史性变革

    镁客网
  • 如何在调用Marketing Cloud contact创建API时增加对扩展字段的支持

    需求:扩展字段“微信ID”是我创建出来的extension field,我想用Marketing Cloud提供的contact creation API,在创...

    Jerry Wang
  • SAP Cloud for Customer的Calculated field字段

    一个例子:客户在销售订单行项目上创建了一个扩展字段A,这个字段的值是最终用户手动输入的: An example: Suppose customer has a...

    Jerry Wang
  • Data exchange of settype COMM_PRFREEATTR

    (1) in ERP, use tcode SM30, view name: MATERIALID, configure an external long ma...

    Jerry Wang
  • 混合线性模型学习笔记4

    这个小节主要是介绍混合线性模型的理论知识,包括固定因子的显著性检验(Wald),随机因子的检验(LRT),固定因子的效应值(BLUE),随机因子的效应值(BLU...

    邓飞
  • iOS中UITableViewController自带的刷新控件

            在iOS开发中,使用tableView的界面,大多会用到一个下拉刷新的的控件,第三方库中,我们一般会选择比较好用的MJRefresh,其实,在i...

    珲少

扫码关注云+社区

领取腾讯云代金券