Abstract
The Timed Observational Transition System (TOTS)/CafeOBJ method is a version of the OTS/CafeOBJ method for modeling, specification and verification of distributed systems and protocols with real time constraints. In this paper we report on a case study from the field of source authentication protocols, TESLA protocol, to show the application of the method to such complex systems. We prove that our model of the protocol satisfies that the receiver does not accept as authentic any message unless it was actually sent by the sender. To verify the property we have used several other invariants which include timing information. To our knowledge, this is the first time that the method has been applied to the formal analysis of such a complex protocol. © 2012 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Ouranos, I., Ogata, K., & Stefaneas, P. (2012). Formal analysis of TESLA protocol in the timed OTS/CafeOBJ method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7610 LNCS, pp. 126–142). https://doi.org/10.1007/978-3-642-34032-1_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
