《OAuth2.0协议安全形式化分析-》----论文摘抄整理

时间:2020-12-10 16:21:31

---恢复内容开始---

本篇论文发表在计算机工程与设计,感觉写的还是很有水准的。实验部分交代的比较清楚
本篇论文的创新点: 使用Scyther工具 主要是在 DY模型下面 形式化分析了 OAuth2.0协议的安全性。
首先 OAuth2.0协议定义了四种角色分别是: 资源拥有者、资源服务器、客户端、授权服务器、
原文指出,根据应用环境的不同,OAuth2.0协议定义了四种授权模式: 授权码模式、简化模式、客户端模式、密码模式。
其次本篇论文知识讨论了OAuth2.0的中的授权码模型,
![](//bbsmax.ikafan.com/static/L3Byb3h5L2h0dHBzL2ltZzIwMTguY25ibG9ncy5jb20vYmxvZy8xMjc2OTA0LzIwMTkwNS8xMjc2OTA0LTIwMTkwNTI5MTUyNTM3MzQ0LTcxNjY2NDExLnBuZw==.jpg)
本论文中作者将认证服务器和资源服务器作为同一个服务器(方便实验操作) 。给出了顺序图,形象的展示授权码模式下各个参数信息的传递情况:
![](//bbsmax.ikafan.com/static/L3Byb3h5L2h0dHBzL2ltZzIwMTguY25ibG9ncy5jb20vYmxvZy8xMjc2OTA0LzIwMTkwNS8xMjc2OTA0LTIwMTkwNTI5MTUzNDI0NjA3LTE4NTM0Njc4NDYucG5n.jpg)

 角色中需要定义的是本角色中使用的数据类型,(变量和常量的声明-------本作者在原文中没有说明):从图中可以看到 User角色中包括5个事件,

我下面将协议关于授权码模式的 形式化描述过程 重新写了一遍

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

根据作者的解释如下:在用户角色描述 User :------

User :------ 第一行为User角色定义,程序在实例化的时候会根据 U角色实例化 User运行实例,角色中首先需要定义的是本角色中使用到的数据类型,就是变量和常量。User 角色中主要包括5个事件,第3行使用用户和客户端的共享秘钥由用户(user)向客户端(client)发送数据req ,第4行表示表示使用共享秘钥加密接受从客户端到用户的消息,第5行表示使用共享秘钥加密客户端(user)向服务器(server)发送授权码请求,并向服务器出示必要的参数信息如:已注册的重定向 uri 、状态码等。 第6行表示接受服务器端的授权码响应,第7行表示授权码重定向客户端。

接下来讨论安全属性的问题:

 Scyther 定义一对属性  (Running ,Commit)用来表示谢意双方对传输数据的认可,如果角色 I 认可角色 R的数据  (随机数 ni  和 nr),则在角色 I 的定义末尾插入语句 Claim (I,Commit, R ,ni, nr);同样在 R中send 事件之前插入语句  claim(R,Running,ni ,nr)<p>---恢复内容结束---</p>本篇论文发表在计算机工程与设计,感觉写的还是很有水准的。实验部分交代的比较清楚
本篇论文的创新点: 使用Scyther工具 主要是在 DY模型下面 形式化分析了 OAuth2.0协议的安全性。
首先 OAuth2.0协议定义了四种角色分别是: 资源拥有者、资源服务器、客户端、授权服务器、
原文指出,根据应用环境的不同,OAuth2.0协议定义了四种授权模式: 授权码模式、简化模式、客户端模式、密码模式。
其次本篇论文知识讨论了OAuth2.0的中的授权码模型,

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

本论文中作者将认证服务器和资源服务器作为同一个服务器(方便实验操作) 。给出了顺序图,形象的展示授权码模式下各个参数信息的传递情况:

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

 角色中需要定义的是本角色中使用的数据类型,(变量和常量的声明-------本作者在原文中没有说明):从图中可以看到 User角色中包括5个事件,

我下面将协议关于授权码模式的 形式化描述过程 重新写了一遍

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

根据作者的解释如下:在用户角色描述 User :------

User :------ 第一行为User角色定义,程序在实例化的时候会根据 U角色实例化 User运行实例,角色中首先需要定义的是本角色中使用到的数据类型,就是变量和常量。User 角色中主要包括5个事件,第3行使用用户和客户端的共享秘钥由用户(user)向客户端(client)发送数据req ,第4行表示表示使用共享秘钥加密接受从客户端到用户的消息,第5行表示使用共享秘钥加密客户端(user)向服务器(server)发送授权码请求,并向服务器出示必要的参数信息如:已注册的重定向 uri 、状态码等。 第6行表示接受服务器端的授权码响应,第7行表示授权码重定向客户端。

接下来讨论安全属性的问题:

 Scyther 定义一对属性  (Running ,Commit)用来表示谢意双方对传输数据的认可,如果角色 I 认可角色 R的数据  (随机数 ni  和 nr),则在角色 I 的定义末尾插入语句 Claim (I,Commit, R ,ni, nr);同样在 R中send 事件之前插入语句  claim(R,Running,ni ,nr)
现在对实验结果解释:
通过实验分析得到实验结果,Scyther本身采用的是黑盒的验证思想,各个角色从自己的角度考虑观察问题,是否能够满足安全目标和安全属性,如果安全属性不满足则可能存在攻击路径,(实验输出攻击路径图),分别从三个角色出发分析攻击:‘
首先是 User 端角色观察到的攻击图。

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

对上面的如做解释:-------- 只有User端认为自己是和攻击者进行通信的,User端认为通信三方分别是: 角色U 为自己 ,角色C 为 Eve(攻击者),角色S为 Server;

客户端 Client 端认为通信三方 :----角色 U为 Uer ,角色 C 为自己, 角色 S为 Server

Server 端认为 ,角色 U 为 User, 角色 C 为 Client, 角色 S为自己 ,

攻击者可以破坏用户的DNS服务,将信息重定向到恶意的客户端,然后将信息修改没发送给正常的客户端和服务器,一单获得授权码,可以将授权码发送给正常客户端只是监听用户和客户端的通信,或者攻击者可以将信息修改将授权码发送给恶意的客户端,那么恶意的客户端就可以获得用户的受保护的资源实现资源的窃取。

其次是 Client 端角色观察攻击路径图如下:

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

解释如下: 只有客户端认为自己是和攻击者通信的,

User端认为通信三方为:角色 U为自己 ,角色C为 Client ,角色 S为 Server

Client端认为通信三方 : 角色U为 User,同时可能存在另一个User进程 Eve(攻击者),角色C为自己 ,角色S为 Server

Server 端认为: 角色U为User ,角色C为Client ,角色S为自己 ,此项攻击为中间人攻击,首先攻击者监听到用户向Client端发送授权码信息,如果这个通信信道未受到保护户,攻击者将原有的信息截获、原有的通道阻塞,保证授权码的有效性,之后攻击者以User的身份发起另一个会话,使用监听到的授权码嘻嘻获取资源。

Server端观察到的攻击路径如下:

《OAuth2.0协议安全形式化分析-》----论文摘抄整理

解释如下: 只有Server端认为自己是和攻击者进行通信的,

User端认为通信三方为 :角色 U为自己 ,角色C为Client ,角色 S为Server

Client端认为通信三方为: 角色U为 User ,角色C为自己 ,角色S为Server,

Sever端认为:角色U为Eve(攻击者),角色C为Client ,角色S为自己 , 首先监听者User发送到Server的授权码请求消息,然后对信息进行修改,转发给Server,Server做出授权码响应,将授权码转发给攻击者Eve。