We revise a known attack on the PIN verification framework, based on a weakness of the underlying security API. We specify this flawed API in an imperative language with cryptographic primitives and we show why its type-based verification fails in the type system of Myers, Sabelfeld and Zdancewic. We propose an improved API, extend the type system with cryptographic primitives for assuring integrity, and show our new API to be type-checkable.
Type-based Analysis of Financial APIs (extended abstract)
FOCARDI, Riccardo;LUCCIO, Flaminia;
2009-01-01
Abstract
We revise a known attack on the PIN verification framework, based on a weakness of the underlying security API. We specify this flawed API in an imperative language with cryptographic primitives and we show why its type-based verification fails in the type system of Myers, Sabelfeld and Zdancewic. We propose an improved API, extend the type system with cryptographic primitives for assuring integrity, and show our new API to be type-checkable.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
cfls-wits.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
Accesso chiuso-personale
Dimensione
215.56 kB
Formato
Adobe PDF
|
215.56 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
