@COMMENT{{{This file has been generated by bib2bib 1.74}}
@COMMENT{{{Command line: /usr/bin/bib2bib -ob 2004-secu.bib -c 'gvcat :"secu"' bibs/2004.bib}}
@INPROCEEDINGS{dg04,
AUTHOR = {Giorgio Delzanno and Pierre Ganty},
TITLE = {{Automatic Verification of Time Sensitive Cryptographic Protocols}},
BOOKTITLE = {Proc. of Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems ({TACAS}'04)},
YEAR = 2004,
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag},
VOLUME = 2988,
PAGES = {342--356},
GVCAT = {secu}
}
@INPROCEEDINGS{ChadhaKremerScedrov2004,
ABSTRACT = {We analyze the multi-party contract-signing protocols
of Garay and MacKenzie (GM) and of Baum and Waidner
(BW). We use a finite-state tool, {\scshape Mocha},
which allows specification of protocol properties in
a branching-time temporal logic with game semantics.
While our analysis does not reveal any errors in the
BW protocol, in the GM protocol we discover serious
problems with fairness for four signers and an
oversight regarding abuse-freeness for three signers.
We propose a complete revision of the GM subprotocols
in order to restore fairness.},
ADDRESS = {Barcelona, Spain},
AUTHOR = {Chadha, Rohit and Kremer, Steve and Scedrov, Andre},
BOOKTITLE = {{P}roceedings of the 4th {IFIP} {WG1.7} {W}orkshop on
{I}ssues in the {T}heory of {S}ecurity ({WITS}'04)},
MONTH = APR,
TITLE = {Formal Analysis of Multi-Party Contract Signing},
YEAR = {2004},
MONTH = APR,
GVCAT = {secu}
}
@INPROCEEDINGS{ChadhaKremerScedrov2004b,
ABSTRACT = {We analyze the multi-party contract-signing protocols
of Garay and MacKenzie (GM) and of Baum and Waidner
(BW). We use a finite-state tool, {\scshape Mocha},
which allows specification of protocol properties in
a branching-time temporal logic with game semantics.
While our analysis does not reveal any errors in the
BW protocol, in the GM protocol we discover serious
problems with fairness for four signers and an
oversight regarding abuse-freeness for three signers.
We propose a complete revision of the GM subprotocols
in order to restore fairness.},
ADDRESS = {Asilomar, Pacific Grove, California, USA},
AUTHOR = {Chadha, Rohit and Kremer, Steve and Scedrov, Andre},
BOOKTITLE = {{P}roceedings of the 17th {IEEE} {C}omputer
{S}ecurity {F}oundations {W}orkshop ({CSFW}'04)},
MONTH = JUN,
PAGES = {266-279},
PUBLISHER = {{IEEE} Computer Society Press},
TITLE = {Formal Analysis of Multi-Party Contract Signing},
YEAR = {2004},
MONTH = JUN,
GVCAT = {secu}
}
@INPROCEEDINGS{KremerRyan2004,
ABSTRACT = {In this paper we report on an analysis for finding
known-pair and chosen-text attacks in protocols. As
these attacks are at the level of blocks, we extend
the attacker by special capabilities related to block
chaining techniques. The analysis is automated using
Blanchet's protocol verifier and illustrated on two
well-known protocols, the Needham-Schroeder-Lowe
public-key protocol as well as the Needham-Schroeder
symmetric-key protocol. On the first protocol, we
show how the special intruder capabilities related to
chaining may compromise the secrecy of nonces and
that chosen-ciphertext attacks are possible. We
propose two modified versions of the protocol which
strengthen its security. We then illustrate
known-pair and chosen-plaintext attacks on the second
protocol.},
ADDRESS = {London, UK},
AUTHOR = {Kremer, Steve and Ryan, Mark D.},
BOOKTITLE = {{P}roceedings of the 2nd {I}nternational {W}orkshop
on {S}ecurity {I}ssues in {C}oordination {M}odels,
{L}anguages and {S}ystems ({SecCo}'04)},
PUBLISHER = {Elsevier Science Publishers},
SERIES = {Electronic Notes in Theoretical Computer Science},
TITLE = {Analysing the Vulnerability of Protocols to produce
known-pair and chosen-text attacks},
YEAR = {2004},
MONTH = AUG,
GVCAT = {secu}
}
@INPROCEEDINGS{KremerMukhamedovRitter2005,
ABSTRACT = {Multi-party protocol with fairness is a cryptographic
protocol allowing several parties to exchange
commodities in such a way that everyone gives an item
away if and only if it receives an item in return. In
this paper we discuss a multi-party fair exchange
protocol originally proposed by Franklin and Tsudik,
and subsequently shown to have flaws and fixed by
Gonz\'alez and Markowitch. We identify flaws in a
fixed version of the protocol, propose a corrected
version, and use strand spaces formal method to prove
fairness guarantee of the corrected protocol.},
ADDRESS = {Roseau, The Commonwealth Of Dominica},
AUTHOR = {Kremer, Steve and Mukhamedov, Aybek and Ritter, Eike},
BOOKTITLE = {{P}roceedings of the 9th {I}nternational {C}onference
on {F}inancial {C}ryptography and {D}ata {S}ecurity
({FC}'05)},
MONTH = FEB # {-} # MAR,
NOTE = {To appear},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
TITLE = {Analysis of a Multi-Party Fair Exchange Protocol and
Formal Proof of Correctness in the Strand Space
Model},
YEAR = {2005},
MONTH = FEB,
GVCAT = {secu}
}
@INPROCEEDINGS{KremerRyan2005,
ABSTRACT = {Electronic voting promises the possibility of a
convenient, efficient and secure facility for
recording and tallying votes in an election. Recently
highlighted inadequacies of implemented systems have
demonstrated the importance of formally verifying the
underlying voting protocols. The applied pi calculus
is a formalism for modelling such protocols, and
allows us to verify properties by using automatic
tools, and to rely on manual proof techniques for
cases that automatic tools are unable to handle. We
model a known protocol for elections known as FOO~92
in the applied pi calculus, and we formalise three of
its expected properties, namely fairness,
eligibility, and privacy. We use the ProVerif tool to
prove that the first two properties are satisfied. In
the case of the third property, ProVerif is unable to
prove it directly, because its ability to prove
observational equivalence between processes is not
complete. We provide a manual proof of the required
equivalence.},
ADDRESS = {Edinburgh, U.K.},
AUTHOR = {Kremer, Steve and Ryan, Mark D.},
BOOKTITLE = {{P}roceedings of the 14th {E}uropean {S}ymposium on
{P}rogramming ({ESOP}'05)},
MONTH = APR,
NOTE = {To Appear},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
TITLE = {Analysis of an Electronic Voting Protocol in the
Applied Pi-Calculus},
YEAR = {2005},
MONTH = APR,
GVCAT = {secu}
}
This file has been generated by bibtex2html 1.74