|
Constructive
Cryptography
in
HOL:
the
Communication
Modeling
Aspect
Title: |
Constructive Cryptography in HOL: the Communication Modeling Aspect |
Authors:
|
Andreas Lochbihler and
S. Reza Sefidgar
|
Submission date: |
2021-03-17 |
Abstract: |
Constructive Cryptography (CC) [ICS
2011, TOSCA
2011, TCC
2016] introduces an abstract approach to composable security
statements that allows one to focus on a particular aspect of security
proofs at a time. Instead of proving the properties of concrete
systems, CC studies system classes, i.e., the shared behavior of
similar systems, and their transformations. Modeling of systems
communication plays a crucial role in composability and reusability of
security statements; yet, this aspect has not been studied in any of
the existing CC results. We extend our previous CC formalization
[Constructive_Cryptography,
CSF
2019] with a new semantic domain called Fused Resource
Templates (FRT) that abstracts over the systems communication patterns
in CC proofs. This widens the scope of cryptography proof
formalizations in the CryptHOL library [CryptHOL,
ESOP
2016, J
Cryptol 2020]. This formalization is described in Abstract
Modeling of Systems Communication in Constructive Cryptography using
CryptHOL. |
BibTeX: |
@article{Constructive_Cryptography_CM-AFP,
author = {Andreas Lochbihler and S. Reza Sefidgar},
title = {Constructive Cryptography in HOL: the Communication Modeling Aspect},
journal = {Archive of Formal Proofs},
month = mar,
year = 2021,
note = {\url{https://isa-afp.org/entries/Constructive_Cryptography_CM.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Constructive_Cryptography, Game_Based_Crypto, Sigma_Commit_Crypto |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|