Search papers, labs, and topics across Lattice.
The paper introduces BMC4TimeSec, a tool for verifying Timed Security Protocols (TSP) using SMT-based bounded model checking. The tool models TSP executions as Timed Interpreted Systems (TIS) or Timed Interleaved Interpreted Systems (TIIS) and represents agents' knowledge evolution using knowledge automata. BMC4TimeSec's public availability and demonstration video facilitate accessibility and understanding of the tool's capabilities for security protocol verification.
Find flaws in your timed security protocols faster with BMC4TimeSec, a new end-to-end verification tool combining SMT-based bounded model checking and multi-agent modeling.
We present BMC4TimeSec, an end-to-end tool for verifying Timed Security Protocols (TSP) based on SMT-based bounded model checking and multi-agent modelling in the form of Timed Interpreted Systems (TIS) and Timed Interleaved Interpreted Systems (TIIS). In BMC4TimeSec, TSP executions implement the TIS/TIIS environment (join actions, interleaving, delays, lifetimes), and knowledge automata implement the agents (evolution of participant knowledge, including the intruder). The code is publicly available on \href{https://github.com/agazbrzezny/BMC4TimeSec}{GitHub}, as is a \href{https://youtu.be/aNybKz6HwdA}{video} demonstration.
