Effective reduction of cryptographic protocols specification for model-checking with Spin
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.
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:
PDFDOI: 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 - 570
Downloads (from 2020-06-17) - PDF - 0
Indicators
Refbacks
- There are currently no refbacks.
Copyright (c) 2015 Annales UMCS Sectio AI Informatica
This work is licensed under a Creative Commons Attribution 4.0 International License.