Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2014/05/01 Vol. E97-DNo. 5pp. 1160-1170 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,
Publication: IEICE TRANSACTIONS on Information and Systems Publication Date: 2013/06/01 Vol. E96-DNo. 6pp. 1258-1267 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Formal Methods Keyword: mobile DRM, OMA, order of rights object evaluation, CafeOBJ, safety, invariant properties,