资料获取:关注:养两只猫,发送VISPA教程
声明类型:
'
表示对应的私钥F
是单向(hash)函数 协议描述的核心是指定发送消息的规则的行列表
表达形式:
i
是步骤编号 Si
和Ri
是用户(分别是信息的发送者和接收者)→i
表示用于发送消息的通道类型,有三种类型:->
;∼>
;=>
(如下表)Mi
发送的信息。有以下_'
_[_]
_(_)
_,_
{_}_
_^_
_#_
_,...,_
具体含义如下表通道描述 | 通道表达形式 |
---|---|
Dolev-Yao channels | -> |
write protected | ∼> |
read and write protected | => |
标识符 | 含义 | 例子 |
---|---|---|
_' | arity greater than 0 | |
_[_] | for tables access | |
_(_) | 单向函数访问 | |
_,_ | pairing | |
{_}_ | 加密 | {Ins}K |
_^_ | 指数 | |
_#_ | 异或 | |
_,...,_ | 关联多个参数 | C,D,{Ins}K |
在协议执行的开始,每个主体都需要一些初步的知识来撰写他的消息。知识之后的字段将与每个用户相关联的标识符列表,描述了协议开始之前他所知道的所有数据(names,keys,function等)。我们假设每个用户的名字总是隐含在他的初始知识中。
通过将不同的值分配给持久性标识符,从而来描述运行协议的不同系统。不同的会话可以同时发生,也可以连续发生任意次。
注(个人理解):indentifiers/messages/knowledge相当于定义了一个交互模版。赋值C/D为scard与tv则是scard与tv的交互。
入侵者知识是在会话实例中引入的一组值,而不是标识符。
证明三个目标:保密、强身份认证、弱身份认证。
注:合作CAS+写的协议验证目标这一项不能够很好的由SPAN工具进行转换。需要在HLPSL中使用witness/request进行设置。
声明“messages
”部分中出现的所有值,代理和键.变量名以大写开头。如下:messages中出现有A/B/S/Kab/Kas/Kbs/Na/Nb
protocolsimple;
identifiers
A, B, S : user; %%% Declare all values, agent and keys occurring in the "messages" section
Na, Nb : number; %%% Variable names should start by a capital letter.
Kab, Kas, Kbs:symmetric_key;
messages
1. A -> S : B, {B, Kab}Kas
2. S -> B : {A, Kab}Kbs
在 knowledge
部分,对于每个代理,我们在开始协议会话之前声明其知道的信息。已知信息只能是上一个“标识符”部分的变量。例如,在这里,A知道自己,S,B和长期共享密钥Kas。但是,不知道Kab !!!因为,在此协议中,我们希望Kab是为每个会话生成的会话密钥(像现时一样)。与B相同:他不知道Kab在启动协议之前,将在消息中收到它。 S知道密钥Kas和Kbs,但不知道Kab。
knowledge
A : A, S, B, Kas;
B : A, S, B, Kbs;
S : A, S, B, Kas, Kbs;
此“knowlege
”部分不应声明任何有关入侵者的信息! “ session_instances”上方的所有部分都定义了***标准协议***,而没有入侵者。因此,我们绝不会定义任何入侵者或入侵者密钥等。它们将在下面定义。
session_instances
[A:alice,B:bob,S:server,Kas:kas,Kbs:kbs]
这是一个标准会话,其中alice,bob,server,kas,kbs是选择用来实例化"knowledge”
部分中定义的变量的任意常量。特别是,您不应为Kab定义一个常量,因为我们希望在协议执行期间生成它。
[A:i,B:bob,S:server,Kas:kis,Kbs:kbs]
这是一个会话,其中角色A将由i扮演,i是代表入侵者的保留常数。由于S和B由与上一会话相同的代理播放,因此SAME常量kbs用于此第二会话,表示B和S之间的长期密钥。由于A由i播放,因此我们创建了一个新常量入侵者和服务器之间共享的密钥。
;
会话列表以分号结尾。
intruder_knowledge
alice,bob,server,kis;
入侵者知道alice,bob,服务器和kis
原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。
如有侵权,请联系 cloudcommunity@tencent.com 删除。
原创声明:本文系作者授权腾讯云开发者社区发表,未经许可,不得转载。
如有侵权,请联系 cloudcommunity@tencent.com 删除。