Verifying Secrecy by Abstract Interpretation(2)

cryptographic protocols.Lecture Notes in Computer Science,1427:77–??,1998.

[4]J.Clark et J.Jacob.A survey on authenti?cation protocol.http://www.cs.york.ac.uk/?jac/

papers/drareviewps.ps,1997.

[5]E.M.Clarke,S.Jha,and ing state space exploration and a natural deduction style message

derivation engine to verify security protocols.In IFIP Working Conference on Programming Concepts and Methods(PROCOMET),1998.

[6]on,V.Cortier,and J.Mitchell.Tree automata with one memory,set constraints,and ping-

pong protocols.In Automata,Languages and Programming,28th International Colloquium,ICALP 2001,Crete,Greece,July8-12,2001,Proceedings,volume2076of Lecture Notes in Computer Science.

Springer,2001.

[7]on et V.Shmatikov.Is it possible to decide whether a cryptographic protocol is secure or not?

Journal of Telecommunications and Information Technology.,para??tre,2002.

[8]V.Cortier,J.Millen,and H.Rueß.Proving secrecy is easy enough.In Proc.14th IEEE Computer Security

Foundations Workshop(CSFW’01),Cape Breton,Nova Scotia,Canada,June2001,pages97–110.IEEE Comp.Soc.Press,2001.

[9]N.Durgin,P.Lincoln,J.Mitchell,and A.Scedrov.Undecidability of bounded security protocols.In

N.Heintze and Proceedings E.Clarke,editors,editors,Workshop on Formal Methods and Security Protocols—FMSP,Trento,Italy,July1999.,1999.

[10]S.Even et O.Goldreich.On the security of multi-party ping pong protocols.Technical report,Israel

Institute of Technology,1983.

[11]T.Genet et F.Klay.Rewriting for Cryptographic Protocol Veri?cation.In Proceedings17th International

Conference on Automated Deduction,volume1831of Lecture Notes in Arti?cial Intelligence.Springer-Verlag,2000.

[12]Jean Goubault-Larrecq.A method for automatic cryptographic protocol veri?cation.In Dominique M´e ry,

Beverly Sanders,editors,Fifth International Workshop on Formal Methods for Parallel Programming: Theory and Applications(FMPPTA2000),number1800in Lecture Notes in Computer Science.Springer-Verlag,2000.

[13]G.Lowe.An attack on the Needham-Schroeder public-key authenti?cation rmation

Processing Letters,56(3):131–133,November1995.

[14]G.Lowe.Breaking and?xing the Needham-Schroeder public-key protocol using fdr.In TACAS,number

1055in Lecture Notes in Computer Science,pages147–166,1996.

[15]C.Meadows.Invariant generation techniques in cryptographic protocol analysis.In PCSFW:Proceedings

of The13th Computer Security Foundations Workshop.IEEE Computer Society Press,2000.

[16]J.Millen et V.Shmatikov.Constraint solving for bounded-process cryptographic protocol analysis.In

Proc.8th ACM Conference on Computer and Communications Security(CCS’01),pages166–175,2001.

[17]J.C.Mitchell,M.Mitchell,et U.Stern.Automated analysis of cryptographic protocols using mur.In

Proceedings of the1997Conference on Security and Privacy(S&P-97),pages141–153,Los Alamitos, May4–71997.IEEE Press.

[18]D.Monniaux.Decision procedures for the analysis of cryptographic protocols by logics of belief.In12th

Computer Security Foundations Workshop.IEEE,1999.

117

Verifying Secrecy by Abstract Interpretation

Bozga,Lakhnech,P´e rin

[19]R.M.Needham and ing encryption for authentication in large networks of computers.

CACM,21(12):993–999,1978.

[20]L.Paulson.Proving properties of security protocols by induction.In10th IEEE Computer Security

Foundations Workshop(CSFW’97),pages70–83,June1997.IEEE.

[21]M.Rusinowitch and M.Turuani.Protocol insecurity with?nite number of sessions is np-complete.In

14th IEEE Computer Security Foundations Workshop(2001),pp.174–190.,2001.

[22]S.Schneider.Verifying authentication protocols with CSP.In10th IEEE Computer Security Foundations

Workshop(CSFW’97),pages3–17,June1997.IEEE.

118