Formal verification of cardholder registration in SET

G. Bella; F. Massacci; L.C. Paulson; P. Tramontano

doi:10.1007/10722599_10

Formal verification of cardholder registration in SET

G. Bella, F. Massacci, L.C. Paulson, P. Tramontano

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

© Springer-Verlag Berlin Heidelberg 2000.The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.

Original language	English
Title of host publication	Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings
Editors	F. Cuppens, Y. Deswarte, D. Gollmann, M. Waidner
Publisher	Springer Verlag
Pages	159-174
ISBN (Print)	3540410317
DOIs	https://doi.org/10.1007/10722599_10
Publication status	Published - 2000
Externally published	Yes
Event	6th European Symposium on Research in Computer Security, ESORICS 2000 - Toulouse, France Duration: 4 Oct 2000 → 6 Oct 2000

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th European Symposium on Research in Computer Security, ESORICS 2000
Country/Territory	France
City	Toulouse
Period	4/10/00 → 6/10/00

Access to Document

10.1007/10722599_10

Persistent URL (handle)

Persistent link

Cite this

Bella, G., Massacci, F., Paulson, L. C., & Tramontano, P. (2000). Formal verification of cardholder registration in SET. In F. Cuppens, Y. Deswarte, D. Gollmann, & M. Waidner (Eds.), Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings (pp. 159-174). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Springer Verlag. https://doi.org/10.1007/10722599_10

Bella, G. ; Massacci, F. ; Paulson, L.C. et al. / Formal verification of cardholder registration in SET. Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings. editor / F. Cuppens ; Y. Deswarte ; D. Gollmann ; M. Waidner. Springer Verlag, 2000. pp. 159-174 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9a7b3610b725466c85cb1f5ed70a586c,

title = "Formal verification of cardholder registration in SET",

abstract = "{\textcopyright} Springer-Verlag Berlin Heidelberg 2000.The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.",

author = "G. Bella and F. Massacci and L.C. Paulson and P. Tramontano",

year = "2000",

doi = "10.1007/10722599\_10",

language = "English",

isbn = "3540410317",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "159--174",

editor = "F. Cuppens and Y. Deswarte and D. Gollmann and M. Waidner",

booktitle = "Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings",

note = "6th European Symposium on Research in Computer Security, ESORICS 2000 ; Conference date: 04-10-2000 Through 06-10-2000",

}

Bella, G, Massacci, F, Paulson, LC & Tramontano, P 2000, Formal verification of cardholder registration in SET. in F Cuppens, Y Deswarte, D Gollmann & M Waidner (eds), Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Verlag, pp. 159-174, 6th European Symposium on Research in Computer Security, ESORICS 2000, Toulouse, France, 4/10/00. https://doi.org/10.1007/10722599_10

Formal verification of cardholder registration in SET. / Bella, G.; Massacci, F.; Paulson, L.C. et al.
Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings. ed. / F. Cuppens; Y. Deswarte; D. Gollmann; M. Waidner. Springer Verlag, 2000. p. 159-174 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formal verification of cardholder registration in SET

AU - Bella, G.

AU - Massacci, F.

AU - Paulson, L.C.

AU - Tramontano, P.

PY - 2000

Y1 - 2000

N2 - © Springer-Verlag Berlin Heidelberg 2000.The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.

AB - © Springer-Verlag Berlin Heidelberg 2000.The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.

UR - https://www.scopus.com/pages/publications/84944035753

UR - https://www.scopus.com/inward/citedby.url?scp=84944035753&partnerID=8YFLogxK

U2 - 10.1007/10722599_10

DO - 10.1007/10722599_10

M3 - Conference contribution

SN - 3540410317

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 159

EP - 174

BT - Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings

A2 - Cuppens, F.

A2 - Deswarte, Y.

A2 - Gollmann, D.

A2 - Waidner, M.

PB - Springer Verlag

T2 - 6th European Symposium on Research in Computer Security, ESORICS 2000

Y2 - 4 October 2000 through 6 October 2000

ER -

Bella G, Massacci F, Paulson LC, Tramontano P. Formal verification of cardholder registration in SET. In Cuppens F, Deswarte Y, Gollmann D, Waidner M, editors, Computer Security - 6th European Symposiumon Research in Computer Security, ESORICS 2000, Proceedings. Springer Verlag. 2000. p. 159-174. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/10722599_10

Formal verification of cardholder registration in SET

Abstract

Publication series

Conference

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this