A State-Exploration Technique for Spi-Calculus Testing Equivalence Verification (Contributo in atti di convegno)

Type
Label
  • A State-Exploration Technique for Spi-Calculus Testing Equivalence Verification (Contributo in atti di convegno) (literal)
Anno
  • 2000-01-01T00:00:00+01:00 (literal)
Alternative label
  • L. Durante; R. Sisto; A. Valenzano (2000)
    A State-Exploration Technique for Spi-Calculus Testing Equivalence Verification
    in FORTE/PSTV 2000 Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX), Pisa, 10-13 ottobre 2000
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • L. Durante; R. Sisto; A. Valenzano (literal)
Pagina inizio
  • 155 (literal)
Pagina fine
  • 170 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#url
  • http://www.springer.com/computer/ai/book/978-0-7923-7968-3 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume
  • Formal Methods for Distributed System Development (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#volumeInCollana
  • 55 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#pagineTotali
  • 16 (literal)
Note
  • ACM DL (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • L. Durante; A. Valenzano: CNR-IEIIT, Istituto di Elettronica e di Ingegneria dell'Informazione e delle Telecomunicazioni, Torino, Italy R. Sisto: CNR-IEIIT e Dipartimento di Automatica e Informatica, Politecnico di Torino, Italy (literal)
Titolo
  • A State-Exploration Technique for Spi-Calculus Testing Equivalence Verification (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
  • 0-7923-7968-3 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume
  • T. Bolognesi; D. Latella (literal)
Abstract
  • 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. (literal)
Editore
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:


Prodotto
Autore CNR di
Editore di
Insieme di parole chiave di
data.CNR.it