TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned

• OURANOS Iakovos

  HCAA, Heraklion Airport

• OGATA Kazuhiro

  School of Information Science, JAIST

• STEFANEAS Petros

  School of Applied Mathematical and Physical Sciences, NTUA

抄録

In this paper we report on experiences gained and lessons learned by the use of the Timed OTS/CafeOBJ method in the formal verification of TESLA source authentication protocol. These experiences can be a useful guide for the users of the OTS/CafeOBJ, especially when dealing with such complex systems and protocols.

収録刊行物

• IEICE Transactions on Information and Systems

  IEICE Transactions on Information and Systems E97.D (5), 1160-1170, 2014

  一般社団法人 電子情報通信学会

キーワード

• source authentication
• TESLA protocol
• CafeOBJ
• verification
• timed OTS
• lessons learned

詳細情報

• CRID: 1390001204380070528
• NII論文ID: 130004519231
• DOI: 10.1587/transinf.e97.d.1160
• ISSN: 17451361
• ISSN: 09168532
• Web Site: https://www.jstage.jst.go.jp/article/transinf/E97.D/5/E97.D_1160/_pdf
• 本文言語コード: en
• データソース種別:
  • JaLC
  • Crossref
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可