Effective reduction of cryptographic protocols specification for model-checking with Spin

Piotr Sapiecha, Urszula Krawczyk

Abstract


In this article a practical application of the Spin model checker for verifying cryptographic
protocols was shown. An efficient framework for specifying a minimized protocol model while
retaining its functionality was described. Requirements for such a model were discussed, such
as powerful adversary, multiple protocol runs and a way of specifying validated properties as
formulas in temporal logic.

Full Text:

PDF


DOI: http://dx.doi.org/10.2478/v10065-011-0002-y
Date of publication: 2011-01-01 00:00:00
Date of submission: 2016-04-28 09:04:13


Statistics


Total abstract view - 547
Downloads (from 2020-06-17) - PDF - 0

Indicators



Refbacks

  • There are currently no refbacks.


Copyright (c) 2015 Annales UMCS Sectio AI Informatica

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.