2000 | OriginalPaper | Buchkapitel
A State-Exploration Technique for Spi-Calculus Testing-Equivalence Verification
verfasst von : Luca Durante, Riccardo Sisto, Adriano Valenzano
Erschienen in: Formal Methods for Distributed System Development
Verlag: Springer US
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Several verification techniques based on theorem proving have been developed for the verification of security properties of cryptographic protocols specified by means of the spi calculus. However, to be used successfully, such powerful techniques require skilled users. Here we introduce a different technique which can overcome this drawback by allowing users to carry out the verification task in a completely automatic way. It is based on the definition of an extended labeled transition system, where transitions are labeled by means of the new knowledge acquired by the external environment as the result of the related events. By means of bounding the replication of parallel processes to a finite number, and by using an abstract representation of all explicitly allowed values in interactions between the spi process and the environment, the number of states and transitions remains finite and tractable, thus enabling the use of state-space exploration techniques for performing verification automatically.