Summary
International Technical Conference on Circuits/Systems, Computers and Communications
2016
Session Number:M2-1
Session:
Number:M2-1-4
Toward Formal Analysis of Timed Anonymous Systems
Yoshinobu Kawabe, Nobuhiro Ito ,
pp.129-132
Publication Date:2016/7/10
Online ISSN:2188-5079
Summary:
This paper describes a basic idea to verify the anonymity of timed systems. Even though communication patterns are indistinguishable, the sender of a message can be identified by detecting the timing of message emission. In this paper we describe a timed system with an I/O-automaton-based formal specification language. By introducing a timer variable, we need to deal with an infinite-state system. With a simulation-based proof method for anonymity, we handle the infinite-state system directly.