The analysis of cryptographic APIs using the theorem prover Otter
Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2005
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/18001 |
| _version_ | 1826205079072407552 |
|---|---|
| author | Youn, Paul, 1981- |
| author2 | Ronald Rivest. |
| author_facet | Ronald Rivest. Youn, Paul, 1981- |
| author_sort | Youn, Paul, 1981- |
| collection | MIT |
| description | Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. |
| first_indexed | 2024-09-23T13:06:24Z |
| format | Thesis |
| id | mit-1721.1/18001 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:06:24Z |
| publishDate | 2005 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/180012019-04-11T14:03:50Z The analysis of cryptographic APIs using the theorem prover Otter Analysis of cryptographic application programming interfaces using the theorem prover Otter Youn, Paul, 1981- Ronald Rivest. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (M. Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2004. Includes bibliographical references (p. 79-81). In 2000, Bond and Anderson exposed a new family of attacks on application programming interfaces (APIs) of security modules. These attacks elicit compromising behaviors using an unexpected sequence of legal calls to the module, uncovering severe security flaws even in widely-deployed cryptographic hardware. Because these attacks do not depend on the underlying ryptographic mechanisms, they often succeed even under the assumption of ideal cryptographic primitives. This thesis presents a methodology for the automatic detection of API attacks. Taking a cue from previous work on the formal analysis of security protocols and noting these attacks' independence from precise cryptographic mechanisms, we model APIs opaquely, purely according to specifications. We use a theorem prover tool and adapt it to the security API context. Several specifications of Cryptographic APIs are implemented for analysis using a theorem prover known as OTTER. These implementations successfully found known attacks, and provide evidence that OTTER will also be able to find new attacks, and perhaps eventually verify security in arbitrary Cryptographic APIs. Based on these implementations, various strategies, potential problems, and solutions are discussed that can be applied towards the formal analysis of Cryptographic APIs. We detail how, using these formalization and automation techniques, we have confirmed a number of known attacks and exposed an undocumented behavior of the IBM 4758 CCA, a hardware add-on crucial to a large portion of banking transactions worldwide. We show how the confirmed attacks' complexity and unintuitiveness make a very strong case for continued focus on automated formal verification of cryptographic APIs. by Paul Youn. M.Eng. 2005-06-02T19:34:42Z 2005-06-02T19:34:42Z 2004 2004 Thesis http://hdl.handle.net/1721.1/18001 57204175 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 81 p. 3655429 bytes 3664202 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Youn, Paul, 1981- The analysis of cryptographic APIs using the theorem prover Otter |
| title | The analysis of cryptographic APIs using the theorem prover Otter |
| title_full | The analysis of cryptographic APIs using the theorem prover Otter |
| title_fullStr | The analysis of cryptographic APIs using the theorem prover Otter |
| title_full_unstemmed | The analysis of cryptographic APIs using the theorem prover Otter |
| title_short | The analysis of cryptographic APIs using the theorem prover Otter |
| title_sort | analysis of cryptographic apis using the theorem prover otter |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/18001 |
| work_keys_str_mv | AT younpaul1981 theanalysisofcryptographicapisusingthetheoremproverotter AT younpaul1981 analysisofcryptographicapplicationprogramminginterfacesusingthetheoremproverotter AT younpaul1981 analysisofcryptographicapisusingthetheoremproverotter |