Prof. Dr. Jan Jürjens - Veröffentlichungen nach Thema
Sichere Softwareentwicklung - Code-Sicherheits-Analyse

Disclaimer

• F. Dupressoir, A. D. Gordon, J. Jürjens, D. Naumann: Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. In: Journal of Computer Security, vol. 22, no. 5, pp. 823-866, 2014. Special issue with best papers from the 24th IEEE Computer Security Foundations Symposium (CSF).
  @Article{DGJN14, author = {F.~Dupressoir and A. D.~Gordon and J.~J{\"u}rjens and D.~Naumann}, title = {Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols}, journal = {Journal of Computer Security}, volume = {22}, number = {5}, pages = {823--866}, year = {2014}, note = {Special issue with best papers from the 24th IEEE Computer Security Foundations Symposium (CSF)}, file = {preprint:http\://arxiv.org/abs/1312.6532:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, DOI = {10.3233/JCS-140508}, keywords = {selectedPub,modelbasedSecurityEngineering,secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   preprint   dblp 
• M. Aizatulin, A. D. Gordon, J. Jürjens: Computational Verification of C Protocol Implementations by Symbolic Execution. In: 19th ACM Conference on Computer and Communications Security (CCS 2012), ACM, pp. 712-723, 2012.
  @InProceedings{ccs12AGJ, author = {M.~Aizatulin and A. D.~Gordon and J.~J{\"u}rjens}, title = {Computational Verification of C Protocol Implementations by Symbolic Execution}, booktitle = {19th ACM Conference on Computer and Communications Security (CCS 2012)}, year = {2012}, pages = {712--723}, DOI = {http://doi.acm.org/10.1145/2382196.2382271}, publisher = {ACM}, file = {slides:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/slides/ccs12AGJslides.pdf:URL;preprint:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/papers/ccs12AGJ.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {selectedPub,internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis,vorsecurestreams}, }

   BibTeX   DOI   slides   preprint   dblp 
• M. Aizatulin, A. D. Gordon, J. Jürjens: Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. In: 18th ACM Conference on Computer and Communications Security (CCS 2011), pp. 331-340, 2011.
  @InProceedings{ccs11AGJ, author = {M.~Aizatulin and A. D.~Gordon and J.~{J}{\"u}{r}jens}, title = {Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution}, booktitle = {18th ACM Conference on Computer and Communications Security (CCS 2011)}, year = {2011}, pages = {331--340}, crossref = {DBLP:conf/ccs/2011}, DOI = {http://doi.acm.org/10.1145/2046707.2046745}, file = {preprint:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/papers/ccs11AGJ.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL;slides:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/slides/ccs11AGJslides.pdf:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis,vorsecurestreams}, }

   BibTeX   DOI   preprint   dblp   slides 
• M. Aizatulin, F. Dupressoir, A. D. Gordon, J. Jürjens: Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. In: 8th International Workshop on Formal Aspects of Security & Trust (FAST2011), pp. 1-20, 2011.
  @Conference{fast11ADGJ, author = {M.~Aizatulin and F.~Dupressoir and A. D.~Gordon and J.~{J}{\"u}{r}jens}, title = {Verifying Cryptographic Code in C: Some Experience and the Csec Challenge}, booktitle = {8th International Workshop on Formal Aspects of Security \& Trust (FAST2011)}, year = {2011}, pages = {1--20}, file = {preprint:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/papers/fast11ADGJ.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL;SpringerLink:http://link.springer.com/chapter/10.1007/978-3-642-29420-4_1:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis, invitedWorkshop}, }

   BibTeX   preprint   dblp   SpringerLink 
• Mihhail Aizatulin, Andrew D. Gordon, J. Jürjens: Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution. In: CoRR, vol. abs/1107.1017, pp. 331-340, 2011.
  @Article{evcm11a, author = {Mihhail Aizatulin and Andrew D. Gordon and J.~{J}{\"u}{r}jens}, title = {Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution}, journal = {CoRR}, year = {2011}, volume = {abs/1107.1017}, pages = {331--340}, DOI = {http://arxiv.org/abs/1107.1017}, file = {dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   dblp 
• F. Dupressoir, A. D. Gordon, J. Jürjens, D. A. Naumann: Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. In: 24th IEEE Computer Security Foundations Symposium (CSF), pp. 3-17, 2011.
  @InProceedings{csf11DGJN, author = {F.~Dupressoir and A. D.~Gordon and J.~{J}{\"u}{r}jens and D. A.~Naumann}, title = {Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols}, booktitle = {24th IEEE Computer Security Foundations Symposium (CSF)}, year = {2011}, pages = {3--17}, DOI = {http://doi.ieeecomputersociety.org/10.1109/CSF.2011.8}, file = {preprint:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/papers/csf11DGJN.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL;slides:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/slides/csf11DGJNtalk.pdf:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis,vorsecurestreams}, URL = {http://research.microsoft.com/apps/pubs/?id=147704}, }

   BibTeX   DOI   URL   preprint   dblp   slides 
• M. Aizatulin, A. D. Gordon, J. Jürjens: Cryptographic Security Verification for C by Symbolic Execution. In: Computer Security Foundations Symposium (CSF), 2010. 5-minute presentation.
  @InProceedings{csvc10, author = {M.~Aizatulin and A. D.~Gordon and J.~{J}{\"u}{r}jens}, title = {Cryptographic Security Verification for C by Symbolic Execution}, booktitle = {Computer Security Foundations Symposium (CSF)}, year = {2010}, note = {5-minute presentation}, file = {preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/csf10.pdf:URL}, keywords = {workshop, industrialConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   preprint 
• F. Dupressoir, A. D. Gordon, J. Jürjens: Verifying authentication properties of C security protocol code using general verifiers. In: Fourth International Workshop on Analysis of Security APIs,, 2010.
  @InProceedings{vapc10, author = {F.~Dupressoir and A. D.~Gordon and J.~{J}{\"u}{r}jens}, title = {Verifying authentication properties of C security protocol code using general verifiers}, booktitle = {Fourth International Workshop on Analysis of Security APIs,}, year = {2010}, file = {preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/asa4.pdf:URL;slides:http\://rgse.uni-koblenz.de/web/pages/people/juerjens/publications/slides/5-dupressoir.pdf:URL}, keywords = {industrialConferences, workshop, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   preprint   slides 
• J. Jürjens: Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project. In: Electr. Notes Theor. Comput. Sci., vol. 250, no. 1, pp. 123-136, 2009.
  @Article{DBLP:journals/entcs/Jurjens09, author = {J.~{J}{\"u}{r}jens}, title = {Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project}, journal = {Electr. Notes Theor. Comput. Sci.}, year = {2009}, volume = {250}, pages = {123--136}, number = {1}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVOCS 2007)}, file = {dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, DOI = {http://doi.org/10.1016/j.entcs.2009.08.009}, keywords = {electronicJournals, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   dblp 
• J. Jürjens, Yijun Yu, A. Bauer: Tools for Traceable Security Verification. In: BCS Visions of Computer Science Conference, pp. 367-390, 2008.
  @InProceedings{ttsc08, author = {J.~{J}{\"u}{r}jens and Yijun Yu and A.~Bauer}, title = {Tools for Traceable Security Verification}, booktitle = {BCS Visions of Computer Science Conference}, year = {2008}, pages = {367--390}, crossref = {DBLP:conf/bcs/2008}, DOI = {http://www.bcs.org/server.php?show=ConWebDoc.22980}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/bcs08talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/bcs08.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint   dblp 
• J. Jürjens: Linking Cryptoprotocol Verification to Reality. In: Annual Meeting of the Working Group on Formal Methods and Software Engineering for Safety and Security (German Computer Society), Darmstadt (Germany), 2008.
  @InProceedings{lcvr08, author = {J.~{J}{\"u}{r}jens}, title = {Linking Cryptoprotocol Verification to Reality}, booktitle = {Annual Meeting of the Working Group on Formal Methods and Software Engineering for Safety and Security (German Computer Society)}, year = {2008}, address = {Darmstadt (Germany)}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/fomsess08talk.pdf:URL}, keywords = {workshop, industrialConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   slides 
• J. Jürjens: Towards Verified Crypto-Protocol Implementations: The Java Secure Sockets Extension. In: ABZ 2008 VSRnet Workshop, 2008.
  @InProceedings{tvcpi08, author = {J.~{J}{\"u}{r}jens}, title = {Towards Verified Crypto-Protocol Implementations: The Java Secure Sockets Extension}, booktitle = {ABZ 2008 VSRnet Workshop}, year = {2008}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/vsrnet08talk.pdf:URL}, keywords = {workshop, industrialConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   slides 
• J. Jürjens: Using Interface Specifications for Verifying Crypto-protocol Implementations. In: Foundations of Interface Technologies 2008 (FIT`08 @ ETAPS 2008), 2008.
  @InProceedings{uisvcpi08, author = {J.~{J}{\"u}{r}jens}, title = {Using Interface Specifications for Verifying Crypto-protocol Implementations}, booktitle = {Foundations of Interface Technologies 2008 (FIT`08 @ ETAPS 2008)}, year = {2008}, DOI = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.2736}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/fit08talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/fit08.pdf:URL}, keywords = {industrialConferences, workshop, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint 
• J. Jürjens: Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project. In: Seventh International Workshop on Automated Verification of Critical Systems (AVOCS 2007), Oxford, 2007.
  @InProceedings{asvspi07, author = {J.~{J}{\"u}{r}jens}, title = {Automated Security Verification for Crypto Protocol Implementations: Verifying the {Jessie} Project}, booktitle = {Seventh International Workshop on Automated Verification of Critical Systems (AVOCS 2007)}, year = {2007}, address = {Oxford}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/avocs07talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/avocs07.pdf:URL}, keywords = {workshop, industrialConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   slides   preprint 
• J. Jürjens: Security Analysis of Crypto-based Java Programs using Automated Theorem Provers. In: S. Easterbrook, S. Uchitel (editors): 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), ACM, pp. 167-176, 2006.
  @InProceedings{sacbjp06, author = {J.~{J}{\"u}{r}jens}, title = {Security Analysis of Crypto-based Java Programs using Automated Theorem Provers}, booktitle = {21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006)}, year = {2006}, editor = {S.~Easterbrook and S.~Uchitel}, pages = {167--176}, publisher = {ACM}, DOI = {http://doi.org/10.1109/ASE.2006.60}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/ase06talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/ase06.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint   dblp 
• J. Jürjens, M. Yampolskiy: Code security analysis with assertions. In: 20th International Conference on Automated Software Engineering (ASE 2005), IEEE/ACM, pp. 392-395, 2005.
  @InProceedings{ase05, author = {J.~{J}{\"u}{r}jens and M.~Yampolskiy}, title = {Code security analysis with assertions}, booktitle = {20th International Conference on Automated Software Engineering (ASE 2005)}, year = {2005}, pages = {392--395}, publisher = {IEEE/ACM}, DOI = {http://doi.acm.org/10.1145/1101908.1101978}, file = {preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/ase05.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   preprint   dblp 
• J. Jürjens: Code Security Analysis of a Biometric Authentication System Using Automated Theorem Provers. In: 21st Annual Computer Security Applications Conference (ACSAC 2005), pp. 138-149, Institute of Electrical and Electronics Engineers, 2005.
  @InProceedings{csabas05, author = {J.~{J}{\"u}{r}jens}, title = {Code Security Analysis of a Biometric Authentication System Using Automated Theorem Provers}, booktitle = {21st Annual Computer Security Applications Conference (ACSAC 2005)}, year = {2005}, pages = {138--149}, organization = {Institute of Electrical and Electronics Engineers}, DOI = {http://doi.org/10.1109/CSAC.2005.15}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/acsac05talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/acsac05.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint   dblp 
• J. Jürjens: Verification of Low-level Crypto-Protocol Implementations Using Automated Theorem Proving. In: 3rd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005), pp. 89-98, Institute of Electrical and Electronics Engineers, 2005.
  @InProceedings{memocode05J, author = {J.~{J}{\"u}{r}jens}, title = {Verification of Low-level Crypto-Protocol Implementations Using Automated Theorem Proving}, booktitle = {3rd ACM \& IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2005)}, year = {2005}, pages = {89--98}, organization = {Institute of Electrical and Electronics Engineers}, alt_note = {Technical report with additional material accessible at \URL{http://www4.in.tum.de/$\tilde{\ }$juerjens/pkcs11results}}, DOI = {http://doi.org/10.1109/MEMCOD.2005.1487898}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/memocode05talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/memocode05.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint   dblp 
• J. Jürjens: Understanding Security Goals Provided by Crypto-Protocol Implementations. In: 21st International Conference on Software Maintenance (ICSM 2005), pp. 643-646, Institute of Electrical and Electronics Engineers, 2005.
  @InProceedings{usgpcpi05, author = {J.~{J}{\"u}{r}jens}, title = {Understanding Security Goals Provided by Crypto-Protocol Implementations}, booktitle = {21st International Conference on Software Maintenance (ICSM 2005)}, year = {2005}, pages = {643--646}, organization = {Institute of Electrical and Electronics Engineers}, alt_note = {Technical report with additional material accessible at \URL{http://www4.in.tum.de/$\tilde{\ }$juerjens/opensslresults}}, DOI = {http://doi.org/10.1109/ICSM.2005.97}, file = {slides:http\://rgse.uni-koblenz.de/jj/publications/papers/icsm05talk.pdf:URL;preprint:http\://rgse.uni-koblenz.de/jj/publications/papers/icsm05.pdf:URL;dblp:http://dblp.uni-trier.de/pers/hd/j/J=uuml=rjens:Jan:URL}, keywords = {internationalConferences, secureSoftwareEngineeringCodeSecurityAnalysis}, }

   BibTeX   DOI   slides   preprint   dblp