腾讯云开发者社区-腾讯云

开发者社区

文档建议反馈控制台

最新优惠活动

文章/答案/技术大牛

发布

认证协议的形式化分析

形式化分析工具：AVISPA 协议安全性分析

专栏作者

19

文章

35428

阅读量

25

订阅数

基础知识补充3：对称加密与非对称加密简介

对称加密是最快速、最简单的一种加密方式，加密（encryption）与解密（decryption）用的是同样的密钥（secret key）。

春风大魔王

2020-07-29

1.8K0

基础知识补充2：身份认证

邮件证书 https 编程算法

对物的认证目的在于使数据能安全可靠地传递，这里的安全是指不被非法获取，可靠是指能鉴别假冒欺骗等行为，对物的认证其实是对数据来源的认证。

春风大魔王

2020-07-29

2.2K0

基础知识补充1：密钥交换/协商机制

编程算法专用宿主机数据加密服务全站加速网络

密钥协商这一概念也得以提出。一方面它能为参与者提供身份认证，另一方面，也能与参与者协商并共享会话密钥。

春风大魔王

2020-07-29

4.6K0

形式化分析工具（七）AVISPA v1.1 User Manual

bash bash 指令 http

A VISPA (Automated Validation of Internet Security Protocols and Applications) Internet安全协议和应用程序的自动验证

春风大魔王

2020-07-26

1.5K0

形式化分析工具（六）：HLPSL Tutorial（Example 4，other）

编程算法 http nat NAT 网关

默认情况下，CL-AtSe打印的攻击痕迹可能不是最小的。实际上，这是CL-Atse的首次攻击。但是，可以使用-short选项要求CL-Atse输出最小的攻击之一（以步数为单位）：

春风大魔王

2020-07-24

1.1K0

形式化分析工具（六）：HLPSL Tutorial（Example3）

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

春风大魔王

2020-07-23

1.3K0

形式化分析工具（六）：HLPSL Tutorial

nat NAT 网关编程算法 linux

本文为阅读笔记。文章题目为： HLPSL Tutorial A Beginner’s Guide to Modelling and Analysing Internet Security Protocols

春风大魔王

2020-07-23

2.9K1

（补充）SPAN+AVISPA for Verifying Cryptographic Protocols

ide python http

消息认证：如果A知道是谁创建的消息m，则称A能认证m。电子签名：私钥加密、公钥解密。（ID,{ID}K-1）比较ID是否一样。

春风大魔王

2020-07-22

1.1K0

SPAN: a Security Protocol ANimator for A VISPA

linux 网络安全安全

Protocol Simulation：模拟协议并建立对应于HLPSL规范的特定MSC（Message Sequence Charts，消息序列图）；

春风大魔王

2020-07-21

1.6K0

SPAN+A VISPA for Verifying Cryptographic Protocols

原作者有配套的视频教程。关注：养两只猫。发送视频教程，获取地址。 image.png image.png image.png image.png image.png image.png image.png image.png image.png image.png image.png image.png image.png image.png

春风大魔王

2020-07-21

1.4K0

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

数据分析面向对象编程

在协议执行的开始，每个主体都需要一些初步的知识来撰写他的消息。知识之后的字段将与每个用户相关联的标识符列表，描述了协议开始之前他所知道的所有数据（names，keys，function等）。我们假设每个用户的名字总是隐含在他的初始知识中。

春风大魔王

2020-07-20

2K0

形式化分析工具：在虚拟操作系统和主机操作系统之间配置共享文件夹

1. 在VirtualBox应用程序中，单击虚拟机名称，然后单击“配置”，然后单击“共享文件夹”，然后添加与主机OS上的路径关联的永久性虚拟共享文件夹。如图所示我关联的共享文件夹为myvirtualFolder。路径根据自己需要进行定义。

春风大魔王

2020-07-20

1.6K0

形式化分析工具AVISPA（四） SPAN工具简要介绍

monitoring pdf simulation

3.protocol、intruder、attack simulation是三种模拟形式。分别是协协议仿真、入侵者仿真、攻击仿真

春风大魔王

2020-07-19

4K0

形式化分析工具AVISPA（三）2.学习User micro-manual of AVISPA

网络安全安全

工具hlpsl2if编译扩展名为.hlpsl的文件中作为参数给定的协议的规范，并列出规范中发现的错误，或者生成一个名称相同但扩展名为 .if 的文件，该文件将在以后分析。

春风大魔王

2020-07-19

9860

形式化分析工具AVISPA（三）学习User micro-manual of AVISPA

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

春风大魔王

2020-07-19

2.2K0

形式化分析工具AVISPA（二）：使用及教程资料

参考资料：https://blog.csdn.net/pan_tian/article/details/22619687

春风大魔王

2020-07-18

1.8K0

形式化分析工具AVISPA

虚拟化 https 网络安全日志服务

1.(3条消息)AVISPA入门级教程_Summer Day-CSDN博客_avispa

春风大魔王

2020-07-15

2.4K0

uthentication Handover and Privacy Protection in 5G HetNets Using Software-Defin

最近，通过共存的异构网络进行覆盖覆盖的密集小蜂窝部署已成为5G移动网络的可行解决方案。但是，由于5G小型蜂窝和HetNets中潜在的频繁切换和认证，这种多层体系结构以及5G中严格的延迟要求带来了新的安全配置挑战。在本文中，我们回顾了相关研究，并将SDN引入5G作为平台，以实现高效的身份验证切换和隐私保护。我们的目标是通过在相关接入点之间共享用户相关的安全上下文信息，通过5G HetNet的全局管理来简化身份验证切换。我们证明了支持SDN的安全解决方案通过其集中控制功能是高效的，这对于延迟受限的5G通信至关重要。

春风大魔王

2020-06-22

3800

虚拟化资源管理阅读笔记（一）

一种新的资源管理系统模型，并提出一种在云数据中心中进行有效的虚拟机分配的方法。从技术上讲，虚拟机分配问题正式化为装箱问题，而Best Fit算法（BF）被部署为云数据中心中的一种有效资源管理。系统模型将有助于节省未充分利用的物理服务器，并在将虚拟机映射到数据中心中的服务器时有效地做出响应。

春风大魔王

2020-06-12

4890

没有更多了

社区活动

腾讯技术创作狂欢月

“码”上创作 21 天，分 10000 元奖品池！

Python精品学习库

代码在线跑，知识轻松学

博客搬家 | 分享价值百万资源包

自行/邀约他人一键搬运博客，速成社区影响力并领取好礼

技术创作特训营·精选知识专栏

往期视频·千货材料·成员作品最新动态