Keyword : formal methods


Verification of LINE Encryption Version 1.0 Using ProVerif
Cheng SHI Kazuki YONEYAMA 
Publication:   
Publication Date: 2019/08/01
Vol. E102-D  No. 8 ; pp. 1439-1448
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approaches)
Category: 
Keyword: 
formal methodsend-to-end encryptionLINE EncryptionProVerif
 Summary | Full Text:PDF(381.5KB)

Computational Soundness of Asymmetric Bilinear Pairing-Based Protocols
Kazuki YONEYAMA 
Publication:   
Publication Date: 2017/09/01
Vol. E100-A  No. 9 ; pp. 1794-1803
Type of Manuscript:  Special Section PAPER (Special Section on Discrete Mathematics and Its Applications)
Category: 
Keyword: 
formal methodscomputational soundnessasymmetric bilinear pairing
 Summary | Full Text:PDF(269.9KB)

Hierarchical System Schedulability Analysis Framework Using UPPAAL
So Jin AHN Dae Yon HWANG Miyoung KANG Jin-Young CHOI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2016/08/01
Vol. E99-D  No. 8 ; pp. 2172-2176
Type of Manuscript:  LETTER
Category: Software System
Keyword: 
hierarchical systemschedulability analysisreal-time systemsformal methodsUPPAAL
 Summary | Full Text:PDF(455.9KB)

Formal Verification of Effectiveness of Control Activities in Business Processes
Yasuhito ARIMOTO Shusaku IIDA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/05/01
Vol. E95-D  No. 5 ; pp. 1342-1354
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Methods
Keyword: 
risk analysisbusiness processformal methods
 Summary | Full Text:PDF(821.4KB)

Towards Reliable E-Government Systems with the OTS/CafeOBJ Method
Weiqiang KONG Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2010/05/01
Vol. E93-D  No. 5 ; pp. 974-984
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Specification
Keyword: 
e-Government messaging frameworkformal methodsthe OTS/CafeOBJ methodfalsificationverification
 Summary | Full Text:PDF(534.1KB)

On Applicability of Formal Methods and Tools to Dependable Services
Fuyuki ISHIKAWA Shinichi HONIDEN 
Publication:   IEICE TRANSACTIONS on Communications
Publication Date: 2009/01/01
Vol. E92-B  No. 1 ; pp. 9-16
Type of Manuscript:  INVITED PAPER (Special Section on Networking Technologies for Dependable Networks)
Category: 
Keyword: 
dependabilitysoftware engineeringformal methods
 Summary | Full Text:PDF(198.4KB)

On Backward-Style Anonymity Verification
Yoshinobu KAWABE Ken MANO Hideki SAKURADA Yasuyuki TSUKADA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2008/09/01
Vol. E91-A  No. 9 ; pp. 2597-2606
Type of Manuscript:  PAPER
Category: Cryptography and Information Security
Keyword: 
formal methodsanonymitysoftware securityverificationtheorem-proving
 Summary | Full Text:PDF(667.2KB)

An Adversary Model for Simulation-Based Anonymity Proof
Yoshinobu KAWABE Hideki SAKURADA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2008/04/01
Vol. E91-A  No. 4 ; pp. 1112-1120
Type of Manuscript:  Special Section PAPER (Special Section on Selected Papers from the 20th Workshop on Circuits and Systems in Karuizawa)
Category: 
Keyword: 
formal methodsanonymitysoftware securityverificationtheorem-proving
 Summary | Full Text:PDF(209.4KB)

State Machines as Inductive Types
Kazuhiro OGATA Kokichi FUTATSUGI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2007/12/01
Vol. E90-A  No. 12 ; pp. 2985-2988
Type of Manuscript:  LETTER
Category: Concurrent Systems
Keyword: 
Coqformal methodsinvariant propertiesprogram specificationobservational transition systems (OTSs)
 Summary | Full Text:PDF(79.9KB)

Formal Verification of an Intrusion-Tolerant Group Membership Protocol
HariGovind V. RAMASAMY Michel CUKIER William H. SANDERS 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2003/12/01
Vol. E86-D  No. 12 ; pp. 2612-2622
Type of Manuscript:  Special Section PAPER (Special Issue on Dependable Computing)
Category: Verification and Dependability Analysis
Keyword: 
intrusion tolerancegroup communication systemsvalidationformal methods
 Summary | Full Text:PDF(538.5KB)

Using Process Algebras for the Semantic Analysis of Data Flow Networks
Cinzia BERNARDESCHI Andrea BONDAVALLI Luca SIMONCINI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 1995/08/25
Vol. E78-D  No. 8 ; pp. 959-968
Type of Manuscript:  PAPER
Category: Computer Systems
Keyword: 
computer systemssoftware theorydata flow networkssemanticsformal methodsspecification and verificationprocess algebras
 Summary | Full Text:PDF(910.6KB)