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

摘要

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.