Petros STEFANEAS


TESLA Source Authentication Protocol Verification Experiment in the Timed OTS/CafeOBJ Method: Experiences and Lessons Learned
Iakovos OURANOS Kazuhiro OGATA Petros STEFANEAS 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2014/05/01
Vol. E97-D  No. 5  pp. 1160-1170
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
Keyword: 
source authenticationTESLA protocolCafeOBJverificationtimed OTSlessons learned
 Summary | Full Text:PDF

An Algorithm for Allocating User Requests to Licenses in the OMA DRM System
Nikolaos TRIANTAFYLLOU Petros STEFANEAS Panayiotis FRANGOS 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2013/06/01
Vol. E96-D  No. 6  pp. 1258-1267
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Methods
Keyword: 
mobile DRMOMAorder of rights object evaluationCafeOBJsafetyinvariant properties
 Summary | Full Text:PDF

An Algebraic Framework for Modeling of Mobile Systems
Iakovos OURANOS Petros STEFANEAS Panayiotis FRANGOS 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2007/09/01
Vol. E90-A  No. 9  pp. 1986-1999
Type of Manuscript:  PAPER
Category: Concurrent Systems
Keyword: 
mobile computingalgebraic specificationformal verificationobservational transition systemsCafeOBJMobileOBJ
 Summary | Full Text:PDF