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

Iakovos OURANOS  Kazuhiro OGATA  Petros STEFANEAS  

IEICE TRANSACTIONS on Information and Systems   Vol.E97-D   No.5   pp.1160-1170
Publication Date: 2014/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E97.D.1160
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
source authentication,  TESLA protocol,  CafeOBJ,  verification,  timed OTS,  lessons learned,  

Full Text: PDF>>
Buy this Article

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.