Consiglio Nazionale delle Ricerche

Tipo di prodottoArticolo in rivista
TitoloAutomatic Testing Equivalence Verification of Spi-calculus Specifications
Anno di pubblicazione2003
Formato
  • Elettronico
  • Cartaceo
Autore/iL. Durante; R. Sisto; A. Valenzano
Affiliazioni autoriL. 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
Autori CNR e affiliazioni
  • RICCARDO SISTO
  • LUCA DURANTE
  • ADRIANO VALENZANO
Lingua/e
  • inglese
AbstractTesting equivalence is a powerful means for expressing the security properties of cryptographic protocols, but its formal verification is a difficult task because of the quantification over contexts on which it is based. Previous articles have provided insights into using theorem-proving for the verification of testing equivalence of spi calculus specifications. This article addresses the same verification problem, but uses a state exploration approach. The verification technique is based on the definition of an environment-sensitive, labeled transition system representing a spi calculus specification. Trace equivalence defined on such a transition system coincides with testing equivalence. Symbolic techniques are used to keep the set of traces finite. If a difference in the traces of two spi descriptions (typically a specification and the corresponding implementation of a protocol) is found, it can be used to automatically build the spi calculus description of an intruder process that can exploit the difference.
Lingua abstractinglese
Altro abstract-
Lingua altro abstract-
Pagine da222
Pagine a284
Pagine totali63
RivistaACM transactions on software engineering and methodology
Attiva dal 1992
Editore: Association for Computing Machinery, - New York, NY
Paese di pubblicazione: Stati Uniti d'America
Lingua: inglese
ISSN: 1049-331X
Titolo chiave: ACM transactions on software engineering and methodology
Titolo proprio: ACM transactions on software engineering and methodology.
Titolo abbreviato: ACM trans. softw. eng. methodol.
Titoli alternativi:
  • Transactions on software engineering and methodology
  • Association for Computing Machinery transactions on software engineering and methodology
  • TOSEM
Numero volume della rivista12
Fascicolo della rivista2
DOI10.1145/941566.941570
Verificato da refereeSì: Internazionale
Stato della pubblicazione-
Indicizzazione (in banche dati controllate)
  • ISI Web of Science (WOS) (Codice:000185742100004)
Parole chiavenetwork security, Formal methods, Testing equivalence, Spi-calculus, Automatic analysis
Link (URL, URI)http://dl.acm.org/citation.cfm?doid=941566.941570
Titolo parallelo-
Data di accettazione-
Note/Altre informazioni-
Strutture CNR
  • IEIIT — Istituto di elettronica e di ingegneria dell'informazione e delle telecomunicazioni
Moduli CNR
    Progetti Europei-
    Allegati
    • Automatic Testing Equivalence Verification of Spi-calculus Specifications

    Dati associati a vecchie tipologie
    I dati associati a vecchie tipologie non sono modificabili, derivano dal cambiamento della tipologia di prodotto e hanno solo valore storico.
    Editore
    • Association Of Computing Machinery (ACM), New York (Stati Uniti d'America)

    Dati storici
    I dati storici non sono modificabili, sono stati ereditati da altri sistemi (es. Gestione Istituti, PUMA, ...) e hanno solo valore storico.
    Area disciplinareComputer Science & Engineering
    Area valutazione CIVRIngegneria industriale e informatica
    Rivista ISIACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY [13142J0]
    Descrizione sintetica del prodottoTesting equivalence is a powerful means for expressing the security properties of cryptographic protocols, but its formal verification is a difficult task because of the quantification over contexts on which it is based. Previous articles have provided insights into using theorem-proving for the verification of testing equivalence of spi calculus specifications. This article addresses the same verification problem, but uses a state exploration approach. The verification technique is based on the definition of an environment-sensitive, labeled transition system representing a spi calculus specification. Trace equivalence defined on such a transition system coincides with testing equivalence. Symbolic techniques are used to keep the set of traces finite. If a difference in the traces of two spi descriptions (typically a specification and the corresponding implementation of a protocol) is found, it can be used to automatically build the spi calculus description of an intruder process that can exploit the difference.