We give an abstraction of verifiable multi-secret sharing schemes that is accessible to a fully mechanized analysis. This abstraction is formalized within the applied pi-calculus by using an equational theory which characterizes the cryptographic semantics of secret share. We also present an encoding from the equational theory into a convergent rewriting system, which is suitable for the automated protocol verifier ProVerif. Based on that, we verify the threshold certificate protocol in ProVerif.
|Number of pages||12|
|Journal||International Journal of Computational Intelligence Systems|
|Publication status||Published - Feb 2012|
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Computational Mathematics