Homepage of Koji Hasebe## Assistant Professor,

Operating System and System Software Lab (Prof. Kazuhiko Kato's Lab),

Department of Computer Science, Graduate School of Systems and Information Engineering

University of Tsukuba

Japanese Page

Photo by Kanako Hasebe

## Research interests:

- Mathematical logic
- Formal methods
- Computer security
- Distributed systems
- Game theory
- Multi-agent systems
## Selected Publications:

- K. Hasebe, T. Sawada, and K. Kato. A Game Theoretic Approach to Power Reduction in Distributed Storage Systems.
IPSJ Transactions on Advanced Computing Systems, vol.8, no.4, pp.1-9, 2015 (to appear).- K. Hasebe, J. Okoshi, and K. Kato. Power-Saving in Storage Systems for Cloud Data Sharing Services with Data Access Prediction.
IEICE Transactions, vol.E98-D, no.10, pp.1744-1754, Oct 2015. [download]- K. Hasebe, H. Kawamoto, K. Kamibayashi, A. Matsushita. Safety and Ethical Issues in the Development of Human Assistive Robots.
Cybernics, Springer-Verlag, pp.299-313, Feb 2014.- K. Hasebe, N. Nishita, and K. Kato. Highly Available Primary-Backup Mechanism for Internet Services with Optimistic Consensus.
IEEE Third International Workshop on Cloud Computing Interclouds, Multiclouds, Federations, and Interoperability (Intercloud 2014), pp.410-416, March 2014. [pdf (corrected version)]- K. Hasebe, T. Sawada, and K. Kato. Using a Potential Game for Power Reduction in Distributed Storage Systems.
IEEE International Workshop on Software Defined Systems (SDS 2014), pp.550-555, March 2014. [pdf]- G. Bana, K. Hasebe, and M. Okada. Computationally Complete Symbolic Attacker and Key Exchange.
20th ACM Conference on Computer and Communications Security (CCS 2013), pp.1231-1246, November 2013. [pdf (long version)]- J. Okoshi, K. Hasebe, and K. Kato. Power-Saving in Storage Systems for Internet Hosting Services with Data Access Prediction.
4th International Green Computing Conference (IGCC 2013), 10 pages, 2013. [pdf]- J. Okoshi, K. Hasebe, and K. Kato. Power-Aware Autonomous Distributed Storage Systems for Internet Hosting Service Platforms.
3rd International Conference on Cloud Computing (CloudComp 2012), Springer LNICST vol.112, pp.52-61, 2012. [pdf]- K. Hasebe and R. Ishikawa. Belief Revision for Inductive Game Theory.
European Workshop on Multi-agent Systems (EUMAS'11), 15 pages, 2011. [pdf]- K. Hasebe, H. Kawamoto, K. Kamibayashi, A. Matsushita, and Y. Sankai. Stepwise Process of Clinical Trials in Safety-Conscious Development of Human Assistive Robots.
IEEE International Conference on Robotics and Biomimetics (ROBIO 2011), pp.50-55, 2011.- K. Hasebe, H. Kawamoto, K. Kamibayashi, A. Matsushita, and Y. Sankai. Stepwise Process of Clinical Trials in Development of Human Assistive Robots (in Japanese).
Journal of the Robotics Society of Japan, vol.29 (3), pp.236-240, 2011.- T. Masuzawa and K. Hasebe. Iterative Information Update and Stability of Strategies.
Synthese, Springer-Verlag, vol.179 (1), pp.87-102, 2011.- K. Yamatozaki, K. Hasebe, A. Sugiki, and K. Kato. A Platform Based on Self-stabilization for Dependable Internet Services (in Japanese).
Journal of Japan Society of Software Science and Technology, vol.28 (1), pp.248-257, 2011.- K. Hasebe, K. Yamatozaki, A. Sugiki, and K. Kato. Self-Stabilizing Passive Replication for Internet Service Platforms.
4th IFIP International Conference on New Technologies, Mobility and Security, 6 pages, 2011. [pdf]- M. Ishikawa, K. Hasebe, A. Sugiki, and K. Kato. Dynamic Grid Quorum: A Reconfigurable Grid Quorum and Its Power Optimization Algorithm.
Service Oriented Computing and Applications, Springer-Verlag, vol.4 (4), pp.245-260, 2010. [pdf]- K. Hasebe, H. Kawamoto, A. Matsushita, K. Kamibayashi, and Y. Sankai. Towards a Guideline for Clinical Trials in the Development of Human Assistive Robots.
IEEE International Conference on Robotics and Biomimetics (ROBIO 2010), pp. 751-756, 2010.- K. Hasebe, T. Niwa, A. Sugiki, and K. Kato. Power-Saving in Large-Scale Storage Systems with Data Migration.
2nd IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2010), pp. 266-273, 2010. [pdf]- K. Hasebe and M. Mabuchi. Capability-Role-based Delegation in Workflow Systems.
6th IEEE/IFIP International Symposium on Trusted Computing and Communications (TrustCom-10), pp.711-717, 2010. [pdf]- K. Hasebe, M. Okada, and G. Bana. Logical Verification Methods for Security Protocol (in Japanese).
Formal Approach to Information Security(Eds. M. Hagiya and Y. Tsukada, Industrial and Applied Mathematics Series, vol. 1), Chapter 9, pp.185-202, Kyoritsu Shuppan, Tokyo, 2010.- K. Hasebe, M. Mabuchi, and A. Matsushita. Capability-Based Delegation Model in RBAC.
15th ACM Symposium on Access Control Models and Technologies (SACMAT 2010), pp. 109-118, 2010. [pdf]- M. Mabuchi, Y. Shinjo, K. Hasebe, A. Sato, and K. Kato. CapaCon: An Access Control Mechanism for Inter-Device Communications through TCP Connections.
25th Symposium on Applied Computing (ACM SAC 2010), pp.706-712, 2010.- T. Masuzawa and K. Hasebe. Iterative Information Update and Stability of Strategies.
7th European Workshop on Multi-Agent Systems (EUMAS'09), 15 pages, 2009. [pdf]- M. Ishikawa, K. Hasebe, A. Sugiki, and K. Kato. Dynamic Grid Quorum: A Novel Approach for Minimizing Power Consumption without Data Migration in Grid Quorums.
IEEE International Conference on Service-Oriented Computing and Applications (SOCA'09), pp.142-149, 2009. [pdf]- G. Bana, K. Hasebe, and M. Okada. Computational Semantics for First-Order Logical Analysis of Cryptographic Protocols.
Formal to Practical Security, Springer LNCS vol. 5458, pp.33-58, 2009. [pdf]- K. Hasebe and M. Okada. An Introduction to Logical Verification Methods for Security Protocols (in Japanese). Bulletin of the Japan Society for Industrial and Applied Mathematics, vol. 17 (4), pp.47-58, 2007.
- G. Bana, K. Hasebe, and M. Okada. Computational Semantics for Basic Protocol Logic --- A Stochastic Approach.
12th Annual Asian Computing Science Conference (ASIAN'07), LNCS vol.4846, pp.86-94, Springer-Verlag, 2007.- K. Hasebe and M. Okada. Completeness and Counter-Example Generations of a Basic Protocol Logic.
6th International Workshop on Rule-Based Programming (RULE'05), Electronic Notes in Theoretical Computer Science, vol.147 (1), pp.73-92, Elsevier Science, 2005. [pdf]- K. Hasebe and M. Okada. Non-monotonic Properties for Proving Correctness in a Framework of Compositional Logic.
Workshop on Foundations of Computer Security (FCS'04), pp.97-113, Turku, Finland, 2004. [pdf]- K. Hasebe and M. Okada. Inferences on Honesty in Compositional Logic for Security Analysis.
International Symposium on Software Security 2003 (ISSS2003), Lecture Notes in Computer Science, vol. 3233, pp.65-86, Springer-Verlag, 2004. [pdf]- V. Cremet, K. Hasebe, J.-P. Jouannaud, A. Kremer, and M. Okada. FATALIS: Real Time Processes as Linear Logic Specifications.
International Workshop on Automated Verification of Infinite-State Systems (AVIS'03), Warsaw, Poland, 2003.- K. Hasebe and M. Okada. A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic.
Software Security - Theories and Systems, LNCS vol.2609, pp.417-440, Springer-Verlag, 2003.## Teaching:

- Discrete Structure (since FY2011)
## Misc:

- My hobby/fun
- Paper fortune on the New Year's Day (at Sensoji)
## Address:

1-1-1 Tennodai, Tsukuba 305-8573, Japan

Room: CA205-2, 3F827

OSSS Lab.: Room #923, Bldg. of the Laboratory of Advanced Research B

Tel: +81-29-853-{2441, 5765, 5163}

E-mail: hasebe :: cs.tsukuba.ac.jp (where "::" = "@")