Minimal backups of cryptographic protocol runs

As cryptographic protocols execute they accumulate information such as values and keys, and evidence of properties about this information. As execution proceeds, new information becomes relevant while some old information ceases to be of use. Identifying what information is necessary at each point in a protocol run is valuable for both analysis and deployment. We formalize this necessary information as the minimal backup of a protocol. We present an analysis that determines the minimal backup at each point in a protocol run. We show that this minimal backup has many uses: it serves as a foundation for job-migration and other kinds of faulttolerance, and also assists protocol designers understand the structure of protocols and identify potential flaws. In a cryptographic context it is dangerous to reason informally. We have therefore formalized and verified this work using the Coq proof assistant. Additionally, Coq provides a certified implementation of our analysis. Concretely, our an...

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: Jay A. McCarthy, Shriram Krishnamurthi
• Keywords: CCS 2008, Cryptographic Protocols, Minimal Backup, Protocol Run, Security Privacy