An example of proving UC-realization with formal methods

S. Andova; K. Gjøsteen; L. Kråkmo; S. F. Mjølsnes; S. Radomirović

An example of proving UC-realization with formal methods

S. Andova
, K. Gjøsteen
, L. Kråkmo
, S. F. Mjølsnes
, S. Radomirović

Computing

Research output: Contribution to conference › Paper

83 Downloads (Pure)

Abstract

In the universal composability framework we consider ideal functionalities for secure messaging and signcryption. Using traditional formal methods techniques we show that the secure messaging functionality can be UC-realized by a hybrid protocol that uses the signcryption functionality and a public key infrastructure functionality. We also discuss that the signcryption functionality can be UC-realized by a secure signcryption scheme.

Original language	English
Pages	46-54
Number of pages	9
Publication status	Published - 9 Jul 2006
Event	2nd Workshop on Formal and Computational Cryptography - Venice, Italy Duration: 9 Jul 2006 → 9 Jul 2006

Workshop

Workshop	2nd Workshop on Formal and Computational Cryptography
Abbreviated title	FCC 2006
Country/Territory	Italy
City	Venice
Period	9/07/06 → 9/07/06
Other	Co-located with ICALP'06 and CSFW'06

Access to Document

Final Published VersionFinal published version, 633 KB

Cite this

@conference{b4f879259099415090e2a127f0bddc98,

title = "An example of proving UC-realization with formal methods",

abstract = "In the universal composability framework we consider ideal functionalities for secure messaging and signcryption. Using traditional formal methods techniques we show that the secure messaging functionality can be UC-realized by a hybrid protocol that uses the signcryption functionality and a public key infrastructure functionality. We also discuss that the signcryption functionality can be UC-realized by a secure signcryption scheme. ",

author = "S. Andova and K. Gj{\o}steen and L. Kr{\aa}kmo and Mj{\o}lsnes, \{S. F.\} and S. Radomirovi{\'c}",

note = "No funding info; 2nd Workshop on Formal and Computational Cryptography, FCC 2006 ; Conference date: 09-07-2006 Through 09-07-2006",

year = "2006",

month = jul,

day = "9",

language = "English",

pages = "46--54",

}

TY - CONF

T1 - An example of proving UC-realization with formal methods

AU - Andova, S.

AU - Gjøsteen, K.

AU - Kråkmo, L.

AU - Mjølsnes, S. F.

AU - Radomirović, S.

N1 - No funding info

PY - 2006/7/9

Y1 - 2006/7/9

N2 - In the universal composability framework we consider ideal functionalities for secure messaging and signcryption. Using traditional formal methods techniques we show that the secure messaging functionality can be UC-realized by a hybrid protocol that uses the signcryption functionality and a public key infrastructure functionality. We also discuss that the signcryption functionality can be UC-realized by a secure signcryption scheme.

AB - In the universal composability framework we consider ideal functionalities for secure messaging and signcryption. Using traditional formal methods techniques we show that the secure messaging functionality can be UC-realized by a hybrid protocol that uses the signcryption functionality and a public key infrastructure functionality. We also discuss that the signcryption functionality can be UC-realized by a secure signcryption scheme.

M3 - Paper

SP - 46

EP - 54

T2 - 2nd Workshop on Formal and Computational Cryptography

Y2 - 9 July 2006 through 9 July 2006

ER -

An example of proving UC-realization with formal methods

Abstract

Workshop

Access to Document

Fingerprint

Cite this