2003, English, Article edition: Verification of cryptographic protocols implemented in Java Card Marlet, Renaud; Le Métayer, Daniel

User activity

Share to:
 
Bookmark: http://trove.nla.gov.au/version/203904
Physical Description
  • text
Published
  • HAL - CCSD
  • 2003
Language
  • English

Edition details

Title
  • Verification of cryptographic protocols implemented in Java Card
Author
  • Marlet, Renaud
  • Le Métayer, Daniel
Published
  • HAL - CCSD
  • 2003
Physical Description
  • text
Subjects
Notes
  • A large number of cryptographic protocols have been specified and implemented. However, many of them have been shown to be flawed, even long after they were published. This has generated a line of works concerning the formal specification and verification of protocols, e.g., Casper, Capsl, Casrul. Still, all these techniques and tools are based on conceptual views (or models) of protocols and provide no guarantee on their actual implementation. This paper reports on a method and analysis tool whose goal is precisely to bridge the gap between protocol models that can be proven flawless and their implementation. Our target in this work is Java Card applets: In this case, applications on a card represent principals involved in authentication protocols, with strong security requirements. We have defined a domain-specific language, called DEXTRA, for expressing requirements regarding the implementation of a protocol in Java Card. We have also developed a prototype analyzer to verify the compliance of a Java Card applet with respect to such a specification of a protocol implementation. The verifier relies on static program analysis techniques.
  • HAL:hal-00306305, version 1
  • HAL:http:/​/​hal.archives-ouvertes.fr/​hal-00306305/​en/​
Language
  • English
Contributed by
OAIster

Get this edition

  • Set up My libraries

    How do I set up "My libraries"?

    In order to set up a list of libraries that you have access to, you must first login or sign up. Then set up a personal list of libraries from your profile page by clicking on your user name at the top right of any screen.

  • All (1)
  • Unknown (1)
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.

User activity


e.g. test cricket, Perth (WA), "Parkes, Henry"

Separate different tags with a comma. To include a comma in your tag, surround the tag with double quotes.

Be the first to add a tag for this edition

Be the first to add this to a list

Comments and reviews

What are comments? Add a comment

No user comments or reviews for this version

Add a comment