FORMALIZATION OF BROADCAST COMMUNICATION IN PROCESS CALCULUS AND ITS MODEL CHECKING

Ritsuya Ikeda, Takuya Ohata, Shin-ya Nishizaki

2009

Abstract

A large number of studies have examined communicating processes in formalizing concurrent systems for unicast communications. We propose a process calculus to enable formalizing communicating processes and their computational costs to analyze denial-of-service attack resistance by estimating the cost balance between a victim and attackers. Our system is similar to other process calculi in that it is based on unicast communication. Broadcast communication is also important in the context of denial-of-service attack resistance because several denial-of-service attack methods, such as the Smurf attack, use broadcast communications. Little is known about the formal framework of broadcast communicating processes. In this paper, we formalize broadcast communication in the framework of process calculus and apply it to an analysis of denial-of-service attack resistance of communicating processes via broadcast communication. We propose an extension of the proposed process calculus and an analysis method that uses the SPIN model checker. We give two examples of broadcast communication and verify several properties using the SPIN model checker.

Paper Citation

in Harvard Style

Ikeda R., Ohata T. and Nishizaki S. (2009). FORMALIZATION OF BROADCAST COMMUNICATION IN PROCESS CALCULUS AND ITS MODEL CHECKING . In Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT, ISBN 978-989-674-009-2, pages 348-352. DOI: 10.5220/0002276703480352

in Bibtex Style

@conference{icsoft09,
author={Ritsuya Ikeda and Takuya Ohata and Shin-ya Nishizaki},
title={FORMALIZATION OF BROADCAST COMMUNICATION IN PROCESS CALCULUS AND ITS MODEL CHECKING},
booktitle={Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT,},
year={2009},
pages={348-352},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002276703480352},
isbn={978-989-674-009-2},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Software and Data Technologies - Volume 1: ICSOFT,
TI - FORMALIZATION OF BROADCAST COMMUNICATION IN PROCESS CALCULUS AND ITS MODEL CHECKING
SN - 978-989-674-009-2
AU - Ikeda R.
AU - Ohata T.
AU - Nishizaki S.
PY - 2009
SP - 348
EP - 352
DO - 10.5220/0002276703480352