Loading...
Please wait, while we are loading the content...
Similar Documents
Refining Computationally Sound Mechanized Proofs for Kerberos
| Content Provider | Semantic Scholar |
|---|---|
| Author | Blanchet, Bruno Jaggard, Aaron D. Rao, J. Sunil Scedrov, Andre Tsay, Joe-Kai |
| Copyright Year | 2009 |
| Abstract | Kerberos is designed to allow a user to repeatedly authenticate herself to multiple servers based on a single login. The PKINIT extension to Kerberos modi es the initial round of the protocol to use a PKI instead of long-term shared keys (e.g., password-derived keys). Especially with PKINIT, Kerberos uses a rich collection of cryptographic operations and constructs, and Kerberos, both with and without the PKINIT extension, is used in real world settings (including Microsoft Windows). Kerberos is thus a great test case for protocol-analysis tools. The CryptoVerif prover works directly in the computational model to prove properties of protocols that are formalized as games. This talk will both survey some of our earlier work using CryptoVerif to analyze Kerberos, with and without PKINIT, and describe two recent extensions of this work. First, we brie y survey our work [1] to formalize all three rounds of Kerberos (with and without PKINIT) as games that CryptoVerif could analyze. This allowed us to prove, using CryptoVerif, authentication and secrecy properties under certain cryptographic assumptions (e.g., that the public-key encryption scheme satis es IND-CCA2 security). This work included the de nition of a version of key usability that was stronger than that originally given by Datta et al. [2]; the stronger version is amenable to being proved using CryptoVerif, and we showed that freshly generated keys in Kerberos are usable in this strong sense for IND-CCA2-secure encryption. Second, we describe more recent results that extend our initial work on key usability. We suggest the following de nition of strong key usability for INT-CTXT-secure encryption; like our strong notion of INDCCA2 usability, this de nition can be captured in the language used by CryptoVerif. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://faculty.nps.edu/gwdinolt/ProtocolExchange/Fall2009/jaggard_px_091007.pdf |
| Alternate Webpage(s) | http://prosecco.gforge.inria.fr/personal/bblanche/publications/BlanchetJaggardRaoScedrovTsayFCC09.pdf |
| Alternate Webpage(s) | http://www.di.ens.fr/~blanchet/publications/BlanchetJaggardRaoScedrovTsayFCC09.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
