TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E97-D No.5 pp.1160-1170
- Publication Date
- 2014/05/01
- Publicized
- 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
Authors
Iakovos OURANOS
Heraklion Airport
Kazuhiro OGATA
JAIST
Petros STEFANEAS
NTUA
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Iakovos OURANOS, Kazuhiro OGATA, Petros STEFANEAS, "TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned" in IEICE TRANSACTIONS on Information,
vol. E97-D, no. 5, pp. 1160-1170, May 2014, doi: 10.1587/transinf.E97.D.1160.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E97.D.1160/_p
Copy
@ARTICLE{e97-d_5_1160,
author={Iakovos OURANOS, Kazuhiro OGATA, Petros STEFANEAS, },
journal={IEICE TRANSACTIONS on Information},
title={TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned},
year={2014},
volume={E97-D},
number={5},
pages={1160-1170},
abstract={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.},
keywords={},
doi={10.1587/transinf.E97.D.1160},
ISSN={1745-1361},
month={May},}
Copy
TY - JOUR
TI - TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
T2 - IEICE TRANSACTIONS on Information
SP - 1160
EP - 1170
AU - Iakovos OURANOS
AU - Kazuhiro OGATA
AU - Petros STEFANEAS
PY - 2014
DO - 10.1587/transinf.E97.D.1160
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E97-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2014
AB - 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.
ER -
English
