Automatic verification of multi-agent systems security properties specified with LTL

Resumen

We propose a way to verify security requirements of critical multi-agent system processes by using logic representations
and automatic reasoning. The typical multi-agent system considered in our work would be an election system with agents
representing their users and aiming to ensure security. Relevant processes are authentication, voting, re-voting, and election verification. The security requirements commonly addressed in such a voting system are: no user can vote unless it got authenticated, no invalid vote should be counted, no vote should be counted twice, and each valid vote should be eventually counted. We show a model of such security requirements by using system liveness properties, and exemplify their verification on a real system that we implement for this purpose.