Cryptographic types
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Cryptographic types are a way to express cryptographic guarantees (of secrecy and integrity) in a type system for a network programming language. This allows some of these guarantees to be checked statically, before a network program executes. Where dynamic checks are required, these are represented at the source language level as dynamic type-checking, and are translated by the compiler to lower level cryptographic operations. Static checking avoids the unnecessary overhead of run-time cryptographic operations where communication is through a trusted medium (e.g. the OS kernel, or a trusted subnet), and also provides static guarantees of the reliability of a network application. Cryptographic types can also be used to build application-specific security protocols, where type-checking in the lower layers of the protocol stack verifies security properties for upper layers. Cryptographic types are described formally using a process calculus, the ec-calculus. Correctness is verified for a scheme for compiling type operations to cryptographic operations.Keywords
This publication has 29 references indexed in Scilit:
- Logical relations for encryptionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- A semantic model for authentication protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Complete, safe information flow with decentralized labelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Information flow inference for freePublished by Association for Computing Machinery (ACM) ,2000
- Trust and partial typing in open systems of mobile agentsPublished by Association for Computing Machinery (ACM) ,1999
- On bisimulations for the asynchronous π-calculusTheoretical Computer Science, 1998
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- An asynchronous model of locality, failure, and process mobilityPublished by Springer Nature ,1997
- Safe kernel extensions without run-time checkingACM SIGOPS Operating Systems Review, 1996
- Authentication for distributed systemsComputer, 1992