INITIAL EXAMPLE 15
]
-->
[ Client_1( $S, ~k ) // Store server and key for next step of thread
, Out( aenc(~k, pkS) ) // Send the encrypted session key to the server
]
rule Client_2:
[ Client_1(S, k) // Retrieve server and session key from previous step
, In( h(k) ) // Receive hashed session key from network
]
--[ SessKeyC( S, k ) ]-> // State that the session key 'k'
[] // was setup with server 'S'
// A server thread answering in one-step to a session-key setup request from
// some client.
rule Serv_1:
[ !Ltk($S, ~ltkS) // lookup the private-key
, In( request ) // receive a request
]
--[ AnswerRequest($S, adec(request, ~ltkS)) ]-> // Explanation below
[ Out( h(adec(request, ~ltkS)) ) ] // Return the hash of the
// decrypted request.
Here, the rst rule models the client sending its message, while the second rule models it receiving
a response. The third rule models the server, both receiving the message and responding in one
single rule.
Several explanations are in order. First, Tamarin uses C-style comments, so everything between /*
and */ or the line following // is a comment. Second, we log the session-key setup requests received
by servers using an action to allow the formalization of the authentication property for the client
later.
Modeling security properties
Security properties are dened over traces of the action facts of a protocol execution.
We have two properties that we would like to evaluate. In the Tamarin framework, properties to be
evaluated are denoted by lemmas. The rst of these is on the secrecy of session key secrecy from the
client point of view. The lemma Client_session_key_secrecy says that it cannot be that a client
has set up a session key k with a server S and the adversary learned that k unless the adversary
performed a long-term key reveal on the server S. The second lemma Client_auth species client
authentication. This is the statement that, for all session keys k that the clients have setup with
a server S, there must be a server that has answered the request or the adversary has previously
performed a long-term key reveal on S.
lemma Client_session_key_secrecy:
剩余110页未读，继续阅读
车联网安全杂货铺
- 粉丝: 661
- 资源: 38
我的内容管理
展开
最新资源
- AirKiss技术详解：无线传递信息与智能家居连接
- Hibernate主键生成策略详解
- 操作系统实验：位示图法管理磁盘空闲空间
- JSON详解：数据交换的主流格式
- Win7安装Ubuntu双系统详细指南
- FPGA内部结构与工作原理探索
- 信用评分模型解析：WOE、IV与ROC
- 使用LVS+Keepalived构建高可用负载均衡集群
- 微信小程序驱动餐饮与服装业创新转型：便捷管理与低成本优势
- 机器学习入门指南：从基础到进阶
- 解决Win7 IIS配置错误500.22与0x80070032
- SQL-DFS：优化HDFS小文件存储的解决方案
- Hadoop、Hbase、Spark环境部署与主机配置详解
- Kisso：加密会话Cookie实现的单点登录SSO
- OpenCV读取与拼接多幅图像教程
- QT实战：轻松生成与解析JSON数据
资源上传下载、课程学习等过程中有任何疑问或建议，欢迎提出宝贵意见哦~我们会及时处理！
点击此处反馈
