Scyther 形式化分析工具资料整理(三)
作者:互联网
1、作者Cas Cremers在做TLS1.3的时候我么发现并没有使用Scyther 形式化丰分析工具对其进行分析,而是使用了 The Tamarin 。作者建立了TLS.13的模型。 那么我的目标是 使用Scyther工具对TLS1.2协议的握手协议和TLS1.3版本的握手协议分别进行形式化的分析。通过对比TLS1.3较之前的TLS1.2版本上的改进之后是否还存在攻击图输出。或者改变TLS1.3版本协议中的消息发送的时序或者其他工业网络中相关的问题,在检查是否TLS1.3版本的协议存在漏洞。
作者对TLS1.3协议版本的形式化分析发表的相关论文:Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication
作者公开发表的所有文章的列表:(这里我只挑选关于Scyther 形式化分析工具的论文资料)
Publications
Books/Book chapters
- Operational Semantics and Verification of Security Protocols
With S. Mauw. Information Security and Cryptography series, Springer, 2012. - Book chapter: Model Checking Security Protocols
With D. Basin and C. Meadows.
In: Handbook of Model Checking, Springer.
[bibtex]
Conference and workshop papers
- Abstractions for security protocol verification
With Thanh Binh Nguyen and Christoph Sprenger.
Journal of Computer Security, 2018. - A Comprehensive Symbolic Analysis of TLS 1.3
With M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe.
ACM CCS 2017: Proceedings of the 24th ACM Conference on Computer and Communications Security, Dallas, USA, 2017. - A Formal Security Analysis of the Signal Messaging Protocol
With K. Cohn-Gordon, B. Dowling, L. Garratt, and D. Stebila
IEEE EuroS&P 2017.
[full version (eprint) - On Post-Compromise Security
With K. Cohn-Gordon and L. Garratt.
CSF 2016, Proc. of the 29th IEEE Computer Security Foundations Symposium, 2016.
[Long version] [bibtex] - Automated Analysis of TLS 1.3: 0-RTT, Resumption and Delayed Authentication
With M. Horvat, S. Scott, and T. van der Merwe.
IEEE Symposium on Security and Privacy (Oakland), San Jose, CA, May 2016.
[PDF] [further information and sources] [bibtex - Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
With B. Schmidt, S. Meier, and D. Basin.
CSF 2012, Proc. of the 25th IEEE Computer Security Foundations Symposium, Harvard, 2012.
[pdf] [bibtex] [Extended version]
Tool support: Tamarin Prover - Comparing State Spaces in Automatic Security Protocol Analysis
With P. Lafourcade and P. Nadeau.
Formal to Practical Security (LNCS 5458/2009), Springer.
[pdf] [bibtex]
Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file] - Comparing State Spaces in Automatic Security Protocol Analysis
With P. Lafourcade and P. Nadeau.
Formal to Practical Security (LNCS 5458/2009), Springer.
[pdf] [bibtex]
Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file] - Feasibility of multi-protocol attacks
ARES 2006, Proc. of the first international conference on availability, reliability and security, Vienna, Austria, April 2006, IEEE.
[pdf] [bibtex] - Operational semantics of security protocols
With S. Mauw.
Scenarios: models, transformations and tools: revised selected papers. Dagstuhl castle, Germany, September 7-12, 2003, LNCS, Vol. 3466, 2005, Springer.
[pdf] [bibtex] - 以及后面的55-60。
- Operational semantics of security protocols
- Feasibility of multi-protocol attacks
- Comparing State Spaces in Automatic Security Protocol Analysis
- Comparing State Spaces in Automatic Security Protocol Analysis
- Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
2、形式化分析工具的功能差异性比较
并不是说 所有的形式都适合使用某一种形式化分析工具来做,而是每一种协议都有自己适合的分析工具进行分析。 我现在觉得还是没有看懂Scyther的手册还有形式化描述的语言。Scyther是一种自动验证协议的安全工具,
scyther的主要特点是: 可以使用无限次数的会话和随机数来验证协议; 可以表征协议,产生所有可能的协议行为的有限表示。
作者使用 scyther工具已经分析的协议有:
作者一共开发了三种形式化分析的工具,分别是 Scyther 、Scyther-proof 、Tamarin
作者说道: 对于各种对手模型的标准分析或者了解安全协议,可以使用 Scyther 工具
需要机器检查的证据使用 Scyther-proof
对于高级分析和尖端功能使用 Tamarin
标签:协议,TLS1.3,Scyther,形式化,bibtex,整理,Security 来源: https://www.cnblogs.com/xinxianquan/p/10876938.html