For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
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
Publication Date: 2014/05/01
Online ISSN: 1745-1361
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>>
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.