Paper
BMC4TimeSec: Verification Of Timed Security Protocols
Authors
Agnieszka M. Zbrzezny
Abstract
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2602.17590v1</id>\n <title>BMC4TimeSec: Verification Of Timed Security Protocols</title>\n <updated>2026-02-19T18:12:01Z</updated>\n <link href='https://arxiv.org/abs/2602.17590v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2602.17590v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.CR'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.MA'/>\n <published>2026-02-19T18:12:01Z</published>\n <arxiv:comment>To appear in the Proceedings of the 25th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2026), May 25 - 29, 2026, Paphos, Cyprus</arxiv:comment>\n <arxiv:primary_category term='cs.CR'/>\n <author>\n <name>Agnieszka M. Zbrzezny</name>\n </author>\n </entry>"
}