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

Iakovos OURANOS  Kazuhiro OGATA  Petros STEFANEAS  

Publication
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
Keyword: 
source authentication,  TESLA protocol,  CafeOBJ,  verification,  timed OTS,  lessons learned,  

Full Text: PDF>>
Buy this Article




Summary: 
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.