@Article{Abadi98, author = {Mart{\'\i}n Abadi}, title = {On {SDSI}'s linked Local Name Spaces}, journal = {Journal of Computer Security}, year = 1998, volume = 6, number = {1--2}, pages = {3--21} } @article{AbadiBlanchet05, author = {Mart{\'\i}n Abadi and Bruno Blanchet}, title = {Analyzing Security Protocols with Secrecy Types and Logic Programs}, journal = {Journal of the ACM}, year = 2005, volume = 52, number = 1, pages = {102--146}, month = {January} } @InProceedings{AbadiEtAl04, author = {Mart{\'\i}n Abadi and Bruno Blanchet and C{\'{e}}dric Fournet}, title = {{Just Fast Keying} in the Pi Calculus}, booktitle = {Programming Languages and Systems: {ESOP} 2004 Proceedings}, pages = {340--354}, month = {January}, year = 2004, editor = {David Schmidt}, number = 2986, series = {LNCS}, publisher = {Springer Verlag} } @Article{AbadiEtAl93, author = {Mart{\'\i}n Abadi and Michael Burrows and Butler Lampson and Gordon D. Plotkin}, title = {A Calculus for Access Control in Distributed Systems}, journal = {{ACM} Transactions on Programming Languages and Systems}, year = 1993, volume = 15, number = 4, pages = {706--34}, month = {September} } @InProceedings{FioreAbadi01, author = {Marcelo Fiore and Mart{\'\i}n Abadi}, title = {Computing Symbolic Models for Verifying Cryptographic Protocols}, booktitle = {Computer Security Foundations Workshop}, year = 2001, month = {June}} @InProceedings{AbadiFournet01, author = {Mart{\'\i}n Abadi and C{\'{e}}dric Fournet}, title = {Mobile Values, New Names, and Secure Communication}, booktitle = {28th ACM Symposium on Principles of Programming Languages ({POPL} '01)}, pages = {104--115}, year = 2001, month = {January} } @article{AbadiJurjens01, author = "Mart{\'\i}n Abadi and Jan J{\"u}rjens", title = "Formal Eavesdropping and Its Computational Interpretation", journal = "Lecture Notes in Computer Science", volume = "2215", pages = "82ff.", year = "2001", url = "http://citeseer.nj.nec.com/abadi00formal.html" } @misc{AbadiJurjens00, title= {Formal Eavesdropping and its Computational Interpretation}, author= {Mart{\'{\i}}n Abadi and Jan J{\"u}rjens}, year= 2000, note= {submitted for publication}, } @Article{AbadiRogaway02, author = {Mart{\'\i}n Abadi and Phillip Rogaway}, title = {Reconciling two views of cryptography (The computational soundness of formal encryption)}, journal = {Journal of Cryptology}, year = 2002, volume = 15, number = 2, pages = {103--127}} @InProceedings{AbadiRogaway00, author = {Mart\'{\i}n Abadi and Phillip Rogaway}, title = {Reconciling two views of cryptography (The computational soundness of formal encryption)}, booktitle = {IFIP International Conference on Theoretical Computer Science (IFIP TCS2000)}, year = 2000, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag} } @InProceedings{AbadiGordon97, author = {Mart\'{\i}n Abadi and Andrew D. Gordon}, title = {A Calculus for Cryptographic Protocols: The Spi Calculus}, booktitle = {4th ACM Conference on Computer and Communications Security}, pages = {36--47}, year = 1997, month = {April}, publisher = {ACM Press}, annote = {From URL http://www.research.digital.com/SRC} } @Article{AbadiGordon99, author = {Mart\'{\i}n Abadi and Andrew D. Gordon}, title = {A Calculus for Cryptographic Protocols: The Spi Calculus}, journal = {Information and Computation}, year = 1999, volume = 148, number = 1, pages = {1--70}, month = {January} } @InProceedings{AbadiGordon97a, author = {Mart\'{\i}n Abadi and Andrew D. Gordon}, title = {Reasoning about cryptographic protocols in the spi calculus}, booktitle = {CONCUR 97}, pages = {59--73}, year = 1997, series = {Lecture Notes in Computer Science}, month = {July}, publisher = {Springer-Verlag} } @InProceedings{AbadiNeedham94, author = {Mart\'{\i}n Abadi and Roger Needham}, title = {Prudent Engineering Practice for Cryptographic Protocols}, booktitle = {Proceedings, 1994 IEEE Symposium on Research in Security and Privacy}, year = 1994, organization = {{\sc ieee}}, publisher = {{\sc ieee} CS Press}, pages = {122--136} } @InProceedings{AbadiTuttle91, author = {Mart\'{\i}n Abadi and Mark R. Tuttle}, title = {A Semantics for a Logic of Authentication}, booktitle = {Proceedings of the 10th {ACM} Symposium on Principles of Distributed Computing}, pages = {201--216}, year = 1991, month = {August} } @book{abiteboul1994foundations, title={{Foundations of Databases: The Logical Level}}, author={Abiteboul, S. and Hull, R. and Vianu, V.}, year=1994, publisher={Addison Wesley} } @article{ables2010escrowed, title={Escrowed data and the digital envelope}, author={Ables, K. and Ryan, M.}, journal={Trust and Trustworthy Computing}, pages={246--256}, year={2010}, publisher={Springer} } @Article{AbrahametalIBM91, author = "DG Abraham and GM Dolan and GP Double and JV Stevens", title = "Transaction Security Systems", journal = "IBM Systems Journal", year = 1991, volume = 30, number = 2, pages = "206--229" } @Article{Adam92, author = "J. Adam", title = "Cryptography = Privacy?", journal = "IEEE Spectrum", year = 1992, pages = "29--35", month = aug } @InProceedings{AdaoEtAl05, author = {Pedro Ad{\~a}o and Gergei Bana and Jonathan Herzog and Andre Scedrov}, title = {Soundness of Formal Encryption in the Presence of Key-Cycles}, booktitle = {Proceedings of the 10th European Symposium On Research In Computer Security {(ESORICS 2005)}}, year = 2005, month = {September} } @Article{Ajluni95, author = "C. Ajluni", title = "Two New Imagine Techniques Promise To Improve IC Defect Identification", journal = "Electronic Design", volume = "43", number = "14", month = "July", year = 1995, pages = "37--38" } @Article{Akl83, author = "Selim G. Akl", title = "Digital Signatures: A Tutorial Survey", journal = "Computer", year = 1983, pages = "15--24", month = feb } @InProceedings{AmadioLugiez00, author = {Roberto M. Amadio and Denis Lugiez}, title = {On the Reachability Problem in Cryptographic Protocols}, booktitle = {Concur}, pages = {380--394}, year = 2000, number = 1877, series = {LNCS}} @article{amadio2003symbolic, title={On the symbolic reduction of processes with cryptographic functions}, author={Amadio, R.M. and Lugiez, D. and Vanack{\`e}re, V.}, journal={Theoretical Computer Science}, volume={290}, number={1}, pages={695--740}, year={2003}, publisher={Elsevier} } @InProceedings{AndersonKuhn96, author = "Ross Anderson and M. Kuhn", title = "Tamper Resistance - a Cautionary Note", booktitle = "Proceedings of the Second Usenix Workshop on Electronic Commerce", pages = "1--11", year = 1996 } @InProceedings{AndersonKuhn97, author = "Ross Anderson and Markus Kuhn", title = "Low Cost Attacks on Tamper Resistant Devices", booktitle = "{IWSP}: International Workshop on Security Protocols, {LNCS}", year = "1997" } @Article{AndersonNeedham, author = "R. Anderson and R. Needham", title = "Programming Satan's Computer", journal = "Computer Science Today: Lecture Notes in Computer Science", volume = "1000", year = 1995, pages = "426--441" } @Article{ACGMMR2006composing, title = {Sufficient Conditions for Composing Security Protocols}, author = {S. Andova and C.J.F. Cremers and K. Gj{\o}steen and S. Mauw and S.F. Mj{\o}lsnes and S. Radomirovi\'{c}}, booktitle = {Special issue on Computer Security: Foundations and Automated Reasoning}, journal = {Information and Computation}, volume={206}, number={2}, pages={425--459}, year = 2008 } @article{ankney1995unified, title={{The Unified Model}. Contribution to {ANSI X9F1}}, author={Ankney, R. and Johnson, D. and Matyas, M.}, journal={Standards Projects (Financial Crypto Tools), ANSI X}, volume={42}, year={1995} } @Article{AnsonMitchell90, author = "Colin l'Anson and Chris Mitchell", title = "Security Defects in the CCITT Recommendation {X}.509 --- The Directory Authentication Framework", journal = "Computer Communication Review", year = 1990, volume = 20, number = 2, pages = "30-34", month = apr } @inproceedings{Anteniese99, author = {Ateniese, Giuseppe}, title = {Efficient verifiable encryption (and fair exchange) of digital signatures}, booktitle = {CCS '99: Proceedings of the 6th ACM conference on Computer and communications security}, year = {1999}, isbn = {1-58113-148-8}, pages = {138--146}, location = {Kent Ridge Digital Labs, Singapore}, doi = {http://doi.acm.org/10.1145/319709.319728}, publisher = {ACM}, address = {New York, NY, USA}, } @InProceedings{AppelFelten99, author = {Andrew W. Appel and Edward W. Felten}, title = {Proof-Carrying Authentication}, booktitle = {6th {ACM} Conference on Computer and Communications Security}, year = 1999, month = {November} } @InProceedings{ArapinisEtAl2011, author = {Myrto Arapinis and Mark Ryan and Eike Ritter}, title = {{StatVerif}: Verification of Stateful Processes}, booktitle = {{IEEE} Symposium on Computer Security Foundations}, year = 2011, month = {June}, publisher = {{IEEE CS} Press}} @Book{AristotleNE, author = {Aristotle}, title = {Nicomachean Ethics}, publisher = {Oxford University Press}, year = 1953 } @Misc{ASN1, author = {ISO}, title = {Abstract Syntax Notation One ({ASN.1})}, howpublished = {ISO/IEC 8824} } @article{AsokanEtAl00, title={Optimistic fair exchange of digital signatures}, author={N. Asokan and Victor Shoup and Michael Waidner}, journal={{IEEE} J. Sel.~Areas in Comms.}, volume=18, number=4, pages={593--610}, year=2000 } @InProceedings{AsokanEtAl97, author = {N. Asokan and Matthias Schunter and Michael Waidner}, title = {Optimistic Protocols for Fair Exchange}, booktitle = {4th Conference on Computer and Communications Security ({CCS})}, pages = {6--17}, year = 1997, publisher = {{ACM}}} @Misc{rfc1826, OPTkey = {}, author = {R. Atkinson}, title = {{IP} Authentication Header}, howpublished = {Internet Request for Comments 1826}, year = {1995}, month = {August}, note = {Available at \texttt{http://ds.internic.net/rfc/rfc1826.txt}.}, OPTannote = {} } @article{ax1968elementary, title={{The elementary theory of finite fields}}, author={Ax, J.}, journal={The Annals of Mathematics}, volume={88}, number={2}, pages={239--271}, issn={0003-486X}, year={1968}, publisher={JSTOR} } @InProceedings{BackesEtAl02, author = {Michael Backes and Christian Jacobi and Birgit Pfitzmann}, title = {Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation}, booktitle = {Formal Methods Europe '02 (FME)}, pages = {310--329}, year = 2002, series = {LNCS}, volume = 2391, publisher = {Springer Verlag} } @InProceedings{BackesPfitzmann05, author = {Michael Backes and Birgit Pfitzmann}, title = {Relating Cryptographic and Symbolic Key Secrecy}, booktitle = {Proceedings, 26th {IEEE} Symposium on Security and Privacy}, year = 2005, month = {May}, note = {Extended version, \url{http://eprint.iacr.org/2004/300}}} @InProceedings{BackesEtAl08, author = {Michael Backes and Matteo Maffei and Dominique Unruh}, title = {Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the {Direct Anonymous Attestation} Protocol}, booktitle = {{IEEE} Symposium on Security and Privacy}, year = 2008} @inproceedings{MaffeiEtAl07, author = {Michael Backes and Agostino Cortesi and Riccardo Focardi and Matteo Maffei}, title = {A calculus of challenges and responses}, booktitle = {FMSE '07: ACM Workshop on Formal methods in Security Engineering}, year = 2007, isbn = {978-1-59593-887-9}, pages = {51--60}, location = {Fairfax, Virginia, USA}, doi = {http://doi.acm.org/10.1145/1314436.1314444}, publisher = {ACM}, address = {New York, NY, USA}, } @Misc{rfc1827, OPTkey = {}, author = {R. Atkinson}, title = {{IP} Encapsulating Security Payload {(ESP)}}, howpublished = {Internet Request for Comments 1827}, year = {1995}, month = {August}, note = {Available at \texttt{http://ds.internic.net/rfc/rfc1827.txt}.}, OPTannote = {} } @InProceedings{BartalEtAl99, author = {Yair Bartal and Alain Mayer and Kobbi Nissim and Avishai Wool}, title = {Firmato: A Novel Firewall Management Toolkit}, booktitle = {Proceedings, {IEEE} Symposium on Security and Privacy}, year = 1999, month = {May}, publisher = {IEEE CS Press} } @inproceedings{BasinEtAl05, author = {A. Armando and D. A. Basin and Y. Boichut and Y. Chevalier and L. Compagna and J. Cu{\'e}llar and P. Hankes Drielsma and P.-C. H{\'e}am and O. Kouchnarenko and J. Mantovani and S. M{\"o}dersheim and D. von Oheimb and M. Rusinowitch and J. Santiago and M. Turuani and L. Vigan{\`o} and L. Vigneron}, title = {The {AVISPA} Tool for the Automated Validation of Internet Security Protocols and Applications}, booktitle = {CAV}, year = {2005}, pages = {281--285}, ee = {http://dx.doi.org/10.1007/11513988_27}, crossref = {DBLP:conf/cav/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/ijisec/BasinMV05, author = {David A. Basin and Sebastian M{\"o}dersheim and Luca Vigan{\`o}}, title = {{OFMC}: A symbolic model checker for security protocols}, journal = {Int. J. Inf. Sec.}, volume = {4}, number = {3}, year = {2005}, pages = {181-208}, ee = {http://dx.doi.org/10.1007/s10207-004-0055-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{CaleiroEtAl2005, title={{Relating strand spaces and distributed temporal logic for security protocol analysis}}, author={Caleiro, C. and Vigano, L. and Basin, D.}, journal={Logic Journal of IGPL}, volume={13}, number={6}, pages={637}, year={2005}, publisher={Oxford Univ Press} } @proceedings{DBLP:conf/cav/2005, editor = {Kousha Etessami and Sriram K. Rajamani}, title = {Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings}, booktitle = {CAV}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3576}, year = {2005}, isbn = {3-540-27231-3}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{BeckerSewell04, author = {Moritz Y. Becker and Peter Sewell}, title = {Cassandra: Flexible Trust Management, Applied to Electronic Health Records}, booktitle = {17th Computer Security Foundations Workshop}, pages = {139--154}, year = 2004, address = {Asilomar, CA}, month = {June}, publisher = {{IEEE CS} Press} } @TechReport{BellLaPadula75, author = {David E. Bell and Leonard J. LaPadula}, title = {Computer Security Model: Unified Exposition and {Multics} Interpretation}, institution = {ESD}, year = 1975, number = {75-306}, month = {June} } @TechReport{BellaEtAl01, author = {Giampaolo Bella and Fabio Massacci and Lawrence C. Paulson}, title = {Verifying the {SET} Purchase Protocols}, institution = {Cambridge University Computer Laboratory}, year = {2001}, OPTkey = {}, OPTtype = {Report}, OPTnumber = {524}, OPTaddress = {}, OPTmonth = {November}, note = {Short version appeared in International Joint Conference on Automated Reasoning, June, 2001. Available at http://www.cl.cam.ac.uk/\-users/\-lcp/\-papers/\-protocols.html}, OPTannote = {} } @InProceedings{Bellare98, author = {Mihir Bellare}, title = {Practice-Oriented Provable Security}, booktitle = {First International Workshop on Information Security ({ISW} 97)}, year = 1998, editor = {E. Okamoto and G. Davida and M. Mambo}, volume = 1396, series = {LNCS}, publisher = {Springer Verlag} } @InProceedings{BellareKillianRogaway94, author = {Mihir Bellare and J. Killian and Phillip Rogaway}, title = {The Security of Cipher Block Chaining}, booktitle = {Advances in Cryptology --- Crypto 94}, year = 1994, editor = {Yvo Desmedt}, volume = 839, series = {LNCS}, publisher = {Springer Verlag} } @InProceedings{BellareRogaway93, author = {Mihir Bellare and Phillip Rogaway}, title = {Entity Authentication and Key Distribution}, booktitle = {Advances in Cryptology -- Crypto '93 Proceedings}, year = 1993, number = 773, series = {LNCS}, publisher = {Springer-Verlag} } @InProceedings{BellareRogaway93a, author = {Mihir Bellare and Phillip Rogaway}, title = {Random Oracles are Practical: a paradigm for designing efficient protocols}, booktitle = {Proceedings, {ACM} Conference on Communications and Computer Security}, year = 1993, pages = "62--73", publisher = {{ACM}}, note = {Full version available at http://www-cse.ucsd.edu/users/mihir/papers/} } @Article{BellerChangYacobi93, author = "Michael J. Beller and Li-Fung Chang and Yacov Yacobi", title = "Privacy and Authentication on a Portable Communications System", journal = "Journal on Selected Areas in Communications", year = 1993, volume = 11, number = 6, pages = "821--829", month = aug } @Article{BellovinMerrit90, author = "S. M. Bellovin and M. Merrit", title = "Limitations of the {Kerberos} Authentication System", journal = "Computer Communication Review", year = 1990, volume = 20, number = 5, pages = "119--132", month = oct, } @InProceedings{BellovinMerrit92, author = "S. M. Bellovin and M. Merrit", title = "Encrypted Key Exchange: Password based protocols secure against dictionary attacks", pages = "72--84", booktitle = "Proceedings 1992 IEEE Symposium on Research in Security and Privacy", year = 1992, publisher = "IEEE CS", month = may } @InProceedings{Bellovin96, author = {Steven Bellovin}, title = {Problem Areas for the {IP} Security Protocols}, booktitle = {Proceedings of the Sixth USENIX {UNIX} Security Symposium}, year = 1996, month = {July}, note = {Also at ftp://ftp.research.att.com/dist/smb/badesp.ps} } @Article{BessonEtAl01, author = {F. Besson and T. Jensen and D. L. M{\'e}tayer and T. Thorn}, title = {Model Checking Security Properties of Control Flow Graphs}, journal = {Journal of Computer Security}, year = 2001, volume = 9, pages = {217--250} } @inproceedings{DBLP:conf/lpar/BezemC05, author = {Marc Bezem and Thierry Coquand}, title = {Automating Coherent Logic}, booktitle = {{LPAR}, Logic for Programming, Artificial Intelligence, and Reasoning}, year = 2005, pages = {246-260}, series = {Lecture Notes in Computer Science}, volume = 3835, ee = {http://dx.doi.org/10.1007/11591191_18}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/lpar/2005, editor = {Geoff Sutcliffe and Andrei Voronkov}, title = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings}, booktitle = {LPAR}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3835}, year = {2005}, isbn = {3-540-30553-X}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{Bieber90, author = "P. Bieber", title = "A Logic of Communication in a Hostile Environment", pages = "14--22", booktitle = "Proceedings of the Computer Security Foundations Workshop III", year = 1990, publisher = "IEEE CS Press" } @Article{BihamShamir91a, author = "E. Biham and A. Shamir", title = "Differential Cryptanalysis of DES-like Cryptosystems", OPTcrossref = "", OPTkey = "", OPTjournal = "Advances in Cryptology -- Proceedings of CRYPTO '90", OPTyear = "1991", OPTvolume = "", OPTnumber = "", OPTpages = "3--72", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{BihamShamir97, author = "Eli Biham and Adi Shamir", title = "Differential Fault Analysis of Secret Key Cryptosystems", journal = "Lecture Notes in Computer Science", volume = "1294", year = "1997" } @InProceedings{BirdGopalHerzbergJansonKuttenMolvaYung91, author = "R. Bird and I. Gopal and A. Herzberg and P. A. Janson and S. Kutten and R. Mulva and M. Yung", title = "Systematic Design of Two-Party Authentication Protocols", editor = "J. Feigenbaum", series = "Lecture Notes in Computer Science", number = 576, pages = "44--61", booktitle = "Proceedings of Crypto '91: Advances in Cryptology ", year = 1991, publisher = "Springer Verlag" } @Article{BirdGopalHerzbergJansonKuttenMolvaYung93, author = "R. Bird and I. Gopal and A. Herzberg and P. A. Janson and S. Kutten and R. Mulva and M. Yung", title = "Systematic Design of a Family of Attack-Resistant Authentication protocols", journal = "IEEE Journal on Selected Areas in Communications", year = 1993, volume = 11, number = 5, pages = "679--693" } @Article{Birrell85, author = "A. D. Birrell", title = "Secure Communication using Remote Procedure Calls", journal = "ACM Transactions on Operating Systems", year = 1985, volume = 3, number = 1, pages = "1--14", month = feb } @InProceedings{Blakely79, author = "G. R. Blakely", title = "Safeguarding Cryptographic Keys.", pages = "313--317", booktitle = "Proceedings AFIPS 1979 National Computer Conference", year = 1979, publisher = AFIPS } @InProceedings{Blanchet01, author = {Bruno Blanchet}, title = {An Efficient Protocol Verifier based on {Prolog} Rules}, booktitle = {14th Computer Security Foundations Workshop}, pages = {82--96}, year = 2001, month = {June}, publisher = {IEEE CS Press} } @InProceedings{Blanchet02, author = {Bruno Blanchet}, title = {From Secrecy to Authenticity in Security Protocols}, booktitle = {9th Static Analysis Symposium}, pages = {342--359}, number = 2477, series = {LNCS}, month = {September}, year = 2002, publisher = {Springer Verlag} } @INPROCEEDINGS{Blanchet04, title={Automatic proof of strong secrecy for security protocols}, author={Blanchet, B.}, booktitle={Security and Privacy, 2004. Proceedings. 2004 IEEE Symposium on}, year=2004, month={May}, publisher = {IEEE CS Press}, pages={ 86-100} } @PHDTHESIS{Blanchet08, AUTHOR = {Bruno Blanchet}, TITLE = {V\'{e}rification automatique de protocoles cryptographiques: mod{\`e}le formel et mod{\`e}le calculatoire. Automatic verification of security protocols: formal model and computational model}, SCHOOL = {Universit{\'e} Paris-Dauphine}, YEAR = 2008, TYPE = {M\'{e}moire d'habilitation \`{a} diriger des recherches}, MONTH = NOV, NOTE = {En fran\c{c}ais avec publications en anglais en annexe. In French with publications in English in appendix.} } @InProceedings{BlanchetPodelski03, author = {Bruno Blanchet and Andreas Podelski}, title = {Verification of Cryptographic Protocols: Tagging Enforces Termination}, booktitle = {Foundations of Software Science and Computation Structures}, pages = {136--152}, year = 2003, series = {LNCS}, month = {April} } @InProceedings{Boebert85, author = "W. E. Boebert and R. Y. Kain", title = "A Practical Alternative to Hierarchical Integrity Policies", booktitle = "Proceedings of the Eighth National Computer Security Conference", year = 1985 } @InProceedings{BlazeEtAl97, author = {Matt Blaze and Joan Feigenbaum and Jack Lacy}, title = {Distributed Trust Management}, booktitle = {Proceedings, 1996 {IEEE} Symposium on Security and Privacy}, pages = {164--173}, year = 1997, month = {May} } @Misc{BlazeEtAl99, author = {Matt Blaze and Joan Feigenbaum and John Ioannidis and Angelos D. Keromytis}, title = {The {KeyNote} Trust Management System, version 2}, howpublished = {{IETF RFC} 2704}, month = {September}, year = 1999 } @Article{BonehEtAl97, author = "Dan Boneh and Richard A. DeMillo and Richard J. Lipton", title = "On the Importance of Checking Cryptographic Protocols for Faults", journal = "Lecture Notes in Computer Science", volume = "1233", pages = "37--51", year = "1997" } @TechReport{BonehEtAl98, author = "Bill Aiello and Dan Boneh and Matthew Franklin and Jeremy Horwitz", title = "Protocols for Secure Generation of Shared {RSA} Keys", institution = "Standford University", year = 1998, note = "DARPA Contract F30602-97-C-0326, Data Item Number A007: Technical Information Report" } @InProceedings{Boneh98, author = {Dan Boneh}, title = {The decision {Diffie-Hellman} problem}, booktitle = {Proceedings of the Third Algorithmic Number Theory Symposium}, pages = {48--63}, year = 1998, number = 1423, series = {Lecture Notes in Computer Science}, publisher = {Springer--Verlag} } @InProceedings{BonehFranklin97, author = "D. Boneh and M. Franklin", title = "Efficient Generation of Shared RSA Keys", series = "Lecture Notes in Computer Science", number = 1233, pages = "425--439", booktitle = "Proceedings of Crypto '97", year = 1997, publisher = "Springer Verlag" } @InProceedings{Boreale01, author = {Michele Boreale}, title = {Symbolic Trace Analysis of Cryptographic Protocols}, booktitle = {{ICALP}}, year = 2001 } @InProceedings{Bovenlander, author = "E. Bovenlander and RL van Renesse", title = "Smartcards and Biometrics: An Overview", booktitle = "Computer Fraud and Security Bulletin", year = "1995", pages = "8--12" } @Article{Boyd90, author = "Colin Boyd", title = "Hidden Assumptions in Cryptographic Protocols", journal = "Proceedings of the IEE", year = 1990, volume = "137 Pt E", number = 6, pages = "433--436", month = nov, } @InProceedings{Boyd92, author = "C. Boyd", title = "A Formal Framework for Authentication", pages = "273--292", booktitle = "Proceedings ESORICS 92", editor = "Y. Deswarte and G. Eizenberg and J.-J. Quisquater", publisher = "Springer LNCS 648", year = "1992", } @InProceedings{BoydMao94a, title = "Designing Secure Key Exchange Protocols", year = 1994, pages = "93--106", editor = "Dieter Gollmann", booktitle= "Computer Security---{ESORICS} '94", author = "Colin Boyd and Wenbo Mao", publisher = "Springer-Verlag" } @InProceedings{BraceEtAl90, author = {Karl S. Brace and Richard L. Rudell and Randal E. Bryant}, title = {Efficient Implementation of a {BDD} Package}, booktitle = {27th {ACM/IEEE} Design Automation Conference}, pages = {40--45}, year = 1990 } @InProceedings{BrickellCamenischChen04, author = {Ernie Brickell and Jan Camenisch and Liqun Chen}, title = {Direct Anonymous Attestation}, booktitle = {ACM Conference on Communications and Computer Security ({CCS})}, year = 2004, note = {Full version available at \url{http://eprint.iacr.org/2004/205}}} @Article{BrickellOdlyzko88, author = "E. F. Brickell and A. M. Odlyzko", title = "Cryptanalysis: A Survey of Recent Results", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, month = may } @InProceedings{BroadfootLowe03, author = {Philippa Broadfoot and Gavin Lowe}, title = {On Distributed Security Transactions that use Secure Transport Protocols}, booktitle = {Proceedings, 16th Computer Security Foundations Workshop}, pages = {63--73}, year = 2003, publisher = {{IEEE} {CS} Press} } @Article{Bryant86, author = {Randal E. Bryant}, title = {Graph-Based Algorithms for Boolean Function Manipulation}, journal = {IEEE Transactions on Computers}, year = 1986, volume = {C-35}, number = 8, pages = {677--691}, month = {August} } @Article{BurrowsAbadiNeedham89, author = {Michael Burrows and Mart\'{\i}n Abadi and Roger Needham}, title = {A Logic of Authentication}, journal = {Proceedings of the Royal Society}, year = 1989, volume = {Series A, 426}, number = 1871, pages = {233--271}, month = {December}, OPTnote = {Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer Systems 8, 1 (February 1990), 18-36. } } @TechReport{BurrowsAbadiNeedham89a, author = "Michael Burrows and Mart\'{\i}n Abadi and Roger Needham", title = "A Logic of Authentication", institution = "Digital Systems Research Center", year = 1989, type = "Technical Report", number = 39, month = feb } @Article{BurrowsAbadiNeedham90, author = "Michael Burrows and Mart\'{\i}n Abadi and Roger M. Needham", title = "Rejoinder to {Nessett}", journal = "ACM Operating Systems Review", year = 1990, volume = 24, number = 2, pages = "39--40", month = apr } @TechReport{BurrowsAbadiNeedham94, author = "Michael Burrows and Mart\'{\i}n Abadi and Roger M. Needham", title = "The Scope of a Logic of Authentication", institution = "Digital Systems Research Center", year = 1994, type = "Revised Research Report", number = 39 } @InProceedings{ButtyanEtAl98, author = {Levente Butty{\'a}n and Sebastian Staamann and Uwe Wilhelm}, title = {A Simple Logic for Authentication Protocol Design}, booktitle = {11th {IEEE} Computer Security Foundations Workshop}, pages = {153--162}, year = 1998 } @Manual{CCITTX509, title = "The Directory-Authentication Framework", author = "{C. C. I. T. T. Recommendation X.509}", organization = "C. C. I. T. T.", year = 1988, month = dec, } @InProceedings{CampbellSafavi-NainiPleasants92, author = "E. A. Campbell and R. Safavi-Naini and P. A. Pleasants", title = "Partial Belief and Probabilistic Reasoning in the Analysis of Secure Protocols", pages = "84--91", booktitle = "Proceedings 5th IEEE Computer Security Foundations Workshop", year = 1992, publisher = "IEEE CS Press" } @TechReport{Canetti01, author = {Ran Canetti}, title = {Universally Composable Security: A New Paradigm for Cryptographic Protocols}, institution = {IACR}, year = 2001, number = {2000/067}, month = Oct, note = {Appeared in FOCS, 2001}, online = {http://eprint.iacr.org/2000/067.ps.gz}, } @InProceedings{CanettiHerzog06, author = {Ran Canetti and Jonathan Herzog}, title = {Universally composable symbolic analysis of mutual authentication and key exchange protocols}, booktitle = {Proceedings, Theory of Cryptography Conference (TCC)}, year = 2006, month = {March}} @InProceedings{CanettiKrawczyk01, title={Analysis of key-exchange protocols and their use for building secure channels}, author={Canetti, R. and Krawczyk, H.}, booktitle={Advances in Cryptology—EUROCRYPT 2001}, pages={453--474}, series = {LNCS}, year={2001}, publisher={Springer} } @InProceedings{CanettiKrawczyk02, author = {Ran Canetti and Hugo Krawczyk}, title = {Universally Composable Notions of Key Exchange and Secure Channels}, booktitle = {Eurocrypt 2002}, pages = {337--351}, series = {LNCS}, publisher = {Springer Verlag}, year = 2002 } @InProceedings{CarboneEtAl03, author = {Marco Carbone and Mogens Nielsen and Vladimiro Sassone}, title = {A Formal Model for Trust in Dynamic Networks}, booktitle = {International Conference on Software Engineering and Formal Methods}, year = 2003, editor = {Antonio Cerone}, month = {September}, publisher = {{IEEE CS} Press} } @inproceedings{CarboneEtAl07, author = {Marco Carbone and Kohei Honda and Nobuko Yoshida}, title = {Structured Communication-Centred Programming for Web Services}, booktitle = {Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007}, year = 2007, pages = {2-17}, ee = {http://dx.doi.org/10.1007/978-3-540-71316-6_2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{Carlsen94a, author = "Ulf Carlsen", title = "Cryptographic Protocol Flaws", booktitle = "Proceedings 7th IEEE Computer Security Foundations Workshop", publisher = "IEEE CS", year = 1994, pages = "192--200" } @InProceedings{Carlsen94b, author = "Ulf Carlsen", title = "Generating Formal Cryptographic Protocol Specifications", booktitle = "Proceedings 7th IEEE Computer Security Foundations Workshop", year = 1994, organization = "IEEE CS Press" } @Article{Carlsen94c, author = "Ulf Carlsen", title = "Optimal Privacy and Authentication on a Portable Communications System", journal = "Operating Systems Review", year = 1994, volume = 28, number = 3, pages = "16--23" } @Article{CarterWegman79, author = {J. Lawrence Carter and Mark N. Wegman}, title = {Universal Classes of Hash Functions}, journal = {Journal of Computer and System Sciences}, year = 1979, volume = 18, pages = {143--54} } @Article{WegmanCarter81, author = {Mark N. Wegman and J. Lawrence Carter}, title = {New Hash Functions and Their Use in Authentication and Set Equality}, journal = {Journal of Computer and System Sciences}, year = 1981, volume = 22, pages = {265--79} } @InProceedings{CederquistEtAl07, author = {Jan Cederquist and Mohammad Torabi Dashti and Sjouke Mauw}, title = {A Certified Email Protocol using Key Chains}, booktitle = {Advanced Information Networking and Applications Workshops/Symposia {(AINA'07)}, Symposium on Security in Networks and Distributed Systems {(SSNDS07)}}, pages = {525--530}, year = 2007, volume = 1, publisher = {IEEE CS Press}} @InProceedings{MitchellEtAl99, author = {I. Cervesato and N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov}, title = {A Meta-Notation for Protocol Analysis}, booktitle = {Proceedings, 12th {IEEE} Computer Security Foundations Workshop}, year = 1999, month = {June}, publisher = {{IEEE} CS Press} } @InProceedings{CervesatoEtAl00, author = {I. Cervesato and N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov}, title = {Relating Strands and Multiset Rewriting for Security Protocol Analysis}, booktitle = {Proceedings, 13th {IEEE} Computer Security Foundations Workshop}, year = 2000, month = {July}, publisher = {{IEEE} CS Press} } @Article{CeriGottlobTanca89, author = "Stefano Ceri and Georg Gottlob and Letizia Tanca", title = "What You Always Wanted to Know About Datalog (And Never Dared to Ask)", journal = "IEEE Transactions of Knowledge and Data Engineering", year = 1989, volume = 1, number = 1 } @InProceedings{ChadhaEtAl01, author = {Rohit Chadha and Max Kanovich and Andr{\'e} Scedrov}, title = {Inductive Methods and Contract-Signing Protocols}, booktitle = {Proceedings, 8th {ACM} Conference on Computer and Communications Security}, pages = {176--185}, year = 2001, editor = {Pierangela Samarati}, address = {New York}, month = {November}, publisher = {{ACM} Press} } @InProceedings{ChadhaEtAl03, author = {Rohit Chadha and John C. Mitchell and Andre Scedrov and Vitaly Shmatikov}, title = {Contract Signing, Optimism, and Advantage}, booktitle = {Concur --- Concurrency Theory}, pages = {366-382}, year = 2003, series = {LNCS}, publisher = {Springer}} @InProceedings{Chaum83, author = "D. Chaum", title = "Blind Signatures for Untraceable Payments", booktitle = "Advances in Cryptology: proceedings of Crypto 82", pages = "199--203", year = "1983", publisher = "Plenum Press" } @InProceedings{ChengGligor90, author = "P.-C. Cheng and Virgil D. Gligor", title = "On the Formal Specification and Verification of a Multiparty Session Protocol", pages = "216--233", booktitle = "Proceedings of the IEEE 1990 Symposium on Research in Security and Privacy", year = 1990, publisher = "IEEE CS Press" } @Article{ChenSwiftWarren95, author = "W. Chen and T. Swift and D. S. Warren", title = "Efficient Top-Down Computation of Queries under the Well-Founded Semantics", journal = "J. Logic Prog.", year = 1995, volume = 24, number = 3, pages = "161--199" } @Article{ChenWarren96, author = "W. Chen and D. S. Warren", title = "Tabled Evaluation with Delaying for General Logic Programs", journal = "J. ACM", mon = jan, year = 1996, volume = 43, number = 1, pages = "20--74" } @ARTICLE{CheinMugnier92, author = {Michel Chein and Marie-Laure Mugnier}, title = {Conceptual Graphs: fundamental notions}, journal = {Revue d'Intelligence Artificielle}, year = {1992}, volume = {6}, pages = {365--406} } @inproceedings{CheinMugnier04, author = {Michel Chein and Marie-Laure Mugnier}, title = {Concept Types and Coreference in Simple Conceptual Graphs}, booktitle = {Conceptual Structures at Work: 12th International Conference on Conceptual Structures, ICCS 2004, Huntsville, AL, USA, July 19-23, 2004. Proceedings}, year = {2004}, series = {LNCS}, number = {3127}, pages = {303-318}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{chevalier2003deciding, title={{Deciding the security of protocols with {Diffie-Hellman} exponentiation and products in exponents}}, author={Yannick Chevalier and Ralf K{\"u}sters and Micha{\"e}l Rusinowitch and Mathieu Turuani}, journal={FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science}, pages={124--135}, year={2003}, publisher={Springer} } @InProceedings{Choretal85, author = "B. Chor and S. Goldwasser and S. Micali and B. Awerbuch", title = "Verifiable secret sharing and achieving simultaneity in the presence of faults", pages = "383--395", booktitle = "Proceedings of the 26th IEEE Symposium on Foundations of Computer Science", year = 1985, publisher = "IEEE" } @Manual{CiscoCommandRef10, title = {Router Products Command Reference}, organization = {Cisco Systems}, address = {San Jose, CA}, edition = "10th", year = 1994, note = {Chapters 10 to 17 (especially Chapter~16). For more recent information, see~\url{http://www.cisco.com/univercd/}.} } @inproceedings{CiobacaCortier2010, author = {{\c{S}}tefan Ciob{\^a}c{\u{a}} and V{\'e}ronique Cortier}, booktitle = {CSF}, DOI = {10.1109/CSF.2010.29}, month = jul, pages = {322-336}, publisher = {{IEEE} Computer Society Press}, title = {Protocol composition for arbitrary primitives}, url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/ rr-lsv-2010-09.pdf}, year = {2010}, } @Article{DClarkeEtAl01, author = {Dwaine Clarke and Jean-Emile Elien and Carl Ellison and Matt Fredette and Alexander Morcos and Ronald L. Rivest}, title = {Certificate Chain Discovery in {SPKI/SDSI}}, journal = {Journal of Computer Security}, year = 2001, volume = 9, number = 4, pages = {285--322} } @Book{ClarkeEtAl01, author = {Edmund M. {Clarke, Jr.} and Orna Grumberg and Doron A. Peled}, title = {Model Checking}, publisher = {{MIT} Press}, year = 2001 } @Article{ClarkJacob95, author = "John Clark and Jeremy Jacob", title = "On The Security of Recent Protocols", journal = "Information Processing Letters", year = 1995, volume = 56, number = 3, pages = "151--155", month = nov } @TechReport{ClarkJacob95a, author = "John Clark and Jeremy Jacob", title = "{Security Protocols: An Annotated Bibliography}", institution = "Dept. of Computer Science, University of York", year = 1995, month = "June" } @TechReport{ClarkJacob95b, author = "John Clark and Jeremy Jacob", title = "{A Library of Security Protocols}", institution = "Dept. of Computer Science, University of York", year = 1995, month = "June" } @TechReport{ClarkJacob95c, author = "John Clark and Jeremy Jacob", title = "{A Library of Security Protocols with Attacks}", institution = "Dept. of Computer Science, University of York", year = 1995, month = "June" } @Unpublished{ClarkJacob95d, author = "John Clark and Jeremy Jacob", title = "{Implementation Dependencies in Repeated Authentication Protocols}", note = "", OPTcrossref = "", OPTkey = "", OPTyear = "1995", OPTmonth = "June", OPTannote = "" } @Unpublished{ClarkJacob95e, author = "John Clark and Jeremy Jacob", title = "{On the Security of Hwang and Chen's SPLICE/AS Augmented Protocol}", year = 1995, month = "June", note = "University of York, Department of Computer Science" } @Unpublished{ClarkJacob97a, author = "John Clark and Jeremy Jacob", title = "A Survey of Authentication Protocol Literature: Version 1.0", year = 1997, month = "November", note = "University of York, Department of Computer Science" } @Unpublished{ClarkJacob95f, author = "John Clark and Jeremy Jacob", title = "On the {Security of Recent Protocols}", note = "Submitted to Information Processing Letters", year = 1995, month = "July", annote = "Submitted to Information Processing Letters" } @Unpublished{ClarkJacob96a, author = "John Clark and Jeremy Jacob", title = "Multi-server Spoofing in the {Kerberos} Authentication Protocol", note = "", OPTcrossref = "", OPTkey = "", OPTyear = 1996, OPTmonth = jan, } @Unpublished{ClarkJacob96b, author = "John Clark and Jeremy Jacob", title = "Freshness is Not Enough", note = "", OPTcrossref = "", OPTkey = "", OPTyear = 1996, OPTmonth = jan, } @Unpublished{ClarkJacob96c, author = "John Clark and Jeremy Jacob", title = "Non-Repeatability is Not Enough", note = "", OPTcrossref = "", OPTkey = "", OPTyear = 1996, OPTmonth = jan, } @InProceedings{ClarkeJhaMarrero98, author = {Edmund Clarke and Somesh Jha and Will Marrero}, title = {Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols}, booktitle = {Proceedings, {IFIP} Working Conference on Programming Concepts and Methods (\textsc{Procomet})}, year = 1998 } @Article{CokerEtAl10, author = {George Coker and Joshua Guttman and Peter Loscocco and Amy Herzog and Jonathan Millen and Brian O'Hanlon and John Ramsdell and Ariel Segall and Justin Sheehy and Brian Sniffen}, title = {Principles of Remote Attestation}, journal = {International Journal of Information Security}, year = 2011, volume = 10, number = 2, pages = {63--81}} @Article{ComonCortier04, author = {Hubert Comon and V\'{e}ronique Cortier}, title = {Security properties: two agents are sufficient}, journal = {Science of Computer Programming}, year = 2004, volume = 50, number = {1-3}, pages = {51--71}, month = {March} } @inproceedings{CortierDelaune07, author = {V{\'e}ronique Cortier and J{\'e}r{\'e}mie Delaitre and St{\'e}phanie Delaune}, booktitle = {{F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'07)}, month = dec, publisher = {Springer}, series = {LNCS}, title = {Safely Composing Security Protocols}, url = {\url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07.pdf}}, year = 2007, } @article{cortier2009safely, title={Safely composing security protocols}, author={V{\'e}ronique Cortier and St{\'e}phanie Delaune}, journal={Formal Methods in System Design}, volume={34}, number={1}, pages={1--36}, year={2009}, publisher={Springer} } @TechReport{Coppersmith89, author = "D. Coppersmith", title = "Analysis of {ISO/CCITT} Document {X.509} Annex {D}", institution = "IBM Research Division", year = 1989, address = "Yorktown Heights", month = jun } @Article{Coppersmith94, author = "D. Coppersmith", title = "The Data Encryption Standard (DES) and its strength against attacks", journal = "IBM Journal of Research and Development", year = 1994, volume = 38, number = 3, pages = "243--250", month = "May" } @inproceedings{CorinEtAl07, author = {Ricardo Corin and Pierre-Malo Deni{\'e}lou and C{\'e}dric Fournet and Karthikeyan Bhargavan and James J. Leifer}, title = {Secure Implementations for Typed Session Abstractions}, booktitle = {20th IEEE Computer Security Foundations Symposium {CSF}}, year = {2007}, pages = {170-186}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{BhargavanEtAl09, author = {Karthikeyan Bhargavan and Ricardo Corin and Pierre-Malo Deni{\'e}lou and C{\'e}dric Fournet and James J. Leifer}, title = {Cryptographic Protocol Synthesis and Verification for Multiparty Sessions}, booktitle = {IEEE Computer Security Foundations Symposium}, year = 2009 } @conference{blake1999authenticated, title={{Authenticated {Diffe-Hellman} key agreement protocols}}, author={Simon Blake-Wilson and Alfred Menezes}, booktitle={Selected Areas in Cryptography}, pages={630--630}, year={1999}, organization={Springer} } @article{boneh1998decision, title={The decision {Diffie-Hellman} problem}, author={Dan Boneh}, journal={Algorithmic Number Theory}, pages={48--63}, year={1998}, publisher={Springer} } @article{boreale2003symbolic, title={{Symbolic analysis of crypto-protocols based on modular exponentiation}}, author={Boreale, M. and Buscemi, M.G.}, journal={Mathematical Foundations of Computer Science}, pages={269--278}, year={2003}, publisher={Springer} } @InCollection{BressonEtAl11, author = {Emmanuel Bresson and Yassine Lakhnech and Laurent Mazar{\'e} and Bogdan Warinschi}, title = {Computational Soundness: The Case of {Diffie-Hellman} Keys}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, key = {CortierKremer2011}, publisher = {{IOS} Press}, year = 2011, editor = {Veronique Cortier and Steve Kremer}, series = {Cryptology and Information Security Series} } @InProceedings{Ciobaca10, author = {Stefan Ciobaca and V\'eronique Cortier}, title = {Protocol Composition for Arbitrary Primitives}, booktitle = {{CSF} '10}, pages = {322-336}, year = 2010, publisher = {{IEEE} {CS} Press}} @article{CokerEtAl11, author = {George Coker and Joshua Guttman and Peter Loscocco and Amy Herzog and Jonathan Millen and Brian O'Hanlon and John Ramsdell and Ariel Segall and Justin Sheehy and Brian Sniffen}, affiliation = {National Security Agency and The MITRE Corporation}, title = {Principles of remote attestation}, journal = {International Journal of Information Security}, publisher = {Springer Berlin / Heidelberg}, issn = {1615-5262}, keyword = {Computer Science}, pages = {1-19}, url = {http://dx.doi.org/10.1007/s10207-011-0124-7}, year = {2011} } @InProceedings{CrazzolaraMilicia02, author = {Federico Crazzolara and Giuseppe Milicia}, title = {Developing Security Protocols in $\chi$-Spaces}, booktitle = {Proceedings, 7th Nordic Workshop on Secure {IT} Systems}, year = 2002, address = {Karlstad, Sweden}, month = {November} } @InProceedings{CrazzolaraWinskel01, author = {Federico Crazzolara and Glynn Winskel}, title = {Events in Security Protocols}, booktitle = {Proceedings, 8th {ACM} Conference on Computer and Communications Security}, pages = {96--105}, year = 2001, address = {Philadelphia}, month = {November}, publisher = {{ACM} Press} } @InProceedings{CrazzolaraWinskel02, author = {Federico Crazzolara and Glynn Winskel}, title = {Composing Strand Spaces}, booktitle = {Proceedings, Foundations of Software Technology and Theoretical Computer Science}, pages = {97--108}, year = 2002, number = 2556, series = {LNCS}, address = {Kanpur}, month = {December}, publisher = {Springer Verlag} } @phdthesis{Cremers06, Author = {C.J.F. Cremers}, Title = {Scyther - Semantics and Verification of Security Protocols}, School = {Eindhoven University of Technology}, Publisher = {University Press Eindhoven}, Year = 2006, Type = {{Ph.D.} dissertation}, ISBN = {978-90-386-0804-4}, } @inproceedings{Cremers2008, author = {Cas J.F. Cremers}, title = {Unbounded verification, falsification, and characterization of security protocols by pattern refinement}, booktitle = {{ACM} Conference on Computer and Communications Security ({CCS})}, year = 2008, isbn = {978-1-59593-810-7}, pages = {119--128}, location = {Alexandria, Virginia, USA}, doi = {http://doi.acm.org/10.1145/1455770.1455787}, publisher = {ACM}, address = {New York, NY, USA}, } @misc{CremersFeltz2011, author = {Cas Cremers and Michele Feltz}, title = {One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability}, howpublished = {Cryptology ePrint Archive, Report 2011/300}, year = {2011}, note = {\url{http://eprint.iacr.org/2011/300}}, } @article{Cremers12, title={Automated analysis of {Diffie-Hellman} protocols and advanced security properties}, author={Benedikt Schmidt and Simon Meier and Cas Cremers and David A. Basin}, journal={Computer Security Foundations, ({CSF})}, pages= {25--27}, year= 2012 } @Proceedings{Crypto93, title = "Efficient DES Key Search", year = 1993 } @PhdThesis{TorabiDashti07, author = {Mohammad Torabi Dashti}, title = {Keeping Fairness Alive}, school = {Vrije Universiteit}, year = 2007, address = {Amsterdam}} @inproceedings{DattaEtAl03a, author = "Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic", title = "Secure protocol composition", booktitle = "Proceedings, Formal Methods in Security Engineering", editor = "Michael Backes and David Basin and Michael Waidner", publisher = "ACM", pages = "11--23", year = 2003 } @inproceedings{DattaEtAl03, author = "Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic", title = "A derivation system for security protocols and its logical formalization", booktitle = "Proceedings, 16th Computer Security Foundations Workshop", editor = "Dennis Volpano", publisher = "IEEE CS Press", pages = "109--125", year = "2003", url = "ftp://ftp.kestrel.edu/pub/papers/pavlovic/CSFW03.pdf", } @InProceedings{DattaEtAl04, author = {Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic}, title = {Abstraction and Refinement in Protocol Derivation}, booktitle = {{IEEE} Computer Security Foundations Workshop}, year = 2004, publisher = {{IEEE} {CS} Press}} @Article{DattaEtAl05, author = {Anupam Datta and Ante Derek and John C. Mitchell and Dusko Pavlovic}, title = {A Derivation System and Compositional Logic for Security Protocols}, journal = {Journal of Computer Security}, year = 2005, volume = 13, number = 3, pages = {423--482} } @inproceedings{DBLP:conf/csfw/DattaDMW06, author = {Anupam Datta and Ante Derek and John C. Mitchell and Bogdan Warinschi}, title = {Computationally Sound Compositional Logic for Key Exchange Protocols}, booktitle = {Computer Security Foundations Workshop}, year = 2006, pages = {321-334}, ee = {http://doi.ieeecomputersociety.org/10.1109/CSFW.2006.9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/csfw/2006, title = {19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy}, booktitle = {CSFW}, publisher = {IEEE CS}, year = {2006}, isbn = {0-7695-2615-2}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{DavisSwick90, author = "D Davis and R Swick", title = "Network Security via Private-Key Certificates", year = 1990, journal = "Operating Systems Review", pages = "64--67" } @Booklet{Dedekind1888, title = {Was Sind und Was Sollen die Zahlen?}, author = {Richard Dedekind}, address = {Brunschweig}, year = 1888, note = {Translated as ``The Nature and Meaning of Numbers,'' in Richard Dedekind, \emph{Essays on the Theory of Numbers}, New York: Dover, 1963.} } @InProceedings{DelauneEtAl2011, author = {St{\'e}phanie Delaune and Steve Kremer and Mark D. Ryan and Graham Steel}, title = {Formal analysis of protocols based on {TPM} state registers}, booktitle = {{IEEE} Symposium on Computer Security Foundations}, year = 2011, month = {June}, publisher = {{IEEE CS} Press}} @Book{Denning82, author = "D. E. Denning", title = "Cryptography and Data Security", publisher = "Addison Wesley", year = "1982", } @Article{DenningSacco81, author = "Dorothy Denning and G. Sacco", title = "Timestamps in Key Distribution Protocols", journal = "Communications of the ACM", year = 1981, volume = 24, number = 8, month = aug } @Misc{DOD5200.28, title = {{Department of Defense} Trusted Computer System Evaluation Criteria}, howpublished = {{DOD} 5200.28-{STD}}, month = {December}, year = 1985, key = {Department of Defense} } @Misc{DES, author = "National Bureau of Standards", title = "Data Encryption Standard", howpublished = "Federal Information Processing Standards Publication 46", month = "January", year = 1977 } @Misc{DierksEtAl99, author = {T. Dierks and C. Allen}, title = {The {TLS} Protocol}, howpublished = {{RFC} 2246}, month = {January}, year = 1999 } @Misc{RFC2104, author = {H. Krawczyk and M. Ballare and R. Canetti}, title = {{HMAC}: Keyed--Hashing for Message Authentication}, howpublished = {{RFC} 2104}, month = {February}, year = 1997 } @Misc{rfc2246, author = {T. Dierks and C. Allen}, title = {The {TLS} Protocol}, howpublished = {{RFC} 2246}, month = {January}, year = 1999 } @Article{Diffie88, author = "Whitfield Diffie", title = "The First Ten Years in Public Key Cryptography", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, pages = "560-577", month = may, } @Article{DiffieHellman76, author = "W. Diffie and M. Hellman", title = "New Directions in Cryptography", journal = "IEEE Transactions on Information Theory", year = 1976, volume = 22, number = 6, pages = "644--654", month = nov } @article{diffie1992authentication, title={{Authentication and authenticated key exchanges}}, author={Whitfield Diffie and Paul C. {van Oorschot} and Michael J. Wiener}, journal={Designs, Codes and Cryptography}, volume=2, number=2, pages={107--125}, issn={0925-1022}, year=1992, publisher={Springer} } @inproceedings{dilloway2008specifying, title={Specifying secure transport channels}, author={Christopher Dilloway and Gavin Lowe}, booktitle={CSF}, pages={210--223}, year=2008, organization={IEEE} } @article{DoughertyGuttman2012, title={Symbolic Protocol Analysis for {Diffie-Hellman}}, author={Daniel J. Dougherty and Joshua D. Guttman}, journal={Arxiv preprint arXiv:1202.2168}, note = {At \url{http://arxiv.org/abs/1202.2168v1}}, year={2012} } @InProceedings{DoughertyGuttman2012a, author = {Daniel J. Dougherty and Joshua D. Guttman}, title = {An Algebra for Symbolic {Diffie-Hellman} Protocol Analysis}, booktitle = {Trustworthy Global Computing}, year = 2012, editor = {C. Palamidessi and M. Ryan}, volume = {8191}, pages = {164--181}, series = {LNCS}} @TechReport{DoghmiGuttmanThayer04, author = {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer}, title = {The Shapes of Bundles}, institution = {The MITRE Corp.}, year = 2004, type = {MTR}, number = {05 B 02} } @TechReport{DoghmiGuttmanThayer05, author = {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer}, title = {Skeletons and the Shapes of Bundles}, institution = {The MITRE Corp.}, year = 2005, type = {MTR}, number = {05 B 02, Revision 1} } @TechReport{DoghmiGuttmanThayer05a, author = {Shaddin Doghmi and Joshua Guttman and F. Javier Thayer}, title = {Skeletons and the Shapes of Bundles}, institution = {The MITRE Corp.}, year = 2005, note = {Available at \url{http://www.ccs.neu.edu/home/guttman/skeletons.pdf}} } @Unpublished{DoghmiGuttmanThayer06, author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer}, title = {Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions}, note = {Submitted for publication}, month = {June}, year = 2006} @Unpublished{DoghmiGuttmanThayer06a, author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer}, title = {Searching for Shapes in Cryptographic Protocols (Extended Version)}, note = {\url{http://eprint.iacr.org/2006/435}}, month = {November}, year = 2006} @InProceedings{DoghmiGuttmanThayer07a, author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer}, title = {Skeletons, Homomorphisms, and Shapes: Characterizing Protocol Executions}, booktitle = {Proceedings, Mathematical Foundations of Program Semantics}, year = 2007, editor = {M. Mislove}, OPTseries = {Electronic Lecture Notes in Theoretical Computer Science}, month = {April}} @InProceedings{DoghmiGuttmanThayer07, author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer}, title = {Searching for Shapes in Cryptographic Protocols}, booktitle = {Tools and Algorithms for Construction and Analysis of Systems {(TACAS)}}, year = 2007, series = {LNCS}, number = 4424, pages = {523--538}, formernote = {Extended version at \url{http://eprint.iacr.org/2006/435}. {CPSA} is available at \url{http://hackage.haskell.org/package/cpsa}}} @InProceedings{DoghmiGuttmanThayer07b, author = {Shaddin F. Doghmi and Joshua D.~Guttman and F. Javier Thayer}, title = {Completeness of the Authentication Tests}, booktitle = {European Symposium on Research in Computer Security ({ESORICS})}, pages = {106--121}, year = 2007, editor = {J. Biskup and J. Lopez}, number = 4734, series = {LNCS}, month = {September}, publisher = {Springer-Verlag}} @InProceedings{DoghmiGuttmanThayer07c, author = {Shaddin~F. Doghmi and Joshua~D. Guttman and F.~Javier Thayer}, title = {Skeletons and the Shapes of Bundles}, booktitle = {Workshop on Issues in the Theory of Security ({WITS})}, year = 2007, month = {March}, note = {Workshop associated with ETAPS, Braga, Portugal}} @Article{DolevYao83, author = {Daniel Dolev and Andrew Yao}, title = {On the Security of Public-Key Protocols}, journal = {{IEEE} Transactions on Information Theory}, year = 1983, volume = 29, pages = {198--208} } @Article{DolevEvenKarp82, author = {D. Dolev and S. Even and R. M. Karp}, title = {On the Security of Ping-Pong Protocols}, journal = {Information and Control}, year = 1982, volume = 55, pages = {57--68} } @TechReport{DTOS97, author = "Secure Computing Corporation", title = "DTOS General System Security and Assurability Assessment Report", institution = "MD A904-93-C-4209 CDRL A011", year = 1997, month = "June", note = "(http://www.securecomputing.com/randt/HTML/dtos.html)" } @InProceedings{DurginEtAl99, author = {N. A. Durgin and P. D. Lincoln and J. C. Mitchell and A. Scedrov}, title = {Undecidability of Bounded Security Protocols}, booktitle = {Proceedings of the Workshop on Formal Methods and Security Protocols --- FMSP}, year = 1999, note = {Final version appears in \emph{Journal of Computer Security}, 2004} } @Article{DurginEtAl04a, author = {Nancy Durgin and Patrick Lincoln and John Mitchell and Andre Scedrov}, title = {Multiset Rewriting and the Complexity of Bounded Security Protocols}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = 2, pages = {247--311}, note = {Initial version appeared in \emph{Workshop on Formal Methods and Security Protocols}, 1999} } @Article{DurginEtAl04, author = {Nancy Durgin and Patrick Lincoln and John Mitchell and Andre Scedrov}, title = {Multiset Rewriting and the Complexity of Bounded Security Protocols}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = 2, pages = {247--311}, note = {Initial version appeared in \emph{Workshop on Formal Methods and Security Protocols}, 1999} } @Unpublished{DurginEtAl00, author = {Nancy Durgin and John C. Mitchell and Dusko Pavlovic}, title = {Protocol Composition and Correctness}, note = {Short talk delivered at \emph{Logic in Computer Science}}, month = {June}, year = 2000 } @InProceedings{DurginEtAl01, author = {Nancy Durgin and John Mitchell and Dusko Pavlovic}, title = {A Compositional Logic for Protocol Correctness}, booktitle = {Proceedings, 14th Computer Security Foundations Workshop}, year = 2001, publisher = {{IEEE} CS Press}, month = {June} } @Article{DurginEtAl03, author = {Nancy Durgin and John Mitchell and Dusko Pavlovic}, title = {A Compositional Logic for proving security properties of protocols}, journal = {Journal of Computer Security}, year = 2003, volume = 11, number = 4, pages = {677--721} } @Misc{Eastlake99, author = {D. Eastlake}, title = {Domain Name Security Extensions}, howpublished = {{RFC} 2535}, month = {March}, year = 1999 } @Misc{RFC2535, author = {D. Eastlake}, title = {Domain Name Security Extensions}, howpublished = {{RFC} 2535}, month = {March}, year = 1999 } @Misc{Eastlake98, author = {Donald Eastlake}, title = {Secret Key Establishment for {DNS}}, howpublished = {Internet--Draft draft-ietf-dnssec-tkey-01.txt}, month = {September}, year = 1998 } @Misc{Eastlake98a, author = {Donald E. Eastlake}, title = {Secure Domain Name System Dynamic Update}, howpublished = {Internet--Draft draft-ietf-dnssec-update2-00.txt}, month = {August}, year = 1998 } @Misc{Ellison99, author = {Carl Ellison}, title = {{SPKI} Requirements}, howpublished = {{IETF RFC} 2692}, month = {September}, year = 1999 } @Misc{EllisonEtAl99, author = {Carl Ellison and Bill Frantz and Butler Lampson and Ron Rivest and Brian Thomas and Tatu Ylonen}, title = {{SPKI} Certificate Theory}, howpublished = {{IETF RFC} 2693}, month = {September}, year = 1999 } @Misc{ElzBush97, author = {R. Elz and R. Bush}, title = {Clarifications to the {DNS} Specification}, howpublished = {{RFC} 2182}, month = {July}, year = 1997 } @Misc{RFC2182, author = {R. Elz and R. Bush}, title = {Clarifications to the {DNS} Specification}, howpublished = {{RFC} 2182}, month = {July}, year = 1997 } @article{escobar2008state, title={{State space reduction in the Maude-{NPA} protocol analyzer}}, author={Santiago Escobar and Catherine Meadows and Jos\'e Meseguer}, journal={Computer Security-ESORICS 2008}, pages={548--562}, year={2008}, publisher={Springer} } @article{escobar2009maude, title={{Maude-{NPA}: Cryptographic protocol analysis modulo equational properties}}, author={Santiago Escobar and Catherine Meadows and Jos\'e Meseguer}, journal={Foundations of Security Analysis and Design V}, pages={1--50}, year={2009}, publisher={Springer} } @inproceedings{DBLP:conf/fosad/EscobarMM07, author = {Santiago Escobar and Catherine Meadows and Jos\'e Meseguer}, title = {Maude-{NPA}: Cryptographic Protocol Analysis Modulo Equational Properties}, booktitle = {Foundations of Security Analysis and Design {V}, {FOSAD} 2007--2009 Tutorial Lectures}, pages = {1-50}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 5705, year = 2009, isbn = {978-3-642-03828-0}, ee = {http://dx.doi.org/10.1007/978-3-642-03829-7_1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @TechReport{EvenYacobi80, title={Relations among public key signature systems}, author={Shimon Even and Yacov Yacobi}, institution={Computer Science Department, Technion}, number=175, year = 1980 } @InProceedings{EvenEtAl85, author = {Shimon Even and Oded Goldreich and Adi Shamir}, title = {On the Security of Ping-Pong Protocols when Implemented using the {RSA}}, booktitle = {Advances in Cryptology---{\sc crypto} '85}, pages = {58--72}, year = 1985, series = {LNCS}, publisher = {Springer Verlag} } @InProceedings{FarmerEtAl92, author = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer}, title = {Little theories}, booktitle = {Automated Deduction: CADE-11}, number = 607, series = {LNCS}, year = 1992, pages = {567--581}, publisher = {Springer-Verlag} } @InProceedings{, author = {}, title = {}, OPTcrossref = {}, OPTkey = {}, OPTbooktitle = {}, OPTpages = {}, OPTyear = {}, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @Article{FarmerEtAl93, author = {William M.~Farmer and Joshua D.~Guttman and F.~Javier Thayer}, title = {{\sc imps}: An {I}nteractive {M}athematical {P}roof {S}ystem}, journal = {Journal of Automated Reasoning}, year = 1993, volume = 11, pages = {213--248}} @Article{FarmerGuttman00, author = {W. M. Farmer and J. D. Guttman}, title = {A Set Theory with Support for Partial Functions}, journal = {Studia Logica}, year = 2000, volume = 65, pages = {59--70} } @InProceedings{Failure98, author = {P.A. Loscocco and S.D. Smalley and P.A. Muckelbauer and R.C. Taylor and S.J. Turner and J.F. Farrell}, title = {The Inevitability of Failure: The Flawed Assumption of Security in Modern Computing Environments}, booktitle = {Proceedings of the 21st National Information Systems Security Conference}, pages = {303--314}, year = 1998, month = {October} } @InProceedings{Feldman87, author = "P. Feldman", title = "A practical scheme for non-interactive verifiable secret sharing", booktitle = "Proceedings of the 28th IEEE Symposium on the Foundations of Computer Science", pages = "427-438", year = 1987, publisher = "IEEE" } @InProceedings{FerraioloKuhn92, author = "David Ferraiolo and Richard Kuhn", title = "Role-Based Access Control", booktitle = "Proceedings of the 15th National Computer Security Conference", year = 1992 } @Book{Feller, author = "W. Feller", title = "An Introduction to Probability Theory and its Applications", publisher = "John Wiley and Sons, Inc.", year = "1958", OPTeditor = "", OPTvolume = "", OPTseries = "", address = "New York", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{Dudley, author = "R. M. Dudley", title = "Real Analysis and Probability", publisher = "Wadsworth and Brookscole", year = "1989", OPTeditor = "", OPTvolume = "", OPTseries = "", address = "Pacific Grove", OPTedition = "", OPTmonth = "", OPTnote = "" } @Manual{FIPS, title = "Security Requirements for Cryptographic Modules", note = "FIPS PUB 140-1", author = "Federal Information Processing Standards Publication", organization = "National Institue of Standards and Technology", note = "US Department of Commerce", month = "January", year = 1994 } @Manual{FIPS4676, title = "Federal Information Processing Standard 46 -- the Data Encryption Standard", OPTcrossref = "", OPTkey = "", OPTauthor = "", OPTorganization = "", OPTaddress = "", OPTedition = "", OPTyear = "1976", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{FocardiGorrieri97, author = {Riccardo Focardi and Roberto Gorrieri}, title = {The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties}, journal = {IEEE Transactions on Software Engineering}, year = 1997, volume = 23, number = 9, month = {September}, annote = {Retrieved from http://www.cs.unibo.it/\~focardi/www/biblio2.html} } @InProceedings{DuranteFocardiGorrieri99, author = {Antonio Durante and Riccardo Focardi and Roberto Gorrieri}, title = {{CVS}: A Compiler for the Analysis of Cryptographic Protocols}, booktitle = {12th Computer Security Foundations Workshop Proceedings}, pages = {203--212}, year = 1999, month = {June}, publisher = {{IEEE} CS Press} } @TechReport{FDR2, author = {Formal Systems (Europe) Ltd.}, title = {Failures-Divergence Refinement: {FDR}~2 User Manual}, institution = {Formal Systems (Europe) Ltd.}, year = {1997}, OPTkey = {}, OPTtype = {}, OPTnumber = {}, address = {http: //www.formal.demon.co.uk/}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @InProceedings{FournetEtAl05, author = {C\'{e}dric Fournet and Andrew Gordon and Sergei Maffeis}, title = {A Type Discipline for Authorization Policies}, booktitle = {European Symposium on Programming}, year = 2005, editor = {Mooly Sagiv}, volume = {LNCS No}, series = {LNCS}, publisher = {Springer Verlag} } @Misc{FrierEtAl96, author = {Alan Frier and Philip Karlton and Paul Kocher}, title = {The {SSL} 3.0 Protocol}, year = 1996, key = {draft-freier-ssl-version3-02.txt}, howpublished = {Internet Draft}, month = nov } @InProceedings{Froeschle08, author = {Sibylle Fr{\"o}schle}, title = {Adding Branching to the Strand Space Model}, booktitle = {Proceedings of {EXPRESS'08}}, series = {ENTCS}, publisher = {Elsevier}, year = 2008 } @Article{FumyLandrock93, author = "W. Fumy and P. Landrock", title = "Principles of Key Management", journal = "IEEE Journal on Selected Areas in Communications", year = 1993, pages = "785--793", month = jun } @inproceedings{GarayEtAl99, author = {Juan A. Garay and Markus Jakobsson and Philip D. MacKenzie}, title = {Abuse-Free Optimistic Contract Signing}, booktitle = {CRYPTO '99: Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology}, year = {1999}, isbn = {3-540-66347-9}, pages = {449--466}, publisher = {Springer-Verlag}, address = {London, UK}, } @InCollection{Gentzen35, author = "G. Gentzen", title = "Investigations into Logical Deduction (1935)", booktitle = "The Collected Works of Gerhard Gentzen", publisher = "North Holland", year = 1969} @InProceedings{GeometricLogic, author = {NN}, title = {Geometric Logic}, booktitle = {Whatever volume contains it}, year = {200?}} @misc{ghcUsersGuide, title = {{GHC} User's Guide Documentation, release 8.2.1}, author = {The {GHC} Team}, note = {\url{https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf}}, month = {July}, year = {2017}, day = 21, } @InProceedings{GoguenMeseguer82, author = {Joseph A. Goguen and Jos\'e Meseguer}, title = {Security Policies and Security Models}, booktitle = {{IEEE} Symposium on Security and Privacy}, year = 1982 } @article{GoguenMeseguer92, author = {Joseph A. Goguen and Jos\'{e} Meseguer}, title = {Order-sorted algebra {I}: equational deduction for multiple inheritance, overloading, exceptions and partial operations}, journal = {Theoretical Computer Science}, volume = {105}, number = {2}, year = {1992}, pages = {217--273}, doi = {http://dx.doi.org/10.1016/0304-3975(92)90302-V}, publisher = {Elsevier Science Publishers Ltd.}, address = {Essex, UK}, } @Article{GongAuth, author = "Li Gong", title = "Increasing Availability and Security of an Authentication Service", journal = "IEEE Journal on Selected Areas in Communications", year = 1993, volume = 11, number = 5, month = jun } @Article{Gong89, author = "Li Gong", title = "Using One-way Functions for Authentication ", journal = "Computer Communication Review", year = 1989, volume = 19, number = 5, pages = "8-11", month = oct } @Unpublished{GoldwasserBellare, author = {Shafi Goldwasser and Mihir Bellare}, title = {Lecture Notes on Cryptography}, note = {Avaliable at http://www.cs.ucsd.edu/users/mihir/papers/gb.html}, month = {August}, year = 1999 } @InProceedings{Gong90a, author = "Li Gong", title = "Verifiable-Text Attacks in Cryptographic Protocols", pages = "686--693", booktitle = "Proceedings {IEEE} {INFOCOM'90} ", year = 1990, publisher = "IEEE CS", month = jun, } @Article{Gong90b, author = "Li Gong", title = "A Note on Redundancy in Encrypted Messages", journal = "Computer Communication Review", year = 1990, volume = 20, number = 5, pages = "18-22", month = oct, } @InProceedings{Gong91, author = "Li Gong", title = "Handling Infeasible Specifications of Cryptographic Protocols", pages = "99--102", booktitle = "Proceedings of The 4th {IEEE} Computer Security Foundations Workshop", year = 1991, publisher = "IEEE CS", month = jun } @InProceedings{Gong93, author = "Li Gong", title = "Variations on the Themes of Message Freshness and Replay and Replay or, the Difficulty of of Devising Formal Nethods to Analyse Cryptographic Protocols", pages = "131--136", booktitle = "Proceedings 6th Computer Security Foundations Workshop", year = 1993, publisher = "IEEE CS Press" } @Article{GongLomasNeedhamSaltzer93, author = "Li Gong and A. Lomas and Roger M. Needham and Jerry H. Saltzer", title = "Protecting Poorly Chosen Secrets from Guessing Attacks", journal = "IEEE Journal on Selected Areas in Communications", year = 1993, volume = 11, number = 5, month = jun } @InProceedings{GongNeedhamYahalom90, author = "Li Gong and Roger Needham and Raphael Yahalom", title = "Reasoning About Belief in Cryptographic Protocols", editor = "Deborah Cooper and Teresa Lunt", pages = "234--248", booktitle = "Proceedings 1990 IEEE Symposium on Research in Security and Privacy", year = 1990, publisher = "IEEE CS", month = may } @InProceedings{GongSyverson95, author = {Li Gong and Paul Syverson}, title = {Fail-Stop Protocols: An Approach to Designing Secure Protocols}, booktitle = {5th International Working Conference on Dependable Computing for Critical Applications}, pages = {44--55}, year = 1995, month = {September} } @InProceedings{Gordon84, title = "Public Key Cryptosystems", author = "John Gordon", booktitle = "Proceedings of Networks '84", year = 1984 } @InProceedings{GordonJeffrey01a, author = {Andrew D. Gordon and Alan Jeffrey}, title = {Authentication by Typing}, booktitle = {Proceedings, 14th Computer Security Foundations Workshop}, year = 2001, month = {June}, publisher = {{IEEE} CS Press} } @InProceedings{GordonJeffrey02, author = {Andrew D. Gordon and Alan Jeffrey}, title = {Types and Effects for Asymmetric Cryptographic Protocols}, booktitle = {Proceedings, 15th Computer Security Foundations Workshop}, year = 2002, month = {June}, publisher = {{IEEE} CS Press} } @Article{GordonJeffrey03, author = {Andrew D. Gordon and Alan Jeffrey}, title = {Authenticity by typing for security protocols}, journal = {Journal of Computer Security}, year = 2003, volume = 11, number = 4, pages = {451-–521}} @Article{GordonJeffrey03a, author = {Andrew D. Gordon and Alan Jeffrey}, title = {Types and effects for asymmetric cryptographic protocols}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = {3/4}, pages = {435–-484}} @article{goubault2005abstraction, title={{Abstraction and resolution modulo AC: How to verify {Diffie-Hellman}-like protocols automatically}}, author={Jean Goubault-Larrecq and Muriel Roger and Kumar Verma}, journal={Journal of Logic and Algebraic Programming}, volume={64}, number={2}, pages={219--251}, issn={1567-8326}, year={2005}, publisher={Elsevier} } @inproceedings{GoubaultLarrecq08, author = {Jean Goubault-Larrecq}, title = {Towards Producing Formally Checkable Security Proofs, Automatically}, booktitle = {Computer Security Foundations Workshop}, year = {2008}, pages = {224-238}, ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.21}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{gross2011vertical, title={Vertical protocol composition}, author={Thomas Gro{\ss} and Sebastian M{\"o}dersheim}, booktitle={CSF}, pages={235--250}, year={2011}, organization={IEEE} } @Article{VLispIntro95, author = {Joshua~D. Guttman and John~D. Ramsdell and Mitchell Wand}, title = {{VLISP}: A verified implementation of {Scheme}}, journal = {Lisp and Symbolic Computation}, year = 1995, volume = 8, number = {1/2}, pages = {5--32}} @Article{VLispScheme95, author = {Joshua~D. Guttman and John~D. Ramsdell and Vipin Swarup}, title = {The {VLISP} verified {Scheme} system}, journal = {Lisp and Symbolic Computation}, year = 1995, volume = 8, number = {1/2}, pages = {33--110}} @TECHREPORT{Guttman96, AUTHOR = "Joshua D. Guttman", TITLE = "Filtering Postures: Local Enforcement for Global Policies", NUMBER = "MTR 97B0000007", INSTITUTION = "The MITRE Corporation, Center for Integrated Intelligence Systems", ADDRESS = "Bedford, Massachusets", MONTH = "November", YEAR = "1996" } @InProceedings{Guttman97, author = {Joshua D. Guttman}, title = {Filtering Postures: Local Enforcement for Global Policies}, booktitle = {Proceedings, 1997 {IEEE} Symposium on Security and Privacy}, pages = {120--29}, year = 1997, month = {May}, publisher = {{IEEE} CS Press} } @Unpublished{Guttman99, author = {Joshua D. Guttman}, title = {Packet Filters and their Atoms}, note = {Lecture at University of Pennsylvania, host C.~Gunter}, month = {April}, year = 1999 } @InCollection{Guttman01, author = {Joshua D. Guttman}, title = {Security Goals: Packet Trajectories and Strand Spaces}, booktitle = {Foundations of Security Analysis and Design}, publisher = {Springer Verlag}, year = 2001, editor = {Roberto Gorrieri and Riccardo Focardi}, volume = 2171, series = {LNCS}, pages = {197--261}, note = {} } @Article{Guttman01a, author = {Joshua D. Guttman}, title = {Key Compromise and the Authentication Tests}, journal = {Electronic Notes in Theoretical Computer Science}, year = 2001, volume = 47, note = {Editor, M. Mislove. URL~\url{http://www.elsevier.nl/locate/entcs/volume47.html}, 21 pages} } @InProceedings{Guttman02, author = {Joshua D. Guttman}, title = {Security Protocol Design via Authentication Tests}, booktitle = {Proceedings, 15th Computer Security Foundations Workshop}, year = 2002, month = {June}, publisher = {{IEEE} CS Press} } @Article{Guttman04, author = {Joshua D. Guttman}, title = {Authentication Tests and Disjoint Encryption: a Design Method for Security Protocols}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = {3/4}, pages = {409--433} } @Article{Guttman04old, author = {Joshua D. Guttman}, title = {Authentication Tests and Disjoint Encryption: a Design Method for Security Protocols}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = {3/4}, note = {Extended version of ``Security Protocol Design via Authentication Tests,'' CSFW 2002.}, pages = {409--433} } @InProceedings{Guttman04a, author = {Joshua D. Guttman}, title = {Security, Protocols, and Trust}, booktitle = {VMCAI 2004: Verification, Model Checking, and Abstract Interpretation}, year = 2004, editor = {G. Levi and B. Steffen}, volume = 2937, series = {LNCS}, publisher = {Springer Verlag}, note = {(abstract of tutorial)} } @Unpublished{Guttman08, author = {Joshua D. Guttman}, title = {Cryptographic Protocol Composition, via the Authentication Tests}, note = {Submitted for publication}, month = {January}, year = 2008} @InProceedings{Guttman09, author = {Joshua D. Guttman}, title = {Cryptographic Protocol Composition via the Authentication Tests}, booktitle = {Foundations of Software Science and Computation Structures ({FOSSACS})}, year = 2009, editor = {Luca de Alfaro}, series = {LNCS}, number = 5504, pages = {303--317}, month = {March}, publisher = {Springer}} @InProceedings{Guttman09a, author = {Joshua D. Guttman}, title = {Transformations between Cryptographic Protocols}, booktitle = {Automated Reasoning in Security Protocol Analysis, and Workshop on Issues in the Theory of Security ({ARSPA-WITS})}, year = 2009, pages = {107--123}, number = 5511, editor = {P. Degano and L. Vigan{\`o}}, series = {LNCS}, publisher = {Springer}} @InProceedings{Guttman09b, author = {Joshua D. Guttman}, title = {Fair Exchange in Strand Spaces}, booktitle = {SecCo: 7th International Workshop on Security Issues in Concurrency}, year = 2009, editor = {M. Boreale and S. Kremer}, series = {EPTCS}, month = {Sep}, publisher = {Electronic Proceedings in Theoretical Computer Science}} @Article{Guttman09c, author = {Joshua D. Guttman}, title = {Security Theorems via Model Theory}, journal = {EXPRESS: Expressiveness in Concurrency (EPTCS)}, volume = {8}, pages = {51}, url = {http://cgi.cse.unsw.edu.au/~rvg/eptcs/content.cgi?EXPRESS2009}, note = {doi:10.4204/EPTCS.8.5}, year = {2009} } @Article{Guttman12, author = {Joshua D. Guttman}, title = {State and Progress in Strand Spaces: Proving Fair Exchange}, journal = {Journal of Automated Reasoning}, year = 2012, volume = 48, number = 2, pages = {159--195}, url = {http://www.springerlink.com/content/p87u245036468165/}, doinote = {DOI: 10.1007/s10817-010-9202-1}} @Article{Guttman11a, author = {Joshua D. Guttman}, title = {State and Progress in Strand Spaces: Proving Fair Exchange}, journal = {Journal of Automated Reasoning}, year = 2012, url = {http://www.springerlink.com/content/p87u245036468165/}, note = {Accepted, March 2010. DOI: 10.1007/s10817-010-9202-1}} @Book{CortierKremer2011, editor = {Veronique Cortier and Steve Kremer}, title = {Formal Models and Techniques for Analyzing Security Protocols}, publisher = {IOS Press}, year = 2011, series = {Cryptology and Information Security Series}} @InCollection{Guttman10, author = {Joshua D. Guttman}, title = {Shapes: Surveying Crypto Protocol Runs}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, key = {CortierKremer2011}, publisher = {{IOS} Press}, year = 2011, editor = {Veronique Cortier and Steve Kremer}, series = {Cryptology and Information Security Series}} @InProceedings{Guttman11, author = {Joshua D. Guttman}, title = {Security Goals and Protocol Transformations}, booktitle = {Tosca: Theory of Security and Applications}, year = 2011, editor = {Sebastian M{\"o}dersheim and Catuscia Palamidessi}, series = {LNCS}, month = {March}, publisher = {Springer}} @InProceedings{GuttmanEtAl00, author = {Joshua Guttman and Amy L. Herzog and F. Javier Thayer}, booktitle = {Proceedings, ESORICS 2000}, pages = {255-272}, year = {2000}, month = {October}, publisher = {Springer}, note = {Lecture Notes in Computer Science 1895} } @InProceedings{GuttmanHerzog02, author = "Joshua D. Guttman and Amy L. Herzog", title = "Eager Formal Methods for Security Management", booktitle = "Proceedings, VERIFY '02", pages = "91--101", year = 2002, month = "July" } @Article{GuttmanHerzog05, author = {Joshua D. Guttman and Amy L. Herzog}, title = {Rigorous Automated Network Security Management}, journal = {International Journal for Information Security}, year = 2005, volume = 5, number = {1--2}, pages = {29--48} } @Article{GuttmanHerzog03, author = {Joshua D. Guttman and Amy L. Herzog}, title = {Rigorous Automated Network Security Management}, journal = {International Journal for Information Security}, year = 2004, note = {Forthcoming} } @Misc{GuttmanHerzogRamsdell03, author = {Joshua D. Guttman and Amy L. Herzog and John D. Ramsdell}, title = {Information Flow in Operating Systems: Eager Formal Methods}, howpublished = {Submitted for publication}, month = {January}, year = 2003 } @Article{GuttmanHerzogRamsdell04, author = {Joshua D. Guttman and Amy L. Herzog and John D. Ramsdell and Clement W. Skorupka}, title = {Verifying Information Flow Goals in {Security-Enhanced Linux}}, journal = {Journal of Computer Security}, year = 2005, volume = 13, number = 1, pages = {115--134}, note = {Preliminary version appeared in the Workshop on Issues in the Theory of Security (IFIP WG 1.7), April 2003.} } @TechReport{GuttmanHerzogThayer00ab, author = {Joshua D. Guttman and Amy L. Herzog and F. Javier Thayer}, title = {Authentication and Confidentiality via {IPsec}}, institution = {The {MITRE} Corporation}, year = 2000, month = {March} } @InProceedings{GuttmanHerzogThayer00, author = {Joshua D. Guttman and Amy L. Herzog and F. Javier Thayer}, title = {Authentication and Confidentiality via {IPsec}}, booktitle = {ESORICS 2000: European Symposium on Research in Computer Security}, year = 2000, number = 1895, editor = {D. Gollman}, series = {LNCS}, publisher = {Springer Verlag} } @InProceedings{GuttmanEtAl05, author = {Joshua D. Guttman and Jonathan C. Herzog and John D. Ramsdell and Brian T. Sniffen}, title = {Programming Cryptographic Protocols}, booktitle = {Trust in Global Computing}, pages = {116--145}, year = 2005, editor = {Rocco De Nicola and Davide Sangiorgi}, number = 3705, series = {LNCS}, publisher = {Springer} } @inproceedings{McCarthyEtAl07, author = {Jay A. McCarthy and Shriram Krishnamurthi and Joshua D. Guttman and John D. Ramsdell}, title = {Compiling cryptographic protocols for deployment on the web}, booktitle = {World Wide Web Conference}, pages = {687--696}, publisher = {{ACM}}, year = {2007}, url = {https://doi.org/10.1145/1242572.1242665}, doi = {10.1145/1242572.1242665}, timestamp = {Tue, 06 Nov 2018 16:57:07 +0100}, biburl = {https://dblp.org/rec/conf/www/McCarthyKGR07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @Unpublished{GuttmanThayer99, author = {Joshua D. Guttman and F. Javier {\textsc{Thayer} F\'abrega}}, title = {Disjoint Encryption and the Normal Penetrator}, note = {Unpublished}, month = {September}, year = 1999 } @InProceedings{GuttmanThayer00, author = {Joshua D. Guttman and F. Javier {Thayer}}, title = {Authentication Tests}, booktitle = {Proceedings, 2000 IEEE Symposium on Security and Privacy}, year = 2000, organization = {May}, publisher = {IEEE CS Press} } @TechReport{GuttmanThayer00a, author = {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}}, title = {Authentication Tests and the Normal Penetrator}, institution = {The {MITRE} Corporation}, year = 2000, type = {MTR}, number = {00B04}, month = {February}, note = {Also submitted for publication.{\typeout{ERROR: Don't cite this anymore, use GuttmanThayer00c.}}} } @Article{GuttmanThayer00caca, author = {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}}, title = {Authentication Tests and the Structure of Bundles}, journal = {Theoretical Computer Science}, year = 2002, note = {To appear} } @Article{GuttmanThayer00c, author = {Joshua D. Guttman and F. Javier {{Thayer}}}, title = {Authentication Tests and the Structure of Bundles}, journal = {Theoretical Computer Science}, year = 2002, month = {June}, pages = {333--380}, volume = 283, number = 2 } @Article{GuttmanThayer02, author = {Joshua D. Guttman and F. Javier {{Thayer}}}, title = {Authentication Tests and the Structure of Bundles}, journal = {Theoretical Computer Science}, year = 2002, month = {June}, pages = {333--380}, volume = 283, number = 2 } @InProceedings{GuttmanThayer00b, author = {Joshua D. Guttman and F. Javier {{Thayer}}}, title = {Protocol Independence through Disjoint Encryption}, booktitle = {Computer Security Foundations Workshop}, year = 2000, publisher = {{IEEE} {CS} Press} } @Unpublished{GuttmanThayer00ba, author = {Joshua D. Guttman and F. Javier {\textsc{Thayer} F{\'a}brega}}, title = {Protocol Independence through Disjoint Encryption}, note = {In preparation.}, OPTkey = {}, OPTmonth = {}, OPTyear = {}, OPTannote = {} } @TechReport{GuttmanThayer05, author = {Joshua D. Guttman and F. Javier Thayer}, title = {The Sizes of Skeletons: Decidable Cryptographic Protocol Authentication and Secrecy Goals}, institution = {The MITRE Corporation}, year = 2005, type = {MTR}, number = {05B09 Revision~1}, month = {March} } @TechReport{GuttmanThayer05a, author = {Joshua D. Guttman and F. Javier Thayer}, title = {Protocol Security Goals and the Size of Skeletons}, institution = {The MITRE Corp.}, year = 2005, note = {Available at \url{http://www.ccs.neu.edu/home/guttman/sizes_of_skeletons.pdf}, submitted for publication} } @InProceedings{GuttmanThayerZuck01, author = {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck}, title = {The Faithfulness of Abstract Protocol Analysis: Message Authentication}, booktitle = {Proceedings, Eighth ACM Conference on Computer and Communications Security}, year = 2001, month = {November}, organization = {{ACM}} } @InProceedings{GuttmanEtAl04, author = {Joshua D. {Guttman} and F. Javier Thayer and Jay A. Carlson and Jonathan C. Herzog and John D. Ramsdell and Brian T. Sniffen}, title = {Trust Management in Strand Spaces: A Rely-Guarantee Method}, booktitle = {Programming Languages and Systems: 13th European Symposium on Programming}, pages = {325--339}, year = 2004, editor = {David Schmidt}, number = 2986, series = {LNCS}, publisher = {Springer} } @Article{GuttmanThayerZuck03, author = {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck}, title = {The Faithfulness of Abstract Protocol Analysis: Message Authentication}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = 6, pages = {865--891} } @Article{GuttmanThayerZuck04, author = {Joshua D. Guttman and F. Javier Thayer and Lenore D. Zuck}, title = {The Faithfulness of Abstract Protocol Analysis: Message Authentication}, journal = {Journal of Computer Security}, year = 2004, volume = 12, number = 6, pages = {865--891} } @proceedings{DBLP:conf/ifip1-7/2008, editor = {Pierpaolo Degano and Joshua D. Guttman and Fabio Martinelli}, title = {Formal Aspects in Security and Trust, 5th International Workshop, FAST 2008, Malaga, Spain, October 9-10, 2008, Revised Selected Papers}, booktitle = {Formal Aspects in Security and Trust}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5491}, year = {2009}, ee = {http://dx.doi.org/10.1007/978-3-642-01465-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InCollection{Halpern95, author = {Joseph Y. Halpern}, title = {Reasoning about Knowledge: A Survey}, booktitle = {Handbook of Logic in Artificial Intelligence and Logic Programming}, pages = {1--34}, publisher = {Oxford University Press}, year = 1995, editor = {D. Gabbay and C. J. Hogger and J. A Robinson}, volume = 4 } @Article{HalpernvanderMeyden01, author = {Joseph Y. Halpern and Ron {van der Meyden}}, title = {A Logic for {SDSI}'s Linked Local Name Spaces}, journal = {Journal of Computer Security}, year = 2001, volume = 9, number = {1--2}, pages = {47--74} } @Book{HalpernEtAl95, author = {Ronald Fagin and Joseph Y. Halpern and Yoram Moses and Moshe Y. Vardi}, title = {Reasoning about Knowledge}, publisher = {{MIT} Press}, year = 1995, address = {Cambridge, MA} } @Article{HalpernPucella03, author = {Joseph Y. Halpern and Riccardo Pucella}, title = {On the Relationship between Strand Spaces and Multi-Agent Systems}, journal = {{ACM} Transactions on Information and System Security}, year = 2003, volume = 6, number = 1, pages = {43--70}, month = {February} } @InProceedings{HauserJansenMolvaTsudikHerreweghen94, author = "R. Hauser and P. Jansen and R. Molva and G. Tsudik and E. van Herreweghen", title = "Robust and Secure Pasword and Key Change Method", editor = "Dieter Gollmann", number = 875, series = "Lecture Notes in Computer Science", pages = "107--122", booktitle = "Computer Security---{ESORICS} '94", year = 1994, publisher = "Springer" } @InProceedings{HeatherEtAl00, author = {James Heather and Gavin Lowe and Steve Schneider}, title = {How to Prevent Type Flaw Attacks on Security Protocols}, booktitle = {Proceedings, 13th Computer Security Foundations Workshop}, year = 2000, month = {July}, publisher = {{IEEE} CS Press} } @InProceedings{HeatherSchneider00, author = {James Heather and Steve Schneider}, title = {Toward Automatic Verification of Authentication Protocols on an Unbounded Network}, booktitle = {Proceedings, 13th Computer Security Foundations Workshop}, year = 2000, month = {July}, publisher = {{IEEE} CS Press} } @Article{HeatherSchneider05, author = {James A. Heather and Steve A. Schneider}, title = {A Decision Procedure for the Existence of a Rank Function}, journal = {Journal of Computer Security}, year = 2005, note = "Forthcoming." } @Unpublished{HeatherSchneider05a, author = {James A. Heather and Steve A. Schneider}, title = {Infinite/Finite ???}, note = {Submitted for publication}, month = {April}, year = 2005 } @Article{Hellman79, author = "Martin E Hellman", title = "The Mathematics of Public Key Cryptography", journal = "Scientific American", year = 1979, pages = "130-139", month = aug } @TechReport{HerzogGuttman02, author = {Amy L. Herzog and Joshua D. Guttman}, title = {Security Goal Achievement In A Heterogeneous Environment}, institution = {The MITRE Corporation}, year = 2002 } @Unpublished{HerzogEtAl98, author = {Jonathan Herzog and Joshua Guttman and Fred Chase}, title = {A Strand Space Analysis of the {SSH} Version 2 Protocol}, note = {{MITRE} Product {MP} 98B0000056}, month = {September}, year = 1998 } @Unpublished{HerzogEtAl99, author = {Jonathan Herzog and Fred Chase and Joshua Guttman}, title = {A Saying-Logic Analysis of core {DNS} Security}, note = {{MITRE} Product {MP} 99{B}0000039}, year = 1999 } @Unpublished{Herzog00, author = {Jonathan Herzog}, title = {Some Security Concerns Regarding {PPP}--{EAP}--{TLS}}, note = {{MITRE} Product {MP} 00{B}0000019}, year = 2000 } @Unpublished{HerzogEtAl00, author = {Jonathan Herzog and Laura Feinstein and Joshua Guttman}, title = {A Strand Space Analysis of {TLS} 1.0}, note = {{MITRE} Document {MTR} 0{B}0000011}, year = 2000 } @Unpublished{Herzog00b, author = {Jonathan Herzog}, title = {Mobile {IP} Security}, note = {{MITRE} Product {MP} 00{B}0000063}, year = 2000 } @MastersThesis{Herzog02, author = {Jonathan Herzog}, title = {Computational Soundness of Formal Adversaries}, school = {Massachusetts Institute of Technology}, year = 2002 } @InProceedings{Herzog03, author = {Jonathan C. Herzog}, title = {The {Diffie-Hellman} Key-Agreement Scheme in the Strand-Space Model}, booktitle = {16th Computer Security Foundations Workshop}, pages = {234--247}, year = 2003, address = {Asilomar, CA}, month = {June}, publisher = {{IEEE CS} Press} } @TechReport{HerzogEtAl04, author = {Jonathan Herzog and Brian Sniffen and Jay Carlson and Joshua D. Guttman and John D. Ramsdell}, title = {Trust Management with Cryptographic Hardware Assistance}, institution = {The MITRE Corp.}, year = 2003, type = {MTR}, number = {03B0082}, address = {Bedford, MA}, month = {September} } @PhdThesis{Herzog04, author = {Jonathan Herzog}, title = {Computational Soundess for Standard Assumption of Formal Cryptography}, school = {Massachusetts Institute of Technology}, year = 2004 } @Misc{Hitchcock53, author = {Alfred Hitchcock}, title = {I Confess}, howpublished = {Warner Brothers}, month = {March}, year = 1953, note = {\url{http://www.imdb.com/title/tt0045897/}}} @Article{Hoare78, author = {C. A. R. Hoare}, title = {Communicating Sequential Processes}, journal = {CACM}, year = 1978, volume = 21, number = 8, pages = {666--77} } @Book{Hoare85, author = "C. A. R. Hoare", title = "Communicating Sequential Processes", publisher = "Prentice-Hall International", year = 1985, address = "Englewood Cliffs, New Jersey", patron = "Guttman" } @Book{Holzmann91, author = {Gerard Holzmann}, title = {Design and Validation of Computer Protocols}, publisher = {Prentice Hall}, year = 1991 } @Misc{HouselyEtAl99, author = {R. Housley and W. Ford and W. Polk and D. Solo}, title = {Internet {X.509} Public Key Infrastructure Certificate and {CRL} Profile}, howpublished = {{RFC} 2459}, month = {January}, year = 1999 } @Misc{RFC2459, author = {R. Housley and W. Ford and W. Polk and D. Solo}, title = {Internet X.509 Public Key Infrastructure Certificate and CRL Profile}, howpublished = {{RFC} 2459}, month = {January}, year = 1999 } @Misc{RFC3280, author = {R. Housley and W. Polk and W. Ford and D. Solo}, title = {Internet X.509 Public Key Infrastructure Certificate and CRL Profile}, howpublished = {{RFC} 3280}, month = {April}, year = 2002 } @InProceedings{HuiLowe99, author = {Mei Lin Hui and Gavin Lowe}, title = {Safe Simplifying Transformations for Security Protocols}, booktitle = {12th Computer Security Foundations Workshop Proceedings}, year = 1999, publisher = {{IEEE} CS Press}, pages = {32--43}, month = {June} } @article{HuiLowe01, author = {Mei Lin Hui and Gavin Lowe}, title = {Fault-Preserving Simplifying Transformations for Security Protocols}, journal = {Journal of Computer Security}, volume = 9, number = {1/2}, year = 2001, pages = {3-46}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{HwangChen95, author = "Tzonelih Hwang and Yung-Hsiang Chen", title = "On the security of {SPLICE/AS}: The authentication system in {WIDE Internet}", journal = "Information Processing Letters", year = 1995, volume = 53, pages = "97--101" } @Article{HwangLeeLiKoChen95, author = "Tzonelih Hwang and Narn-Yoh Lee and Chuang-Ming Li and Ming-Yung Ko and Yung-Hsiang Chen", title = "Two Attacks on {Neuman-Stubblebine} Authentication Protocols", journal = "Information Processing Letters", year = 1995, volume = 53, pages = "103--107" } @InProceedings{Integrating01, author = {P. Loscocco and S. Smalley}, title = {Integrating Flexible Support for Security Policies into the {Linux} Operating System}, booktitle = {Proceedings of the FREENIX Track of the 2001 USENIX Annual Technical Conference}, year = 2001 } @Misc{ikev2:id:17, author = {Charlie {Kaufman, ed.}}, title = {Internet Key Exchange ({IKEv2}) Protocol}, howpublished = {Internet Draft}, month = {September}, year = 2004, note = {Available at \url{http://www.ietf.org/internet-drafts/draft-ietf-ipsec-ikev2-17.txt}} } @Misc{IPchains00, key = {IPchains00}, author = {Rusty Russell}, title = {Linux IP Firewalling Chains}, howpublished = {Linux Howto}, month = {October}, year = 2000, note = {URL~\url{http://www.netfilter.org/ipchains/}} } @Misc{IPfilter00, key = {IPfilter00}, author = {Darren Reed}, title = {IP Filter}, howpublished = {Download Web Page}, month = {December}, year = 2002, note = {URL~\url{http://coombs.anu.edu.au/~avalon/}} } @Manual{ISOIEC9798-1, title = "Information Technology - Security techniques --- Entity Authentication Mechanisms Part 1: General Model", organization = "ISO/IEC", year = 1991 } @Manual{ISOIECDIS9798-2, title = "Information Technology - Security techniques --- Entity Authentication Mechanisms Part 2: Entity authentication using symmetric techniques", organization = "ISO/IEC", year = 1993 } @Manual{ISOIECDIS9798-3, title = "Information Technology - Security techniques --- Entity Authentication Mechanisms Part 3: Entity authentication using a public key algorithm", organization = "ISO/IEC", year = 1993 } @Misc{ITUMSC99, author = {ITU}, title = {Message Sequence Chart ({MSC})}, howpublished = {Recommendation Z.120}, year = 1999} @Unpublished{ITTCweb, author = "D. Boneh and T. Raj and M. Malkin and T. Wu", title = "Intrustion Tolerance via Threshold Cryptography", note = "http://crypto.stanford.edu/\~dabo/ITTC" } @InProceedings{JiwaSeberryZheng94, author = "A Jiwa and J Seberry and Y Zheng", title = "Beacon Based Authentication", editor = "Dieter Gollmann", number = 875, series = "Lecture Notes in Computer Science", pages = "125--142", booktitle = "Computer Security --- {ESORICS} '94", year = 1994, publisher = "Springer" } @Article{Jones83, author = {Cliff B. Jones}, title = {Tentative Steps toward a Development Method for Interfering Programs}, journal = {{ACM} Transactions on Programming Languages and Systems}, year = {1983}, OPTkey = {}, OPTvolume = {5}, OPTnumber = {4}, OPTpages = {596--619}, OPTmonth = {}, OPTnote = {}, OPTannote = {} } @Unpublished{JurjensWimmel01, author = {Jan {J{\"u}rjens} and Guido Wimmel}, title = {Specification-Based Testing of Firewalls}, note = {Submitted for publication}, year = {2001}, } @InProceedings{KailarGligor91, author = "R. Kailar and Virgil D. Gligor", title = "On Belief Evolution in Authentication Protocols", pages = "103--116", booktitle = "Proceedings of the Computer Security Foundations Workshop IV", year = 1991, publisher = "IEEE CS Press" } @article{kaliski2001unknown, title={{An unknown key-share attack on the MQV key agreement protocol}}, author={Burton S. Kaliski}, journal={{ACM} Transactions on Information and System Security}, volume=4, number=3, pages={275--288}, issn={1094-9224}, year=2001, publisher={ACM} } @article{kapur2003unification, title={{An E-unification algorithm for analyzing protocols that use modular exponentiation}}, author={Deepak Kapur and Paliath Narendran and Lida Wang}, journal={Rewriting Techniques and Applications}, year={2003}, publisher={Springer} } @article{DBLP:journals/joc/KatzY07, author = {Jonathan Katz and Moti Yung}, title = {Scalable Protocols for Authenticated Group Key Exchange}, journal = {J. Cryptology}, volume = {20}, number = {1}, year = {2007}, pages = {85-113}, ee = {http://dx.doi.org/10.1007/s00145-006-0361-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{KehneSchoenwalderLangendorfer92, author = "A. Kehne and J. Sch{\"{o}}enw{\"{a}}lder and H. Langend{\"{o}}rfer", title = "A Nonce-Based Protocol for Multiple Authentication", journal = "Operating Systems Review", year = 1992, volume = 26, number = 4, pages = "84--89" } @InProceedings{KelseySchneierWagner97, author = "John Kelsey and Bruce Schneier and David Wagner", title = " Protocol Interactions and the Chosen Protocol Attack", booktitle = "Security Protocols Workshop", year = 1998, ignorepages = "91--104", publisher = "Springer" } @InProceedings{Kemmerer87, author = "R. A. Kemmerer", title = "Using Formal Verification Techniques to Analyse Encryption Protocols", pages = "134--139", booktitle = "Proceedings of the 1987 IEEE Symposium on Research in Security and Privacy", year = 1987, publisher = "IEEE CS Press" } @Article{Kemmerer89, author = "R. A. Kemmerer", title = "Analysing Encryption Protocols Using Formal Verification Techniques", journal = "IEEE Journal on Selected Areas in Communications", year = 1989, volume = 7, number = 4, pages = "448--457" } @InProceedings{KesslerWedel94, author = "V. Kessler and G. Wedel", title = "AUTLOG --- An advanced logic of authentication", pages = "90--99", booktitle = "Proceedings of the Computer Security Foundations Workshop VII", year = 1994 } @InProceedings{Kocher96, author = "Paul C. Kocher", title = "Timing Attacks on Implementations of {Diffie-Hellman}, {RSA}, {DSS}, and Other Systems", pages = "104--113", editor = "Neal Koblitz", number = 1109, series = "Lecture Notes in Computer Science", booktitle = "Advances in Cryptology --- {CRYPTO} '96", year = 1996, publisher = "Springer" } @inproceedings{KlayVigneron08, author = {Francis Klay and Laurent Vigneron}, title = {Automatic Methods for Analyzing Non-repudiation Protocols with an Active Intruder}, booktitle = {Formal Aspects in Security and Trust}, year = {2008}, pages = {192-209}, ee = {http://dx.doi.org/10.1007/978-3-642-01465-9_13}, crossref = {DBLP:conf/ifip1-7/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{KocherJaffeJun99, author = "Paul Kocher and Joshua Jaffe and Benjamin Jun", title = "Differential Power Analysis", journal = "Lecture Notes in Computer Science", volume = "1666", pages = "388--397", year = "1999" } @Misc{KohlNeuman93, author= "J. Kohl and C. Neuman", title= "The {Kerberos} Network Authentication Service (V5)", howpublished="{RFC} 1510", month=sep, year= 1993 } @Misc{RFC1510, author= "J. Kohl and C. Neuman", title= "The {Kerberos} Network Authentication Service (V5)", howpublished="{RFC} 1510", month=sep, year= 1993 } @InProceedings{KommerlingKuhn99, author = "Oliver K{\"{o}}mmerling and Markus G. Kuhn", title = "Design Principles for Tamper-Resistant Smartcard Processors", pages = "9--20", booktitle = "Proceedings of the USENIX Workshop on Smartcard Technology", year = 1999 } @conference{krawczyk2005hmqv, title={{HMQV: A high-performance secure {Diffie-Hellman} protocol}}, author={Krawczyk, H.}, booktitle={Advances in Cryptology--CRYPTO 2005}, pages={546--566}, year={2005}, organization={Springer} } @InProceedings{KremerRaskin02, author = {Steve Kremer and Jean-Fran{\c{c}}ois Raskin}, title = {Game Analysis of Abuse-Free Contract Signing}, booktitle = {Proceedings, 15th Computer Security Foundations Workshop}, year = 2002, month = {June}, publisher = {{IEEE} CS Press} } @InProceedings{kuesters2009using, title={Using {ProVerif} to analyze protocols with {Diffie-Hellman} exponentiation}, author={Ralf K{\"u}sters and Tomasz Truderung}, booktitle={{IEEE} Computer Security Foundations Symposium}, pages={157--171}, issn={1063-6900}, year=2009, organization={IEEE} } @inproceedings{kusters2011composition, title={Composition theorems without pre-established session identifiers}, author={K{\"u}sters, R. and Tuengerthal, M.}, booktitle={CCS}, pages={41--50}, year={2011}, organization={ACM} } @article{kunz2006security, title={{About the Security of MTI/C0 and MQV}}, author={Sebastian Kunz-Jacques and David Pointcheval}, journal={Security and Cryptography for Networks}, pages={156--172}, year={2006}, publisher={Springer} } @Article{LadkinLeue94, author = {Peter B. Ladkin and Stefan Leue}, title = {Interpreting Message Flow Graphs}, journal = {Formal Aspects of Computing}, year = 1994, volume = 3, number = 1 } @InProceedings{LakhnechEtAl03, author = {L. Bozga and Y. Lakhnech and M. Perin}, title = {Pattern-based Abstraction for Verifying Secrecy in Protocols}, booktitle = {Tools and Algorithms for Construction and Analysis of Systems {(TACAS)}}, year = 2003, number = 2619, series = {LNCS}, publisher = {Springer}} @article{lamacchia2007stronger, title={Stronger security of authenticated key exchange}, author={LaMacchia, B. and Lauter, K. and Mityagin, A.}, journal={Provable Security}, volume = 4784, series = {LNCS}, note = {DOI: \url{dx.doi.org/10.1007/978-3-540-75670-5_1}}, year=2007, publisher={Springer} } @Article{Lamport78, author = {Leslie Lamport}, title = {Time, clocks and the ordering of events in a distributed system}, journal = {CACM}, year = 1978, volume = 21, number = 7, pages = {558–-565}} @Article{LampsonEtAl92, author = {Butler Lampson and Mart{\'\i}n Abadi and Michael Burrows and Edward Wobber}, title = {Authentication in Distributed Systems: Theory and Practice}, journal = {{ACM} Transactions on Computer Systems}, year = 1992, volume = 10, number = 4, pages = {265--310}, month = {November} } @article{law2003efficient, title={{An efficient protocol for authenticated key agreement}}, author={Law, L. and Menezes, A. and Qu, M. and Solinas, J. and Vanstone, S.}, journal={Designs, Codes and Cryptography}, volume={28}, number={2}, pages={119--134}, issn={0925-1022}, year={2003}, publisher={Springer} } @Manual{Leroy00, title = {The Objective Caml System}, author = {Xavier Leroy and Damien Doligez and Jacques Garrigue and Didier R\'emy and J\'er\^ome Vouillon}, organization = {{INRIA}}, address = {\texttt{http://caml.inria.fr/}}, note = {Version 3.00}, year = 2000 } @Misc{LeroyCryptokit05, author = {Xavier Leroy}, title = {Cryptokit}, howpublished = {Sofwtare available via \url{http://pauillac.inria.fr/~xleroy/software.html}}, month = {April}, year = 2005, note = {Version 1.3} } @article{li2012secure, author = {Ming Li and Sucheng Yu and Joshua D. Guttman and Wenjing Lou and Kui Ren}, title = {Secure ad-hoc trust initialization and key management in wireless body area networks}, journal = {ACM Transactions on Sensor Networks (TOSN)}, volume = 9, number = 2, pages = 18, year = 2013 } @InProceedings{LiEtAl02, author = {Ninghui Li and John C. Mitchell and William H. Winsborough}, title = {Design of a Role-Based Trust Management Framework}, booktitle = {Proceedings, 2002 IEEE Symposium on Security and Privacy}, year = 2002, organization = {May}, pages = {114--130}, publisher = {IEEE CS Press} } @InProceedings{LiEtAl03a, author = {Ninghui Li and William H. Winsborough and John C. Mitchell}, title = {Beyond Proof-of-Compliance: Safety and Availability Analysis on Trust Management}, booktitle = {Proceedings, 2003 IEEE Symposium on Security and Privacy}, year = 2003, organization = {May}, publisher = {IEEE CS Press} } @Article{LiEtAl03, author = {Ninghui Li and William H. Winsborough and John C. Mitchell}, title = {Distributed Credential Chain Discovery in Trust Management}, journal = {Journal of Computer Security}, year = 2003, month = feb, volume = 11, number = 1, pages = {35--86} } @Article{Liebl93, author = "Armin Liebl", title = "Authentication in Distributed Systems: A Bibliography", journal = "Operating Systems Review", year = 1993, volume = 27, number = 4, pages = "122--136", month = oct } @Article{Lowe95, author = "Gavin Lowe", title = "An Attack on the {Needham-Schroeder} Public Key Authentication Protocol", journal = "Information Processing Letters", year = 1995, volume = 56, number = 3, pages = "131--136", month = nov } @InProceedings{Lowe96, author = {Gavin Lowe}, title = {Some New Attacks upon Security Protocols}, booktitle = {Proceedings of the Computer Security Foundations Workshop IX}, year = 1996, publisher = {{IEEE} CS Press} } @InProceedings{Lowe96a, author = {Gavin Lowe}, title = {Breaking and Fixing the {Needham-Schroeder} Public-Key Protocol using {FDR}}, booktitle = {Proceeedings of {\sc tacas}}, volume = 1055, series = {LNCS}, year = 1996, pages = {147--166} } @InProceedings{Lowe97, author = {Gavin Lowe}, title = {A Hierarchy of Authentication Specifications}, booktitle = {10th Computer Security Foundations Workshop Proceedings}, year = 1997, publisher = {{IEEE} CS Press}, pages = {31--43} } @InProceedings{Lowe97a, author = {Gavin Lowe}, title = {Casper: A Compiler for the Analysis of Security Protocols}, booktitle = {10th Computer Security Foundations Workshop Proceedings}, year = 1997, publisher = {{IEEE} CS Press}, pages = {18--30} } @InProceedings{Lowe98, author = {Gavin Lowe}, title = {Toward a Completeness Result for Model Checking of Security Protocols}, booktitle = {11th Computer Security Foundations Workshop Proceedings}, year = 1998, publisher = {{IEEE} CS Press}, pages = {96--105} } @InProceedings{Lowe02, author = {Gavin Lowe}, title = {Analyzing Protocols subject to Guessing Attacks}, booktitle = {WITS: Workshop on Issues in the Theory of Security}, year = 2002, month = {January}, note = {Available at http://www.dsi.unive.it/IFIPWG1\_7/wits2002.html} } @Article{Lowe03, author = {Gavin Lowe}, title = {Analyzing Protocols subject to Guessing Attacks}, journal = {Journal of Computer Security}, year = 2003, note = {Forthcoming} } @TechReport{LoweAuty07, author = {Gavin Lowe and Michael Auty}, title = {A Calculus for Security Protocol Development}, institution = {Oxford University Computing Laboratory}, year = 2007, month = {March}} @InProceedings{WuMalkinBoneh99, author = "T. Wu and M. Malkin and D. Boneh", title = "Building Intrusion Tolerant Applications", pages = "79--91", booktitle = "Proceedings of the 8th USENIX Security Symposium", year = 1999 } @InProceedings{MalkinWuBoneh99, author = "M. Malkin and T. Wu and D. Boneh", title = "Experimenting with Shared Generation of RSA Keys", pages = "43--56", booktitle = "Proceedings of the Internet Society's 1999 Symposium on Network and Distributed System Security (SNDSS)", year = 1999 } @InProceedings{MaoBoyd93, author = "Wenbo Mao and Colin Boyd", title = "Towards the Formal Analysis of Security Protocols", pages = "147--158", booktitle = "Proceedings of the Computer Security Foundations Workshop VI", year = 1993, publisher = "IEEE CS Press" } @InProceedings{Maneki99, author = {Al Maneki}, title = {Honest functions and their Application to the Analysis of Cryptographic Protocols}, booktitle = {Proceedings of the 12th Computer Security Foundations Workshop}, year = 1999, month = {June}, publisher = {IEEE CS Press} } @InProceedings{MaoBoyd94a, author = "Wenbo Mao and Colin Boyd", title = "Development of Authentication Protocols: Some Misconceptions and a New Approach", booktitle = "Proceedings 7th Computer Security Foundations Workshop", publisher = "IEEE CS Press", year = 1994, pages = "178--186" } @InProceedings{MaoBoyd94b, author = "Wenbo Mao and Colin Boyd", title = "On Strengthening Authentication protocols to Foil Cryptanalysis", editor = "Dieter Gollmann", number = 875, series = "Lecture Notes in Computer Science", pages = "193--204", booktitle = "Computer Security---ESORICS 94", year = 1994, publisher = "Springer", month = nov } @InProceedings{MarreroEtAl97, author = {Will Marrero and Edmund Clarke and Somesh Jha}, title = {A Model Checker for Authentication Protocols}, booktitle = {Proceedings of the {DIMACS} Workshop on Design and Verification of Security Protocols}, year = 1997, editor = {Cathy Meadows and Hilary Orman}, month = {September}, organization = {{DIMACS}, Rutgers University} } @Article{MaurerMassey93, author = {Ueli Maurer and James Massey}, title = {Cascade Ciphers: The Importance of Being First}, journal = {Journal of Cryptology}, year = 1993, volume = 6, number = 1, pages = {55-61} } @Article{Massey88, author = "James L. Massey", title = "An Introduction to Contemporary Cryptology", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, pages = "533-549", month = may } @Article{Meadows92, author = "Catherine Meadows", title = "Applying Formal Methods to the Analysis of a Key Management Protocol", journal = "Journal of Computer Security", year = 1992, volume = 1, number = 1, pages = "5--35", ISSN = "0926-227X" } @article{meadows1996nrl, title={The {NRL} protocol analyzer: An overview}, author={Meadows, C.}, journal={The Journal of Logic Programming}, volume={26}, number={2}, pages={113--131}, year={1996}, publisher={Elsevier} } @InProceedings{MayerEtAl00, author = {Alain Mayer and Avishai Wool and Elisha Ziskind}, title = {Fang: A Firewall Analysis Engine}, booktitle = {Proceedings, {IEEE} Symposium on Security and Privacy}, pages = {177--187}, year = 2000, month = {May}, publisher = {IEEE CS Press} } @InProceedings{Meadows94, author = {Catherine Meadows}, title = {A Model of Computation for the {NRL} Protocol Analyzer}, booktitle = {Proceedings of the Computer Security Foundations Workshop VII}, year = 1994, organization = {{IEEE}}, publisher = {{IEEE} CS Press}, pages = {84--89} } @InProceedings{Meadows99, author = {Catherine Meadows}, title = {Analysis of the {Internet} {Key} {Exchange} Protocol using the {NRL} Protocol Analyzer}, booktitle = {Proceedings, 1999 IEEE Symposium on Security and Privacy}, year = 1999, month = {May}, publisher = {IEEE CS Press} } @InProceedings{Meadows00, author = {Catherine Meadows}, title = {Open Issues in Formal Methods for Cryptographic Protocol Analysis}, booktitle = {{DISCEX} Workshop}, year = 2000, month = {January}, organization = {DARPA} } @InProceedings{Meadows00a, author = {Catherine Meadows}, title = {Invariant Generation Techniques in Cryptographic Protocol Analsyis}, booktitle = {Proceedings, 13th Computer Security Foundations Workshop}, year = 2000, month = {July}, publisher = {{IEEE} CS Press} } @inproceedings{cervesato2005encapsulated, title={An encapsulated authentication logic for reasoning about key distribution protocols}, author={Cervesato, I. and Meadows, C. and Pavlovic, D.}, booktitle={Computer Security Foundations, 2005. CSFW-18 2005. 18th IEEE Workshop}, pages={48--61}, year={2005}, organization={IEEE} } @article{pavlovic2006deriving, title={Deriving secrecy in key establishment protocols}, author={Pavlovic, D. and Meadows, C.}, journal={Computer Security--ESORICS 2006}, pages={384--403}, year={2006}, publisher={Springer} } @book{menezes2005another, title={{Another look at HMQV}}, author={Menezes, A. and University of Waterloo. Dept. of Combinatorics and Optimization and University of Waterloo. Faculty of Mathematics}, year={2005}, publisher={Citeseer} } @Article{menezes2007another, author = {Alfred Menezes}, title = {Another look at {HMQV}}, journal = {Journal of Mathematical Cryptology}, year = 2007, volume = 1, pages = {47--64} } @Article{MillenClarkFreedman87, author = "J. K. Millen and S. C. Clark and S. B. Freedman", title = "The {Interrogator}: Protocol Security Analysis", journal = "IEEE Transactions on Software Engineering", year = 1987, volume = 13, number = 2, pages = "274--288", month = feb } @InProceedings{Millen95, author = {Jonathan K. Millen}, title = {The {Interrogator} Model}, booktitle = {Proceedings of the 1995 IEEE Symposium on Security and Privacy}, year = 1995, pages = {251--60} } @Article{Millen03, author = {Jonathan K. Millen}, title = {On the Freedom of Encryption}, journal = {Information Processing Letters}, year = 2003, volume = 86, number = 6, pages = {329--333} } @TechReport{MillenMuller01, author = {Jonathan Millen and Frederic Muller}, title = {Cryptographic Protocol Generation from {CAPSL}}, institution = {{SRI} International}, year = 2001, number = {SRI-CSL-01-07}, month = {December} } @InProceedings{MillenRuess00, author = {Jonathan K. Millen and Harald Ruess}, title = {Protocol-Independent Secrecy}, booktitle = {Proceedings, 2000 IEEE Symposium on Security and Privacy}, year = 2000, month = {May}, publisher = {IEEE CS Press} } @InProceedings{MillenShmatikov01, author = {Jonathan K. Millen and Vitaly Shmatikov}, title = {Constraint Solving for Bounded-Process Cryptographic Protocol Analysis}, booktitle = {CCS}, pages = {166--175}, year = 2001, organization = {ACM} } @TechReport{MillerNeumanSchillerSaltzer87, author = "S. P. Miller and C. Neuman and J. I. Schiller and Jerry H. Saltzer", title = "Project Athena Technical Plan (Section E.2.1)", institution = "MIT", year = 1987, month = jul } @Book{Milner89, author = "Robin Milner", title = "Communication and Concurrency", publisher = "Prentice-Hall International", year = 1989, address = "Englewood Cliffs", patron = "Guttman" } @InProceedings{Minear95, author = "Spencer E. Minear", title = "Providing Policy Control Over Object Operations in a Mach Based System", booktitle = "Proceedings of the Fifth USENIX UNIX Security Symposium", pages = "141--156", year = 1995, month = "June" } @Misc{Mockapetris87, author = {P. Mockapetris}, title = {Domain Names - Concepts and Facilities}, howpublished = {{RFC} 1034}, month = {November}, year = 1987 } @Misc{RFC1034, author = {P. Mockapetris}, title = {Domain Names - Concepts and Facilities}, howpublished = {{RFC} 1034}, month = {November}, year = 1987 } @Misc{Mockapetris87a, author = {P. Mockapetris}, title = {Domain Names - Implementation and Specification}, howpublished = {{RFC} 1035}, month = {November}, year = 1987 } @Misc{RFC1035, author = {P. Mockapetris}, title = {Domain Names - Implementation and Specification}, howpublished = {{RFC} 1035}, month = {November}, year = 1987 } @article{modersheim2009secure, title={Secure pseudonymous channels}, author={M{\"o}dersheim, S. and Vigan{\`o}, L.}, journal={ESORICS}, pages={337--354}, year={2009}, series={LNCS} } @Article{Moore88, author = "Judy H. Moore", title = "Protocol Failures in Cryptosystems", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, month = may } @InProceedings{MooreAndersonKuhn00, author = "S. Moore and R. Anderson and M. Kuhn", title = "Improving Smartcard Security using Self-Timed Circuit Technology", booktitle = "Fourth AciD-WG Workshop", year = 2000 } @InProceedings{MooreEtAl02, author = "Simon Moore and Ross Anderson and Paul Cunningham and Robert Mullins and George Taylor", title = "Improving Smart Card Security using Self-Timed Circuits", booktitle = "Eigth International Symposium on Advanced Research in Asynchronous Circuits and Systems", year = 2002 } @InProceedings{Moser89, author = "Louise E. Moser", title = "A Logic of Knowledge and Belief about Computer Security", editor = "J Thomas Haigh", pages = "57--63", booktitle = "Proceedings of the Computer Security Foundations Workshop III", organization = "IEEE", publisher = "CS Press of the IEEE", year = 1989 } @InProceedings{MitchellEtAl97, author = {John C. Mitchell and Mark Mitchell and Ulrich Stern}, title = {Automated Analysis of Cryptographic Protocols using {Mur}$\varphi$}, booktitle = {Proceedings, 1997 IEEE Symposium on Security and Privacy}, pages = {141--151}, year = 1997, organization = {IEEE}, publisher = {CS Press of the IEEE} } @InProceedings{MostrousEtAl09, author = {Dimitris Mostrous and Nobuko Yoshida and Kohei Honda}, title = {Global principal typing in partially commutative asynchronous sessions}, booktitle = {{ESOP} Proceedings}, year = 2009, series = {LNCS}, month = {March}} @Misc{rfc2560, author = {M.Myers and R.Ankney and A.Malpani and S.Galperin and C. Adams}, title = {X.509 Internet Public Key Infrastructure: Online Certificate Status Protocol - OCSP}, howpublished = {Internet Request for Comments 2560}, month = {June}, year = 1999, note = {Available at \texttt{http://www.ietf.org/rfc/rfc2560.txt}} } @Article{NeedhamSchroeder78, author = "Roger Needham and Michael Schroeder", title = "Using Encryption for Authentication in Large Networks of Computers", journal = "{CACM}", year = 1978, volume = 21, number = 12, pages= {993--999}, month = dec } @Article{NeedhamSchroeder87, author = "Roger M. Needham and M. D. Schroeder", title = "Authentication Revisited", journal = "Operating Systems Review", year = 1987, volume = 21, number = 7, pages = "7--7", month = jan } @Article{Nessett90, author = "Daniel M. Nessett", title = "A Critique of the {Burrows}, {Abadi} and {Needham} Logic", journal = "ACM Operating Systems Review", year = 1990, volume = 24, number = 2, pages = "35--38", month = apr } @Article{NeumanStubblebine93, author = "B. Clifford Neuman and Stuart G. Stubblebine", title = "A Note on the Use of Timestamps as Nonces", journal = "Operating Systems Review", year = 1993, volume = 27, number = 2, pages = "10--14", month = apr } @Article{Ng03, author = {Siaw-Lynn Ng}, title = {Posets and protocols: Picking the right three-party protocol}, journal = {{IEEE} Journal on Selected Areas in Communication}, month = {January}, pages = "55--61", year = 2003 } @Misc{NuSMV01, key = {NuSMV}, title = {{NuSMV}: a new symbolic model checker}, howpublished = {URL \url{http://sra.itc.it/tools/nusmv}}, year = 2001 } @InProceedings{OlawskyEtAl96, author = "D. Olawsky and T. Fine and E. Schneider and R. Spencer", title = "Developing and Using a Policy Neutral Access Control Policy", booktitle = "Proceedings of the New Security Paradigms Workshop", year = 1996, month = "September" } @InProceedings{Ottawa01, author = {P. Loscocco and S. Smalley}, title = {Meeting Critical Security Objectives with Security-Enhanced {Linux}}, booktitle = {Proceedings of the 2001 Ottawa Linux Symposium}, year = 2001 } @Article{OtwayRees87, author = "D. Otway and O. Rees", title = "Efficient and Timely Mutual Authentication", journal = "Operating Systems Review", year = 1987, volume = 21, number = 1, pages = "8--10", month = jan } @Misc{PCKS1, author = {{RSA} Laboratories}, title = {{PCKS} \#1: {RSA} Encryption Standard}, month = {November}, year = 1993, note = {Version 1.5} } @InProceedings{Patel97, author = {Sarvar Patel}, title = {Number Theoretic Attacks on Secure Password Schemes}, booktitle = {Proceedings of the 1997 {IEEE} Symposium on Security and Privacy}, pages = {236--247}, year = 1997, month = {May}, publisher = {{IEEE} CS Press} } @Book{Paulson94, author = {L. C. Paulson}, title = {Isabelle: A Generic Theorem Prover}, publisher = {Springer Verlag}, year = 1994, number = 828, series = {LNCS} } @InProceedings{Paulson97, author = {Lawrence C. Paulson}, title = {Proving Properties of Security Protocols by Induction}, booktitle = {10th {IEEE} Computer Security Foundations Workshop}, year = 1997, publisher = {IEEE CS Press}, pages = {70--83} } @InProceedings{Paulson97a, author = {Lawrence C. Paulson}, title = {Mechanized Proofs of a Recursive Authentication Protocol}, booktitle = {10th {IEEE} Computer Security Foundations Workshop}, year = 1997, publisher = {IEEE CS Press}, pages = {84--94} } @TechReport{Paulson97b, author = {Lawrence C. Paulson}, title = {On Two Formal Analyses of the {Yahalom} Protocol}, institution = {Cambridge University Computer Laboratory}, year = 1997, number = 432, month = {July}, annote = {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html} } @Article{Paulson97c, author = {Lawrence C. Paulson}, title = {Relations between secrets: Two Formal Analyses of the {Yahalom} Protocol}, journal = {Journal of Computer Security}, year = 2001, annote = {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html} } @Article{Paulson97d, author = {Lawrence C. Paulson}, title = {Relations between secrets: Two Formal Analyses of the {Yahalom} Protocol}, journal = {Journal of Computer Security}, year = 2001, note = {Also available as Cambridge University Computer Laboratory Technical Report 432 (1997)}, annote = {http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html} } @Article{Paulson98, author = {Lawrence C. Paulson}, title = {The Inductive Approach to Verifying Cryptographic Protocols}, journal = {Journal of Computer Security}, year = 1998, note = {Also Report 443, Cambridge University Computer Lab}, annote = {From http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html} } @Article{Paulson99, author = {Lawrence C. Paulson}, title = {Inductive analysis of the {Internet} protocol {TLS}}, journal = {ACM Transactions on Computer and System Security}, year = 1999, annote = {From http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html} } @Article{PfitzmannEtAl00, author = {Birgit Pfitzmann and Matthias Schunter and Michael Waidner}, title = {Cryptographic Security of Reactive Systems}, journal = {Electronic Notes in Theoretical Computer Science}, year = 2000, volume = 32 } @InProceedings{PfitzmannSchunterWaidner1998, Author = {Birgit Pfitzmann and Matthias Schunter and Michael Waidner}, Title = {Optimal Efficiency of Optimistic Contract Signing}, BookTitle = {Seventeenth Annual {ACM} Symposium on Principles of Distributed Computing}, Pages = {113--122}, Address = {New York}, Organization = {ACM}, month = may, added-by = {aso}, year = 1998, } @InProceedings{PfitzmannWaidner00, author = {Birgit Pfitzmann and Michael Waidner}, title = {Composition and Integrity Preservation of Secure Reactive Systems}, booktitle = {Proceedings, Seventh ACM Conference of Communication and Computer Security}, year = 2000, month = {November}, organization = {{ACM}} } @InProceedings{PfitzmannWaidner01, author = {Birgit Pfitzmann and Michael Waidner}, title = {A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission}, booktitle = {Proceedings, 2001 IEEE Symposium on Security and Privacy}, year = 2001, month = May, publisher = {{IEEE CS} Press}, url = "citeseer.nj.nec.com/pfitzmann00model.html", note = {Preprint at \url{http://iacr.org/2000/066.ps.gz}} } @Book{Prawitz65, author = {Dag Prawitz}, title = {Natural Deduction: A Proof-Theoretic Study}, publisher = {Almqvist and Wiksel}, year = 1965, address = {Stockholm} } @Unpublished{prover9, author = {Bill W. McCune}, title = {Prover9}, note = {\url{http://www.cs.unm.edu/~mccune/mace4/}}, OPTkey = {}, OPTmonth = {}, OPTyear = {}, OPTannote = {} } @InProceedings{PurdyEtAl82, author = {G. B. Purdy and G. J. Simmons and J. A. Studier}, title = {A Software Protection Scheme}, booktitle = {1982 IEEE Symposium on Security and Privacy}, year = 1982, pages = {99--103} } @Book{PearsonEtAl03, author = {Boris Balacheff and Liqun Chen and Siani Pearson and David Plaquin and Graeme Proudler}, title = {Trusted Computing Platforms: {TCPA} Technology in Context}, publisher = {Prentice Hall PTR}, year = 2003, address = {Upper Saddle River, NJ} } @InProceedings{QuisquaterSamyde01, author = "J.J. Quisquater and D. Samyde", title = "ElectroMagnetic Analysis (EMA): Measures and Countermeasures for Smart Cards", booktitle = "International Conference on Research in Smart Cards (E-smart 2001)", pages = "200--210", month = "September", year = 2001 } @Manual{cpsaspec09, title = {The {CPSA} Specification: A Reduction System for Searching for Shapes in Cryptographic Protocols}, OPTkey = {}, author = {John D.~Ramsdell and Joshua D.~Guttman and Moses D.~Liskov and Paul D.~Rowe}, organization = {The MITRE Corporation}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = 2009, note = {In \url{http://hackage.haskell.org/package/cpsa} source distribution, \texttt{doc} directory}, OPTannote = {} } @Manual{cpsadesign09, title = {{CPSA} Design}, OPTkey = {}, author = {John D.~Ramsdell and Joshua D.~Guttman}, organization = {The MITRE Corporation}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = 2009, note = {In \url{http://hackage.haskell.org/package/cpsa} source distribution, \texttt{doc} directory}, OPTannote = {} } @Manual{cpsaprimer09, title = {{CPSA} Primer}, OPTkey = {}, author = {John D.~Ramsdell and Joshua D.~Guttman}, organization = {The MITRE Corporation}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = 2009, note = {In \url{http://hackage.haskell.org/package/cpsa} source distribution, \texttt{doc} directory}, OPTannote = {} } @Manual{cpsaoverview09, title = {{CPSA} Overview}, OPTkey = {}, author = {John D.~Ramsdell and Joshua D.~Guttman}, organization = {The MITRE Corporation}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = 2009, note = {In \url{http://hackage.haskell.org/package/cpsa} source distribution, \texttt{doc} directory}, OPTannote = {} } @Manual{cpsauser09, title = {{CPSA} User Guide}, OPTkey = {}, author = {John D.~Ramsdell}, organization = {The MITRE Corporation}, OPTaddress = {}, OPTedition = {}, OPTmonth = {}, year = 2009, note = {In \url{http://hackage.haskell.org/package/cpsa} source distribution, \texttt{doc} directory}, OPTannote = {} } @Misc{cpsa09, author = {John D. Ramsdell and Joshua D. Guttman}, title = {{CPSA}: A cryptographic protocol shapes analyzer}, booktitle = {Hackage}, publisher = {The MITRE Corporation}, year = 2009, note = {\url{http://hackage.haskell.org/package/cpsa}}} @Misc{cpsa16, author = {John D. Ramsdell and Joshua D. Guttman and Moses Liskov}, title = {{CPSA}: A cryptographic protocol shapes analyzer}, booktitle = {Hackage}, publisher = {The MITRE Corporation}, year = 2016, note = {\url{http://hackage.haskell.org/package/cpsa}}} @Misc{cpsa17, author = {John D. Ramsdell and Joshua D. Guttman}, title = {{CPSA4}: A cryptographic protocol shapes analyzer}, booktitle = {Hackage}, publisher = {The MITRE Corporation}, year = 2017, note = {\url{https://github.com/mitre/cpsaexp}}} @Misc{agum09, author = {John D. Ramsdell}, title = {{AGUM}: Unification and Matching in an Abelian Group}, booktitle = {Hackage}, publisher = {The MITRE Corporation}, year = 2009, note = {\url{http://hackage.haskell.org/package/agum}} } @InProceedings{KepserRichts99, author = {Stephan Kepser and J\"{o}rn Richts}, title = {Optimisation Techniques for Combining Constraint Solvers}, booktitle = {Frontiers of Combining Systems 2}, pages = {193--210}, year = 1999, editor = {Maarten de Rijke and Dov Gabbay}, address = {Asmsterdam}, publisher = {Research Studies Press/Wiley}, note = {\url{http://tcl.sfs.uni-tuebingen.de/~kepser/papers/optimisation.ps.gz}}} @PhdThesis{Liu12, author = {Zhiqiang Liu}, title = {Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis}, school = {Clarkson University}, year = 2012, month = sep, note = {\url{http://people.clarkson.edu/~clynch/papers/}}} @book{Knuth81, author = {Donald E. Knuth}, title = {The Art of Computer Programming, Volume {II:} Seminumerical Algorithms, 2nd Edition}, publisher = {Addison-Wesley}, year = {1981}, isbn = {0-201-03822-6}, timestamp = {Thu, 03 Jan 2002 11:51:07 +0100}, biburl = {http://dblp.org/rec/bib/books/aw/Knuth81}, bibsource = {dblp computer science bibliography, http://dblp.org} } @Misc{rfc1661, author = {W. Simpson}, title = {The Point--to--Point Protocol}, howpublished = {RFC 1661}, month = {July}, year = 1994 } @Misc{rfc2420, author = {H. Jummert}, title = {The {PPP} Triple--{DES} Encryption Protocol}, howpublished = {RFC 2420}, month = {September}, year = 1998 } @Misc{rfc2419, author = {K Sklower and G. Meyer}, title = {The {PPP} {DES} Encryption Protocol, Version 2}, howpublished = {{RFC} 2419}, month = {September}, year = 1998 } @Misc{rfc1968, author = {G. Meyer}, title = {The {PPP} Encryption Control Protocol}, howpublished = {{RFC} 1968}, month = {June}, year = 1996 } @Misc{rfc2284, author = {L. Blunk}, title = {{PPP} Extensible Authentication Protocol}, howpublished = {RFC 2284}, month = {March}, year = 1998 } @Misc{rfc2716, author = {B. Aboba and D. Simon}, title = {{PPP} {EAP} {TLS} Authentication Protocol}, howpublished = {{RFC} 2716}, month = {October}, year = 1999 } @MANUAL{rfc:2401, TITLE = "Security Architecture for the Internet Protocol", ORGANIZATION = "{IETF} Network Working Group {RFC} 2401", AUTHOR = "S. Kent and R. Atkinson", MONTH = "November", YEAR = "1998" } @MANUAL{rfc:2402, TITLE = "IP Authentication Header", ORGANIZATION = "IETF Network Working Group {RFC} 2402", AUTHOR = "S. Kent and R. Atkinson", MONTH = "November", YEAR = "1998" } @MANUAL{rfc:2406, TITLE = "IP Encapsulating Security Payload", ORGANIZATION = "IETF Network Working Group {RFC} 2406", AUTHOR = "S. Kent and R. Atkinson", MONTH = "November", YEAR = "1998" } @MANUAL{rfc:2407, TITLE = "The Internet IP Security Domain of Interpretation for ISAKMP", ORGANIZATION = "IETF Network Working Group {RFC} 2407", AUTHOR = "D. Piper", MONTH = "November", YEAR = "1998" } @MANUAL{rfc:2408, TITLE = "Internet Security Association and Key Management Protocol (ISAKMP)", ORGANIZATION = "IETF Network Working Group {RFC} 2408", AUTHOR = "D. Maughan and M. Schertler and M. Schneider and J. Turner", MONTH = "November", YEAR = "1998" } @MANUAL{rfc:2409, TITLE = "The Internet Key Exchange (IKE)", ORGANIZATION = "IETF Network Working Group {RFC} 2409", AUTHOR = "D. Harkins and D. Carrel", MONTH = "November", YEAR = "1998" } @techreport{Rabin81, title={How to exchange secrets by oblivious transfer}, author={Michael Rabin}, year={1981}, institution={Technical Report TR-81, Harvard Aiken Computation Laboratory}, note = "Available at \url{http://eprint.iacr.org/2005/187}" } @Article{RivestShamirAdleman78, author = "R. Rivest and A. Shamir and L. Adleman", title = "A Method for Obtaining Digital Signatures and Public Key Cryptosystems", journal = "Communications of the ACM", year = 1978, volume = 21, number = 2, pages = "120--126", month = feb } @InCollection{Roscoe94, author = {A. W. Roscoe}, title = {Model-Checking {CSP}}, booktitle = {A Classical Mind: Essays in Honour of C. A. R. Hoare}, publisher = {Prentice-Hall}, year = 1994, editor = {A. W. Roscoe} } @InProceedings{Roscoe95, author = {A. W. Roscoe}, title = {Modeling and Verifying Key-Exchange Protocols Using {CSP} and {FDR}}, booktitle = {Proceedings of the 8th {IEEE} Computer Security Foundations Workshop}, year = 1995, pages = {98--107} } @inproceedings{Roscoe1995csp, title={{CSP} and Determinism in Security Modelling}, author={Roscoe, A William}, booktitle={{IEEE} Security and Privacy}, pages={114--127}, year={1995}, organization={IEEE} } @InProceedings{Roscoe96, author = {A. W. Roscoe}, title = {Intensional Specifications of Security Protocols}, booktitle = {Proceedings of the 9th {IEEE} Computer Security Foundations Workshop}, year = 1996, pages = {28--38} } @Book{Roscoe97, author = {A. W. Roscoe}, title = {The Theory and Practice of Concurrency}, publisher = {Prentice-Hall}, year = 1997 } @InProceedings{RoscoeGoldsmith99, author = {A. W. Roscoe and M. H. Goldsmith}, title = {What is Intransitive Noninterference?}, booktitle = {12th {IEEE} Computer Security Foundations Workshop}, pages = {228--238}, year = 1999, month = {June}, publisher = {{IEEE} {CS} Press} } @TechReport{RubinHoneyman93, author = "A. D. Rubin and P. Honeyman", title = "Formal Methods for the Analysis of Authentication Protocols", institution = "CITI", year = 1993, number = "Technical report 93--7", month = nov } @InProceedings{RubinHoneyman94, author = "A. D. Rubin and P. Honeyman", title = "Nonmonotonic Crytpographic Protocols", pages = "100--115", booktitle = "Proceedings of the Computer Security Foundations Workshop VII", year = 1994, publisher = "IEEE CS Press" } @inproceedings{RusinowitchTuruani01, author = {Micha{\"e}l Rusinowitch and Mathieu Turuani}, title = {Protocol Insecurity with Finite Number of Sessions is {NP}-Complete}, booktitle = {Computer Security Foundations Workshop}, year = 2001, pages = {174-}, ee = {http://csdl.computer.org/comp/proceedings/csfw/2001/1146/00/11460174abs.htm}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{RusinowitchTuruani03, author = {Micha{\"e}l Rusinowitch and Mathieu Turuani}, title = {Protocol insecurity with a finite number of sessions, composed keys is NP-complete}, journal = {Theor. Comput. Sci.}, volume = {1-3}, number = {299}, year = {2003}, pages = {451-475}, ee = {http://dx.doi.org/10.1016/S0304-3975(02)00490-5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{RyanSchneider98, author = {Peter Y. A. Ryan and Steve Schneider}, title = {An Attack on {APM}'s Recursive Authentication Protocol---a Cautionary Tale}, journal = {Information Processing Letters}, year = 1998, volume = 65 } @article{RyanSchneider2001, author = {Peter Ryan and Steve Schneider}, title = {Process Algebra and Non-interference}, journal = {J. Comput. Secur.}, volume = {9}, number = {1-2}, month = jan, year = {2001}, pages = {75--103} } @Article{SabelfeldMyers03, author = {Andrei Sabelfeld and Andrew C. Myers}, title = {Language-based Information-Flow Security}, journal = {{IEEE} Journal on Selected Areas in Communication}, year = 2003, volume = 21, number = 1, pages = {5--19}, month = {January} } @TechReport{Satyanarayanan87, author = "N. Satyanarayanan", title = "Integrating Security in a Large Distributed System", institution = "CMU", year = 1987, number = "iCMU-CS-87-179", month = "nov" } @InProceedings{Schneider96, author = {Steve Schneider}, title = {Security Properties and {CSP}}, booktitle = {Proceedings, 1996 {IEEE} Symposium on Security and Privacy}, pages = {174--87}, year = 1996, month = {May}, publisher = {{IEEE} CS Press} } @InProceedings{Schneider97, author = {Steve Schneider}, title = {Verifying Authentication Protocols with {CSP}}, booktitle = {Proceedings of the 10th {IEEE} Computer Security Foundations Workshop}, year = 1997, publisher = {IEEE CS Press}, pages = {3--17} } @Article{Schneier93, author = "B. Schneier", title = "The IDEA Encryption Algorithm", journal = "Dr. Dobb's Journal", year = 1993, pages = "50--56", month = "December" } @Book{Schneier94, author = "Bruce Schneier", title = "Applied Cryptography", publisher = "Wiley", year = 1994 } @unpublished{SchneierShostack99, author = "Bruce Schneier and Adam Shostack", title = "Breaking Up Is Hard To Do: Modeling Security Threats for Smart Cards", note = "Counterpane Systems and Netect, Inc., available at http://www.counterpane.com/smart-card-threats.html", year = 1999 } @UNPUBLISHED{FergusonSchneier99, AUTHOR = "Niels Ferguson and Bruce Schneier", TITLE = "A Cryptographic Evaluation of IPsec", NOTE = "Counterpane Internet Security, Inc., available at http://www.counterpane.com/ipsec.html", year = 1999 } @article{Selinger01, author = {Peter Selinger}, title = {Models for an adversary-centric protocol logic}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {55}, number = {1}, year = {2001}, ee = {http://www.elsevier.com/gej-ng/31/29/23/83/27/show/Products/notes/index.htt\#007}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Misc{SELinux03, author = {{National Security Agency}}, title = {Security-Enhanced {Linux}}, howpublished = {At URL \url{http://www.nsa.gov/selinux/index.html}}, month = {April}, year = 2003 } @Misc{SetSpec97, key = {SET}, title = {{SET} Secure Electronic Transaction Specification}, month = {May}, year = 1997, note = {Available at {http://www.setco.org/download.html}} } @TechReport{SELTechRep, author = "P. Loscocco and S. Smalley", title = "Integrating Flexible Support for Security Policies into the Linux Operating System", institution = "NSA, NAI Labs", year = "2001", month = "April" } @Unpublished{sendmail01, author = "Franklin Haskell", title = "Confining Sendmail Using Security-Enhanced Linux", month = "October", year = 2001 } @InProceedings{Shamir00, author = "A. Shamir", title = "Protecting Smart Cards from Passive Power Analysis with Detached Power Supplies", booktitle = "CHES 2000, Springer-Verlag", year = 2000, pages = "71--77" } @TechReport{Shoup99, author = {Victor Shoup}, title = {On Formal Models for Secure Key Exchange}, institution = {IBM Research}, year = 1999, type = {Research Report}, number = {RZ 3120 (\#93166)}, month = Apr, day = 19, note = {A revised version 4, dated November 15, 1999, is available from \url{http://www.shoup.net/papers/}} } @InProceedings{Simmons85, author = {Gustavus J. Simmons}, title = {How to (Selectively) Broadcast a Secret}, booktitle = {1985 IEEE Symposium on Security and Privacy}, year = 1985, pages = {108--113} } @Article{Simmons88, author = "G.J. Simmons", title = "How to Insure that Data Aquired to Verify Treaty Compliance are Trustworthy", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, pages = "621--627", month = "May" } @Unpublished{SkoroAnderson02, author = "Sergei Skorobogatov and Ross Anderson", title = "Optical Fault Induction Attacks", year = 2002, note = "University of Cambridge, Computer Laboratory. Available at http://www.ftp.cl.cam.ac.uk/ftp/users/rja14/faultpap3.pdf" } @Article{SmidBranstad88, author = "Miles E. Smid and Dennis K. Branstad", title = "The Data Encryption Standard: Past and Future", journal = "Proceedings of the IEEE", year = 1988, volume = 76, number = 5, pages = "550--559", month = may } @InProceedings{Snekkenes91, author = "Einar Snekkenes", title = "Exploring the BAN Approach to Protocol Analysis", pages = "171--181", booktitle = "1991 IEEE Symposium on Research in Security and Privacy", year = 1991, publisher = "IEEE CS Press" } @InProceedings{Snekkenes92, author = "E. Snekkenes", title = "Roles in Cryptographic protocols", booktitle = "Proceedings of the 1992 IEEE Symposium on Security and Privacy", year = 1992, publisher = "IEEE CS Press" } @InProceedings{Song99, author = {Dawn Xiaodong Song}, title = {Athena: a New Efficient Automated Checker for Security Protocol Analysis}, booktitle = {Proceedings of the 12th {IEEE} Computer Security Foundations Workshop}, year = 1999, month = {June}, publisher = {{IEEE} CS Press} } @InProceedings{PerrigSong00, author = {Adrian Perrig and Dawn Xiaodong Song}, title = {Looking for Diamonds in the Desert: Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement Protocols}, booktitle = {Proceedings of the 13th {IEEE} Computer Security Foundations Workshop}, year = 2000, month = {July}, publisher = {{IEEE} CS Press} } @InProceedings{PerrigSong00a, author = {Adrian Perrig and Dawn Xiaodong Song}, title = {A First Step Toward the Automatic Generation of Security Protocols}, booktitle = {Network and Distributed System Security Symposium}, year = 2000, month = {February}, publisher = {Internet Society} } @InProceedings{SpiessensVanRoy05, author = {Fred Spiessens and Peter {Van Roy}}, title = {A Practical Formal Model for Safety Analysis in Capability-Based Systems}, booktitle = {Trust in Global Computing}, year = 2005, editor = {Rocco De Nicola and Davide Sangiorgi}, number = 3705, series = {LNCS}, publisher = {Springer} } @InProceedings{RamanujamSuresh03, author = {R. Ramanujam and S. P. Suresh}, title = {A Decidable Subclass of Unbounded Security Protocol}, booktitle = {WITS '03: Workshop on Issues in the Theory of Security}, pages = {11--20}, year = 2003, editor = {R. Gorrieri}, address = {Warsaw}, month = {April} } @incollection{ramanujam2003tagging, title={Tagging makes secrecy decidable with unbounded nonces as well}, author={Ramaswamy Ramanujam and S P Suresh}, booktitle={FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science}, pages={363--374}, year={2003}, publisher={Springer} } @Article{RamanujamSuresh05, author = {R. Ramanujam and S. P. Suresh}, title = {Decidability of Context-Explicit Security Protocols}, journal = {Journal of Computer Security}, year = 2005, volume = 13, number = 1, pages = {135--166}, note = {Preliminary version appeared in WITS '03, \emph{Workshop on Issues in the Theory of Security}, Warsaw, April 2003} } @Unpublished{Ramsdell12a, author = {John D. Ramsdell}, title = {Deducing Security Goals From Shape Analysis Sentences}, note = {\url{http://arxiv.org/abs/1204.0480}}, OPTkey = {}, month = apr, year = 2012, OPTannote = {} } @Misc{Ramsdell12, author = {John D. Ramsdell}, title = {Deducing Security Goals from Shape Analysis Sentences}, howpublished = {The MITRE Corporation}, month = apr, year = 2012, note = {\url{http://arxiv.org/abs/1204.0480}}} @Misc{RamsdellEtAl14, author = {John D. Ramsdell and Daniel J. Dougherty and Joshua D. Guttman and Paul D. Rowe}, title = {A Hybrid Analysis for Security Protocols with State}, howpublished = {The MITRE Corporation and Worcester Polytechnic Institute}, month = apr, year = 2014, note = {\url{http://arxiv.org/abs/1404.3899}}} @TechReport{SegallGuttman08, author = {Ariel Segall and Joshua Guttman}, title = {A Strand Space/Multiset Rewriting Model of {TPM} Commands}, institution = {The MITRE Corporation}, year = 2008, type = {MTR}, number = 080181, address = {Bedford, MA}, month = {July}} @InProceedings{SpencerSmalleyEtAl99, author = "R. Spencer and S. Smalley and P. Loscocco and M. Hibler and D. Anderson and J. Lepreau", title = "The Flask Security Architecture: System Support for Diverse Security Policies", booktitle = "Proceedings of the Eighth USENIX Security Symposium", year = 1999, month = "August", pages = "123--139" } @InProceedings{Stoller99, author = {Scott Stoller}, title = {A Reduction for Automated Verification of Authentication Protocols}, booktitle = {Workshop on Formal Methods and Security Protocols}, year = 1999, month = {July}, note = {Available at http://www.cs.indiana.edu/\~{ }stoller/} } @Unpublished{Stoller99a, author = {Scott Stoller}, title = {A Bound on Attacks on Authentication Protocols}, note = {Available at http://www.cs.indiana.edu/\~{ }stoller/}, month = {July}, year = 1999 } @InProceedings{StubblebineGligor92, author = "Stuart G. Stubblebine and Virgil D. Gligor", title = "On Message Integrity in Cryptographic Protocols", pages = "85-104", booktitle = "Proceedings of the 1992 IEEE Symposium on Research in Security and Privacy", year = 1992, publisher = "IEEE" } @InProceedings{Sutherland86, author = {David Sutherland}, title = {A Model of Information}, booktitle = {9th National Computer Security Conference}, year = 1986, organization = {National Institute of Standards and Technology} } @InProceedings{Syverson91, author = "Paul Syverson", title = "The Use of Logic in the Analysis of Cryptographic Protocols", booktitle = "Proceedings of the 1991 IEEE Symposium on Security and Privacy", publisher = "IEEE CS", year = 1991, editor = "Teresa F. Lunt and John McLean", pages = "156--170", month = may } @InProceedings{Syverson94a, author = "Paul Syverson", title = "A Taxonomy Of Replay Attacks", pages = "131--136", booktitle = "Proceedings of the 7th IEEE Computer Security Foundations Workshop", year = 1994, publisher = "IEEE CS Press" } @InProceedings{Syverson94b, author = "Paul Syverson", title = "On Key Distribution for Repeated Authentication", pages = "24--30", booktitle = "Operating Systems Review", year = 1994 } @Article{Syverson99, author = {Paul Syverson}, title = {Towards a Strand Semantics for Authentication Logic}, journal = {Electronic Notes in Theoretical Computer Science}, year = 1999, volume = 20 } @InProceedings{SyversonMeadows93, author = "Paul Syverson and Catherine Meadows", title = "A Logic language for Specifying Cryptographic Protocol Requirements", pages = "165--177", booktitle = "Proceedings of the 1993 IEEE Symposium on Research in Security and Privacy", year = 1993, publisher = "IEEE CS Press", month = May } @InCollection{Tarski28, author = "A. Tarski", title = "On some Fundamental Concepts of Metamathematics", booktitle = "Logic, Semantics, Meta-Mathematics", publisher = "Hackett Publishing Company", year = 1983, editor = "J. Corcoran", chapter = "III", pages = "30--37" } @InCollection{Tarski35, author = "A. Tarski", title = "On the Concept of Logical Consequence", booktitle = "Logic, Semantics, Meta-Mathematics", publisher = "Hackett Publishing Company", year = 1983, editor = "J. Corcoran", chapter = "XVI", pages = "409--420" } @InProceedings{TatebayashiEtAl90, author = {M. Tatebayashi and N. Matsuzaki and D. Newman}, title = {Key Distribution Protocol for Digital Mobile Communication Systems}, booktitle = {Advances in Cryptology: {\sc crypto} '89}, editor = {G. Brassard}, volume = 435, series = {Lecture Notes in Computer Science}, year = 1990, publisher = {Springer Verlag}, pages = {324--331} } @TechReport{ThayerHerzogGuttman97, author = {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman}, title = {Strand Spaces}, institution = {The {\sc Mitre} Corporation}, year = 1997, month = {November} } @InProceedings{ThayerHerzogGuttman98, author = {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman}, title = {Strand Spaces: Why is a Security Protocol Correct?}, booktitle = {1998 {IEEE} Symposium on Security and Privacy}, year = 1998, month = {May}, publisher = {{IEEE} CS Press} } @InProceedings{ThayerHerzogGuttman98a, author = {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman}, title = {Honest Ideals on Strand Spaces}, booktitle = {Proceedings of the 11th {IEEE} Computer Security Foundations Workshop}, year = 1998, month = {June}, publisher = {{IEEE} CS Press} } @Unpublished{ThayerHerzogGuttman98b, author = {F. Javier {\textsc{Thayer} F\'{a}brega} and Jonathan C. Herzog and Joshua D. Guttman}, title = {Strand Space Pictures}, note = {Presented at the {LICS Workshop on Formal Methods and Security Protocols}}, month = {June}, year = 1998 } @Article{ThayerHerzogGuttman99, author = {F. Javier Thayer and Jonathan C. Herzog and Joshua D. Guttman}, title = {Strand Spaces: Proving Security Protocols Correct}, journal = {Journal of Computer Security}, year = 1999, volume = 7, number = {2/3}, pages = {191--230} } @InProceedings{ThayerHerzogGuttman99a, author = {F. Javier Thayer and Jonathan C. Herzog and Joshua D. Guttman}, title = {Mixed Strand Spaces}, booktitle = {Proceedings of the 12th {IEEE} Computer Security Foundations Workshop}, year = 1999, month = {June}, publisher = {{IEEE} CS Press} } @Manual{TCGspec01, title = {Trusted Computing Group Main Specification}, key = {Trusted Computing Group}, organization = {Trusted Computing Group}, edition = {Version 1.1b}, month = sep, year = 2001, note = {URL \url{https://www.trustedcomputinggroup.org/downloads/tcg_spec_1_1b.zip}} } @Manual{TCGArch04, title = {TCG Specification Architecture Overview}, organization = {Trusted Computing Group}, address = {\url{https://www.trustedcomputinggroup.org/downloads/TCG_1_0_Architecture_Overview.pdf}}, edition = {Revision 1.2}, month = {April}, year = 2004 } @Manual{TCGMainDesign05, title = {{TPM} Main: Part {I} Design Principles}, organization = {Trusted Computing Group}, address = {\url{https://www.trustedcomputinggroup.org/downloads/specifications/mainP1DP_rev85.zip}}, edition = {Specification Version 1.2, Revision 85}, month = {February}, year = 2005 } @Misc{VixieEtAl97, author = {P. Vixie and S. Thompson and Y. Rekhter and J. Bound}, title = {Dynamic Updates in the Domain Name System}, howpublished = {RFC 2136}, month = {April}, year = 1997 } @Article{VolpanoEtAl96, author = {Cynthia Irvine and Dennis Volpano and Geoffrey Smith}, title = {A Sound Type System for Secure Flow Analysis}, journal = {Journal of Computer Security}, year = 1996, volume = 4, number = 3, pages = {1--21} } @Article{VoydockKent83, author = "Victor L. Voydock and Stephen T. Kent", title = "Security Mechanisms in High-Level Network Protocols", journal = "Computing Surveys", year = 1983, volume = 15, number = 2, pages = "135--171", month = jun } @InProceedings{WagnerSchneier96, author = {D. Wagner and B. Schneier}, title = {Analysis of the {SSL} 3.0 Protocol}, booktitle = {Proceedings, Second USENIX Workshop on Electronic Commerce}, pages = {29--40}, year = 1996, note = {Available at http://www.counterpane.com/ssl.html} } @InProceedings{WallachFelten98, author = {Daniel S. Wallach and Edward W. Felten}, title = {Understanding Java Stack Inspection}, booktitle = {{IEEE} Symposium on Security and Privacy}, pages = {52--63}, year = 1998 } @article{Wang2006, title={Generic non-repudiation protocols supporting transparent off-line {TTP}}, author={Guilin Wang}, journal={Journal of Computer Security}, volume={14}, number={5}, pages={441--467}, year={2006}, publisher={IOS Press} } @Proceedings{Wiener93, title = "Efficient DES Key Search ", year = 1993, series = "Crypto 93", month = aug } @Article{Willet82, author = "Michael Willet", title = "Cryptography Old and New", journal = "Computers and Security", volume = "Vol 1", pages = "177--186", year = 1982 } @Article{WooLam92, author = "T. Y. C. Woo and S. S. Lam", title = "Authentication for Distributed Systems", journal = "Computer", year = 1992, volume = 25, number = 1, pages = "39--52", month = jan } @Article{WooLam92a, author = {Thomas Y. C. Woo and Simon S. Lam}, title = {Authentication for Distributed Systems}, journal = {Computer}, year = 1992, volume = 25, number = 1, pages = {39--52}, month = {January} } @InProceedings{WooLam93, author = {Thomas Y. C. Woo and Simon S. Lam}, title = {Verifying authentication protocols: Methodology and example}, booktitle = {Proc. Int. Conference on Network Protocols}, year = 1993, month = {October} } @Article{WooLam94, author = "Thomas Y. C. Woo and Simon S. Lam", title = "A Lesson on Authentication Protocol Design", journal = "Operating Systems Review", year = 1994, pages = "24--37" } @InProceedings{Wray91, author = {John C. Wray}, title = {An Analysis of Covert Timing Channels}, booktitle = {Proceedings, 1991 {IEEE} Symposium on Research in Security and Privacy}, pages = {2--7}, year = 1991, month = {May}, organization = {{IEEE} CS} } @InProceedings{YamaguchiOkayamaMiyahara90, author = "S. Yamaguchi and K. Okayama and H. Miyahara", title = "Design and Implementation of an Authentication System in {WIDE Internet} Environment", booktitle = "Proceedings of the 10th Regional Conference on Computers and Communication Systems", year = 1990 } @InProceedings{WoolEtAl00, author = {Alain Mayer and Avishai Wool and Elisha Ziskind}, title = {Fang: A Firewall Analysis Engine}, booktitle = {Proceedings, IEEE Symposium on Security and Privacy}, year = 2000 } @Unpublished{YasinacWulf93, author = "Alec F Yasinsac and William A Wulf", title = "A Formal Semantics for Evaluating Cryptographic Protocols", note = "The paper has been superceeded by a later version published in the IEEE Symposium on Security and Privacy 1994.", year = 1993 } @Misc{SSHArch, author = {T. Ylonen and T. Kivinen and M. Saarinen}, title = {{SSH} Prototcol Architecture}, howpublished = {Internet draft}, month = {November}, year = {1997}, note = {Also named draft-ietf-secsh-architecture-01.txt} } @Misc{SSHConn, author = {T. Ylonen and T. Kivinen and M. Saarinen}, title = {{SSH} Connection Prototcol}, howpublished = {Internet draft}, month = {November}, year = {1997}, note = {Also named draft-ietf-secsh-connect-03.txt} } @Misc{SSHTrans, author = {T. Ylonen and T. Kivinen and M. Saarinen}, title = {{SSH} Transport Layer Prototcol}, howpublished = {Internet draft}, month = {November}, year = {1997}, note = {Also named draft-ietf-secsh-transport-01.txt} } @Misc{SSHAuth, author = {T. Ylonen and T. Kivinen and M. Saarinen}, title = {{SSH} Authentication Prototcol}, howpublished = {Internet draft}, month = {November}, year = {1997}, note = {Also named draft-ietf-secsh-userauth-01.txt} } @Book{ReedSimon80, author = {M. Reed and B. Simon}, title = {Functional Analysis}, publisher = {Academic Press}, year = {1980}, address = {Orlando} } @Book{billingsley1, author = "Patrick Billingsley Jr.", title = "Convergence of Probability Measures", publisher = "John Wiley and Sons", year = "1968", OPTeditor = "", OPTvolume = "", OPTseries = "", address = "New York", OPTedition = "", OPTmonth = "", OPTnote = "" } @Book{DaemenRijmen, author ={J. Daemen and V. Rijmen}, title = {The Design of Rijndael}, publisher = {Springer-Verlag}, year = {2002}, address = {Berlin} } @InProceedings{LincolnEtAl99, author = {Lincoln,P.D. and Mitchell, J.C. and Mitchell, M. and Scedrov, A.}, title = {Probabilistic polynomial-time equivalence and security protocols}, booktitle = {{FM}'99 World Congress On Formal Methods in the Development of Computing Systems}, year = 1999, month = {September} } @InProceedings{LincolnEtAl98, author = {Lincoln, P.D. and Mitchell, J.C. and Mitchell, M. and Scedrov, A.}, title = {A Probabilistic Poly-time Framework for Protocol Analysis}, booktitle = {{ACM} Computer and Communication Security ({CCS}-5)}, pages = {112-121}, year = 1998 } @InProceedings{MitchelEtAl98, author = {J. C. Mitchell and M. Mitchell and A. Scedrov}, title = {A linguistic characterization of bounded oracle computation and probabilistic polynomial time}, booktitle = {{IEEE} Foundations of Computer Science}, pages = {725-733}, year = 1998 } @InProceedings{PereiraO:2001:CSFW, author = "Olivier Pereira and Jean-Jacques Quisquater", title = "A Security Analysis of the Cliques Protocols Suites", booktitle = "14th IEEE Computer Security Foundations Workshop --- CSFW'01", year = 2001, pages = "73--81", address = "Cape Breton, Canada", month = "11--13 June", publisher = "IEEE CS Press" } @inproceedings{pereira2004generic, title={Generic insecurity of cliques-type authenticated group key agreement protocols}, author={Olivier Pereira and J-J Quisquater}, booktitle={Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE}, pages={16--29}, year={2004}, organization={IEEE} } @article{pereira2006impossibility, title={On the impossibility of building secure cliques-type authenticated group key agreement protocols}, author={Olivier Pereira and Jean-Jacques Quisquater}, journal={Journal of Computer Security}, volume={14}, number={2}, pages={197--246}, year={2006}, publisher={IOS Press} } @InProceedings{PereiraO:2001:CSFW, author = "Olivier Pereira and Jean-Jacques Quisquater", title = "A Security Analysis of the Cliques Protocols Suites", booktitle = "14th IEEE Computer Security Foundations Workshop --- CSFW'01", year = 2001, pages = "73--81", address = "Cape Breton, Canada", month = "11--13 June", publisher = "IEEE CS Press" } @Unpublished{BackesEtAl2003, author = {Michael Backes and Birgit Pfitzmann and Michael Waidner}, title = {A Universally Composable Cryptographic Library}, note = {Available at \texttt{http://eprint.iacr.org/2003/015/}}, month = {January}, year = 2003 } @inproceedings{DBLP:conf/esorics/CortierWZ07, author = {V{\'e}ronique Cortier and Bogdan Warinschi and Eugen Zalinescu}, title = {Synthesizing Secure Protocols}, booktitle = {{ESORICS}: European Symposium On Research In Computer Security}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4734}, year = {2007}, pages = {406-421}, ee = {http://dx.doi.org/10.1007/978-3-540-74835-9_27}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{LiEtAl2012, author = {Ming Li and Sucheng Yu and Joshua D. Guttman and Wenjing Lou and Kui Ren}, title = {Secure ad-hoc trust initialization and key management in wireless body area networks}, journal = {ACM Transactions on Sensor Networks (TOSN)}, volume = 9, number = 2, pages = 18, year = 2013} @inproceedings{DenielouYoshida2011, author = {Pierre-Malo Deni{\'e}lou and Nobuko Yoshida}, title = {Dynamic multirole session types}, booktitle = {POPL}, year = 2011, pages = {435-446}, ee = {http://doi.acm.org/10.1145/1926385.1926435}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{CG09b, author = {Marco Carbone and Joshua Guttman}, title = {Choreographies with Secure Boxes and Compromised Principals}, booktitle = {{Proc. of Interaction and Concurrency Experience (ICE'09)}}, publisher = {EPTCS}, volume = {12}, pages = {1--15}, year = {2009}, url = {http://arxiv.org/abs/0911.5444} } @article{KL11, author = {Allaa Kamil and Gavin Lowe}, title = {Analysing {TLS} in the strand spaces model}, journal = {Journal of Computer Security}, volume = {19}, number = {5}, year = {2011}, pages = {975-1025}, ee = {http://dx.doi.org/10.3233/JCS-2011-0429}, } @Misc{onlineappendix, author = {Marco Carbone and Joshua Guttman}, title = {Online Appendix}, howpublished = {\url{http://www.itu.dk/people/maca/separation}} } @InProceedings{ADK08, author = "Myrto Arapinis and Stephanie Delaune and Steve Kremer", title = "From one Session to many: Dynamic Tags for Security Protocols", booktitle = "Proc. of LPAR'08", year = "2008" } @inproceedings{DKR08, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, booktitle = {{P}roceedings of the 21st {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'08)}, DOI = {10.1109/CSF.2008.6}, month = jun, pages = {239-251}, publisher = {{IEEE} Computer Society Press}, title = {Composition of Password-based Protocols}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csf08.pdf}, year = {2008}, } @techreport{KL08, title = "Analysing TLS in the Strand Spaces Model", author = "Allaa Kamil and Gavin Lowe", year = "2008", } @InProceedings{HYC08, author = "K. Honda and N. Yoshida and M. Carbone", title = "Multiparty Asynchronous Session Types", booktitle = "Proc. of POPL", year = "2008", pages = {273--284}, volume = {43(1)}, publisher = {ACM}, } @InProceedings{sessiontypes, author = {Kohei Honda and Vasco Vasconcelos and Makoto Kubo}, title = {Language primitives and type disciplines for structured communication-based programming}, booktitle = "ESOP'98", series = "LNCS", volume = "1381", pages = {22--138}, year = {1998}, publisher = {Springer-Verlag}, } @InProceedings{DoughertyGuttman12, author = {Daniel J. Dougherty and Joshua D. Guttman}, title = {An Algebra for Symbolic {Diffie-Hellman} Protocol Analysis}, booktitle = {Trustworthy Global Computing}, year = 2012, volume = {8191}, pages = {164--181}, series = {LNCS}} @Article{Guttman12a, author = {Joshua D. Guttman}, title = {Establishing and Preserving Protocol Security Goals}, journal = {Journal of Computer Security}, year = 2014, volume = 22, number = 2, pages = {203--267}} @Article{Guttman14, author = {Joshua D. Guttman}, title = {Establishing and Preserving Protocol Security Goals}, journal = {Journal of Computer Security}, year = 2014, volume = 22, number = 2, pages = {201--267}} @InProceedings{Fay79, author = {M. Fay}, title = {First-order Unification in an Equational Theory}, booktitle = {Proc. 4th Workshop on Automated Deduction}, year = 1979} @Book{BaaderNipkow98, author = {Franz Baader and Tobias Nipkow}, title = {Term Rewriting and All That}, publisher = {Cambridge University Press}, year = 1998} @Book{Paulson91, author = {Laurence C. Paulson}, title = {ML for the Working Programmer}, publisher = {Cambridge University Press}, year = 1991} @Book{RobinsonVoronkov01, author = {Alan Robinson and Andrei Voronkov}, title = {Handbook of Automated Reasoning}, vol = 1, publisher = {The {MIT} Press}, year = 2001} @inproceedings{Millen99, author = "Jonathan K. Millen", title = "A Necessarily Parallel Attack", booktitle = "Workshop on Formal Methods and Security Protocols, Part of the Federated Logic Conference", address = "Trento, Italy", editor = "Nevin Heintze and Edmund Clarke", year = "1999", url = "citeseer.ist.psu.edu/millen99necessarily.html" } @inproceedings{PavlovicMeadows06, author = "Dusko Pavlovic and Catherine Meadows", title = "Deriving Secrecy in Key Establishment Protocols", booktitle = "European Symposium on Research in Computer Security", month = sep, year = 2006, url = "http://www.kestrel.edu/home/people/pavlovic/security.html" } @article{GansnerNorth00, author = "Emden R. Gansner and Stephen C. North", title = "An open graph visualization system and its applications to software engineering", journal = "Soft\-ware --- Prac\-tice and Experience", volume = "30", number = "11", pages = "1203--1233", year = "2000", url = "citeseer.ist.psu.edu/gansner99open.html" } @Unpublished{Dijkstra82, author = {Edsger W. Dijkstra}, title = {Why numbering should start at zero}, note = {\url{http://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD831.html}}, month = aug, year = 1982} @TechReport{cpsatheory11, title = {Completeness of {CPSA}}, author = {Moses D.~Liskov and Paul D.~Rowe and F.~Javier Thayer}, institution = {The MITRE Corporation}, year = 2011, month = mar, number = {MTR110479}, note = {\url{http://www.mitre.org/publications/technical-papers/completeness-of-cpsa}} } @TechReport{Ramsdell13, title = {Proving Security Goals With Shape Analysis Sentences}, author = {John D.~Ramsdell}, institution = {The MITRE Corporation}, year = 2013, month = sep, number = {MTR130488}, note = {\url{http://arxiv.org/abs/1403.3563}}, } @inproceedings{cade92-pvs, AUTHOR = {{S.} Owre and {J.} {M.} Rushby and and {N.} Shankar}, TITLE = {{PVS:} {A} Prototype Verification System}, BOOKTITLE = {11th International Conference on Automated Deduction (CADE)}, YEAR = {1992}, EDITOR = {Deepak Kapur}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {607}, PAGES = {748--752}, ADDRESS = {Saratoga, {NY}}, MONTH = jun, PUBLISHER = {Springer-Verlag}, URL = {http://pvs.csl.sri.com/papers/cade92-pvs/}, note = {\url{http://pvs.csl.sri.com}} } @unpublished{algimpl11, author = {Moses Liskov and John D. Ramsdell}, title = {Implementing Strand Space Algebras}, note = {\url{http://www.ccs.neu.edu/home/ramsdell/papers/algimpl.pdf}}, year = 2011 } @incollection{ComonLundhMillen10, author= {H. Comon-Lundh and S. Delaune and J. Millen}, title = {Constraint solving techniques and enriching the model with equational theories}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, editor = {Veronique Cortier and Steve Kremer}, series = {Cryptology and Information Security Series}, volume = 5, year = 2011, isbn = {978-1-60750-713-0}, publisher = {{ISO} Press} } @TechReport{RamsdellEtAl09, author = {John D. Ramsdell and Joshua D. Guttman and Jonathan K. Millen and Brian O'Hanlon}, title = {An Analysis of the {CAVES} Attestation Protocol using {CPSA}}, note = {\url{http://arxiv.org/abs/1207.0418}}, institution = {The {MITRE} Corporation}, month = dec, year = 2009, type = {{MITRE} Technical Report}, number = {{MTR090213}} } @inproceedings{DBLP:conf/csfw/SchmidtMCB12, author = {Benedikt Schmidt and Simon Meier and Cas J. F. Cremers and David A. Basin}, title = {Automated Analysis of {Diffie-Hellman} Protocols and Advanced Security Properties}, booktitle = {{IEEE} Symposium on Computer Security Foundations}, year = {2012}, pages = {78-94}, ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2012.25}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{chevalier2008complexity, title={Complexity results for security protocols with {Diffie-Hellman} exponentiation and commuting public key encryption}, author={Yannick Chevalier and Ralf K{\"u}sters and Micha{\"e}l Rusinowitch and Mathieu Turuani}, journal={ACM Transactions on Computational Logic (TOCL)}, volume={9}, number={4}, pages={24}, year={2008}, publisher={ACM} } @incollection{gurgens2007security, title={Security evaluation of scenarios based on the {TCG's TPM} specification}, author={Sigrid G{\"u}rgens and Carsten Rudolph and Dirk Scheuermann and Marion Atts and Rainer Plaga}, booktitle={Computer Security--ESORICS 2007}, pages={438--453}, year={2007}, publisher={Springer} } @inproceedings{datta2009logic, title={A logic of secure systems and its application to trusted computing}, author={Anupam Datta and Jason Franklin and Deepak Garg and Dilsun Kaynar}, booktitle={Security and Privacy, 2009 30th IEEE Symposium on}, pages={221--236}, year={2009}, organization={IEEE} } @inproceedings{youn2007robbing, title={Robbing the bank with a theorem prover}, author={Paul Youn and Ben Adida and Mike Bond and Jolyon Clulow and Jonathan Herzog and Amerson Lin and Ronald Rivest and Ross Anderson}, booktitle={Security Protocols Workshop}, note={Available at \url{http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-644.pdf}}, year=2007 } @incollection{cortier2007automatic, title={Automatic analysis of the security of XOR-based key management schemes}, author={V{\'e}ronique Cortier and Gavin Keighren and Graham Steel}, booktitle={Tools and Algorithms for the Construction and Analysis of Systems}, pages={538--552}, year={2007}, publisher={Springer} } @incollection{cortier2009generic, title={A generic security API for symmetric key management on cryptographic devices}, author={V{\'e}ronique Cortier and Graham Steel}, booktitle={Computer Security--ESORICS 2009}, pages={605--620}, year={2009}, publisher={Springer} } @incollection{froschle2011reasoning, title={Reasoning with past to prove {PKCS\# 11} keys secure}, author={Sibylle Fr{\"o}schle and Nils Sommer}, booktitle={Formal Aspects of Security and Trust}, pages={96--110}, year={2011}, publisher={Springer} } @article{modersheim2010abstraction, title={Abstraction by set-membership: verifying security protocols and web services with databases}, author={Sebastian M{\"o}dersheim}, journal={ACM Conference on Computer and Communications Security}, pages={351--360}, year={2010} } @inproceedings{arapinis2011statverif, title={Statverif: Verification of stateful processes}, author={Myrto Arapinis and Eike Ritter and Mark Dermot Ryan}, booktitle={Computer Security Foundations Symposium (CSF)}, pages={33--47}, year={2011}, organization={IEEE} } @incollection{delaune2011formal, title={A formal analysis of authentication in the {TPM}}, author={Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D and Steel, Graham}, booktitle={Formal Aspects of Security and Trust}, pages={111--125}, year={2011}, publisher={Springer} } @article{herzog2006applying, title={Applying protocol analysis to security device interfaces}, author={Jonathan Herzog}, journal={IEEE Security \& Privacy}, volume={4}, number={4}, pages={84--87}, year={2006}, publisher={IEEE} } @incollection{sampaio2002refinement, title={Refinement in {Circus}}, author={Augusto Sampaio and Jim Woodcock and Ana Cavalcanti}, booktitle={FME 2002: Formal Methods}, pages={451--470}, year={2002}, publisher={Springer} } @incollection{butler2005combining, title={Combining {CSP} and {B} for specification and property verification}, author={Michael Butler and Michael Leuschel}, booktitle={FM 2005: Formal Methods}, pages={221--236}, year={2005}, publisher={Springer} } @inproceedings{Clulow03, author = {Jolyon Clulow}, title = {On the Security of {PKCS}\#11}, booktitle = {Cryptographic Hardware and Embedded Systems - {CHES} 2003}, year = {2003}, pages = {411-425}, ee = {http://dx.doi.org/10.1007/978-3-540-45238-6_32}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2779}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{meier2013efficient, title={Efficient construction of machine-checked symbolic protocol security proofs}, author={Simon Meier and Cas Cremers and David Basin}, journal={Journal of Computer Security}, volume={21}, number={1}, pages={41--87}, year={2013}, publisher={IOS Press} } @book{cremers2012operational, title={Operational semantics and verification of security protocols}, author={Cas Cremers and Sjouke Mauw}, year={2012}, publisher={Springer} } @article{jacobs2009semantics, title={Semantics and logic for security protocols}, author={Bart Jacobs and Ichiro Hasuo}, journal={Journal of Computer Security}, volume={17}, number={6}, pages={909--944}, year={2009}, publisher={IOS Press} } @techreport{LiskovThayer13, author = {Moses D. Liskov and F. Javier Thayer}, title = {Formal Modeling of {Diffie-Hellman} Derivability for Exploratory Automated Analysis}, institution = {{MITRE} }, year = {2013}, month = {June}, note = {TR 13-0411} } @article{Comon-LundhCZ10, author = {Hubert Comon-Lundh and V{\'e}ronique Cortier and Eugen Zalinescu}, title = {Deciding security properties for cryptographic protocols. {A}pplication to key cycles}, journal = {ACM Trans. Comput. Log.}, volume = {11}, number = {2}, year = {2010}, ee = {http://doi.acm.org/10.1145/1656242.1656244}, bibsource = {DBLP, http://dblp.uni-trier.de} } @book{BoydMathuria03, title={Protocols for authentication and key establishment}, author={Boyd, Colin and Mathuria, Anish}, year={2003}, publisher={Springer} } @Article{MTI86, author = {T. Matsumoto and Y. Takashima and H. Imai}, title = {On Seeking Smart Public-key Distribution Systems}, journal = {Transactions of the IECE of Japan}, year = 1986, volume = {E69}, pages = {99--106}} @article{clarkson2010hyperproperties, title={Hyperproperties}, author={Michael R. Clarkson and Fred B. Schneider}, journal={Journal of Computer Security}, volume={18}, number={6}, pages={1157--1210}, year={2010}, publisher={IOS Press} } @inproceedings{sprenger2010developing, title={Developing security protocols by refinement}, author={Christoph Sprenger and David Basin}, booktitle={{ACM CCS}}, pages={361--374}, year={2010} } @inproceedings{sprenger2012refining, title={Refining key establishment}, author={Christoph Sprenger and David Basin}, booktitle={{IEEE CSF}}, pages={230--246}, year={2012} } @incollection{maurer1994calculus, title={A calculus for secure channel establishment in open networks}, author={{\"U}li Maurer and Pierre Schmid}, booktitle={{ESORICS} 94}, pages={173--192}, year={1994}, publisher={Springer} } @incollection{Cremers11keyexchange, title={Key exchange in {IPsec} revisited: Formal analysis of {IKEv1} and {IKEv2}}, author={Cremers, Cas}, year={2011}, publisher={Springer}, booktitle={Computer Security--ESORICS 2011}, } @Misc{cdgk2014, key = {ckgk2014}, author = {V{\'e}ronique Cortier and Daniel J. Dougherty and Joshua D. Guttman and Steve Kremer}, title = {The Real-or-Random Property for Lightweight {Diffie-Hellman} Protocols}, howpublished = {Meetings}, month = {January}, year = 2014} @Misc{whatever, key = {whatever}, author = {Someone somewhere}, title = {Good citation for undecidability of unification in rings}} @article{MillenShmatikov05, author = {Jonathan K. Millen and Vitaly Shmatikov}, title = {Symbolic protocol analysis with an Abelian group operator or Diffie-Hellman exponentiation}, journal = {Journal of Computer Security}, volume = {13}, number = {3}, year = {2005}, pages = {515-564}, ee = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0926-227X{\&}volume=13{\&}issue=3{\&}spage=515}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{cortier2006survey, title={A survey of algebraic properties used in cryptographic protocols}, author={V{\'e}ronique Cortier and St{\'e}phanie Delaune and Pascal Lafourcade}, journal={Journal of Computer Security}, volume={14}, number={1}, pages={1--43}, year={2006}, publisher={IOS Press} } @article{kremer2010computationally, title={Computationally sound analysis of protocols using bilinear pairings}, author={Steve Kremer and Laurent Mazar{\'e}}, journal={Journal of Computer Security}, volume={18}, number={6}, pages={999--1033}, year={2010}, publisher={IOS Press} } @InProceedings{DoughertyGuttman2014, author = {Daniel J. Dougherty and Joshua D. Guttman}, title = {Decidability for Lightweight {Diffie-Hellman} Protocols}, booktitle = {{IEEE} Symposium on Computer Security Foundations}, year = 2014} @article{jacobs2009semantics, title={Semantics and logic for security protocols}, author={Bart Jacobs and Ichiro Hasuo}, journal={Journal of Computer Security}, volume={17}, number={6}, pages={909--944}, year={2009}, publisher={IOS Press} } @article{meier2013efficient, title={Efficient construction of machine-checked symbolic protocol security proofs}, author={Simon Meier and Cas Cremers and David Basin}, journal={Journal of Computer Security}, volume={21}, number={1}, pages={41--87}, year={2013}, publisher={IOS Press} } @InProceedings{Adida2008, author = {Ben Adida}, title = {Helios: Web-based Open-Audit Voting}, booktitle = {Usenix Security Symposium}, year = 2008, organization = {Usenix Association}} @article{gottlob2008efficient, title={Efficient core computation in data exchange}, author={Gottlob, Georg and Nash, Alan}, journal={{JACM}}, volume={55}, number={2}, pages={9}, year={2008}, publisher={ACM} } @inproceedings{mccullough1987specifications, title={Specifications for multi-level security and a hook-up property}, author={Daryl McCullough}, booktitle={{IEEE} Symposium on Security and Privacy}, pages={161--161}, year={1987} } @inproceedings{mccullough1988noninterference, title={Noninterference and the composability of security properties}, author={Daryl McCullough}, booktitle={{IEEE} Symposium on Security and Privacy}, pages={177--186}, year={1988} } @article{zdancewic2002secure, title={Secure program partitioning}, author={Steve Zdancewic and Lantian Zheng and Nathaniel Nystrom and Andrew C Myers}, journal={ACM Transactions on Computer Systems (TOCS)}, volume={20}, number={3}, pages={283--328}, year={2002}, publisher={ACM} } @inproceedings{LiZdancewic05, author = {Peng Li and Steve Zdancewic}, title = {Downgrading policies and relaxed noninterference}, booktitle = {Principles of Programming Languages {POPL}}, pages = {158--170}, year = {2005}, timestamp = {Tue, 22 May 2012 15:24:56 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/popl/LiZ05}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{chong2007secure, title={Secure web applications via automatic partitioning}, author={Stephen Chong and Jed Liu and Andrew C Myers and Xin Qi and Krishnaprasad Vikram and Lantian Zheng and Xin Zheng}, booktitle={{ACM SIGOPS} Operating Systems Review}, volume={41}, pages={31--44}, year={2007}, organization={ACM} } @inproceedings{bohannon2009reactive, title={Reactive noninterference}, author={Bohannon, Aaron and Pierce, Benjamin C and Sj{\"o}berg, Vilhelm and Weirich, Stephanie and Zdancewic, Steve}, booktitle={{ACM} conference on Computer and Communications Security}, pages={79--90}, year={2009}, organization={ACM} } @article{sabelfeld2009declassification, title={Declassification: Dimensions and principles}, author={Andrei Sabelfeld and David Sands}, journal={Journal of Computer Security}, volume={17}, number={5}, pages={517--548}, year={2009} } @inproceedings{chong2009deriving, title={Deriving epistemic conclusions from agent architecture}, author={Stephen Chong and Ron {van der Meyden}}, booktitle={Theoretical Aspects of Rationality and Knowledge}, pages={61--70}, year={2009}, organization={ACM} } @InProceedings{RafnssonSabelfeld14, author = {Willard Rafnsson and Andrei Sabelfeld}, title = {Compositional Information-Flow Security for Interactive Systems}, booktitle = {{IEEE} Symp.~{CSF}}, year = 2014, pages = {277--292}, month = {July}, } @article{ryan2009pret, title={Pr{\^e}t {\`a} voter: a voter-verifiable voting system}, author={Peter YA Ryan and David Bismark and James Heather and Steve Schneider and Zhe Xia}, journal={Information Forensics and Security, IEEE Transactions on}, volume={4}, number={4}, pages={662--673}, year={2009}, publisher={IEEE} } @article{jacob1992basic, title={Basic theorems about security}, author={Jeremy Jacob}, journal={Journal of Computer Security}, volume={1}, number={3}, pages={385--411}, year={1992}, publisher={IOS Press} } @inproceedings{morgan2006shadow, title={The shadow knows: Refinement of ignorance in sequential programs}, author={Carroll Morgan}, booktitle={Mathematics of program construction}, pages={359--378}, year={2006}, organization={Springer} } @Article{ArapinisEtAl14, author = {Myrto Arapinis and St{\'e}phanie Delaune and Steve Kremer}, title = {Dynamic Tags for Security Protocols}, journal = {Logical Methods in Computer Science}, year = {2014}, OPTkey = {}, OPTvolume = {10}, OPTnumber = {2:11}, OPTpages = {1--50} } @incollection{carbone2013sessions, title={Sessions and separability in security protocols}, author={Marco Carbone and Joshua D Guttman}, booktitle={Principles of Security and Trust}, pages={267--286}, year={2013}, publisher={Springer} } @inproceedings{adao2014mignis, title={Mignis: A semantic based tool for firewall configuration}, author={P Adao and Claudio Bozzato and Gian-Luca Dei Rossi, R Focardi and F Luccio}, booktitle={{IEEE CSF}}, year=2014 } @article{van2012architectural, title={Architectural refinement and notions of intransitive noninterference}, author={Ron {van der Meyden}}, journal={Formal Aspects of Computing}, volume={24}, number={4-6}, pages={769--792}, year={2012}, publisher={Springer} } @book{rushby1992noninterference, title={Noninterference, transitivity, and channel-control security policies}, author={John Rushby}, year={1992}, publisher={SRI International, Computer Science Laboratory} } @incollection{van2007indeed, title={What, indeed, is intransitive noninterference?}, author={Ron {van der Meyden}}, booktitle={Computer Security--ESORICS 2007}, pages={235--250}, year={2007}, publisher={Springer} } @TechReport{ChongvanderMeyden14, author = {Stephen Chong and Ron {van der Meyden}}, title = {Using Architecture to Reason about Information Security}, institution = {Arxiv}, year = 2014, number = {arXiv:1409.0309}, month = {Sept.}, note = {\url{http://arxiv.org/abs/1409.0309v1}}} @incollection{sabelfeld2004model, title={A model for delimited information release}, author={Andrei Sabelfeld and Andrew C Myers}, booktitle={Software Security-Theories and Systems}, pages={174--191}, year={2004}, publisher={Springer} } @article{delaune2009verifying, title={Verifying privacy-type properties of electronic voting protocols}, author={St{\'e}phanie Delaune and Steve Kremer and Mark Ryan}, journal={Journal of Computer Security}, volume={17}, number={4}, pages={435--487}, year={2009}, publisher={IOS Press} } @inproceedings{wittbold1990information, title={Information flow in nondeterministic systems}, author={J Todd Wittbold and Dale M Johnson}, booktitle={{IEEE} Symp. Security and Privacy}, pages={144--144}, year={1990} } @Article{HaighYoung1987, author = {J Thomas Haigh and William D Young}, title = {Extending the non-interference version of MLS for SAT}, journal = {{IEEE} Transactions on Software Engineering}, year = 1987, volume = 13, number = 2} @inproceedings{askarov2007gradual, title={Gradual release: Unifying declassification, encryption and key release policies}, author={Aslan Askarov and Andrei Sabelfeld}, booktitle={{IEEE} Symp. Security and Privacy}, pages={207--221}, year={2007}, organization={IEEE} } @inproceedings{mantel2011assumptions, title={Assumptions and guarantees for compositional noninterference}, author={Heiko Mantel and David Sands and Henning Sudbrock}, booktitle={{IEEE} Computer Security Foundations Symposium}, pages={218--232}, year={2011} } @incollection{roscoe1994non, title={Non-interference through determinism}, author={A.W. Roscoe and J.C.P. Woodcock and L. Wulf}, booktitle={Computer Security---ESORICS 94}, pages={31--53}, year={1994}, publisher={Springer} } @inproceedings{mclean1994general, title={A general theory of composition for trace sets closed under selective interleaving functions}, author={John McLean}, booktitle={{IEEE} Symp.~Security and Privacy}, pages={79--93}, year={1994} } @article{McLean1996, author = {McLean, John}, title = {A General Theory of Composition for a Class of ``Possibilistic'' Properties}, journal = {IEEE Trans. Softw. Eng.}, issue_date = {January 1996}, volume = {22}, number = {1}, month = jan, year = {1996}, pages = {53--67} } @Misc{GuttmanRowe14:cut, author = {Joshua D. Guttman and Paul D. Rowe}, title = {A Cut Principle for Information Flow}, howpublished = {Arxiv}, month = {October}, year = 2014, note = {\url{http://arxiv.org/abs/1410.4617}}} @InProceedings{GuttmanRowe15, author = {Joshua D. Guttman and Paul D. Rowe}, title = {A Cut Principle for Information Flow}, booktitle = {{IEEE} Computer Security Foundations}, year = 2015, month = {July}, publisher = {{IEEE} Computer Society Press}} @book{cormen2003introduction, title={Introduction to Algorithms}, author={Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein}, publisher={MIT Press}, edition={second}, address = {Cambridge, MA}, year=2003 } @article{bossi2004verifying, title={Verifying persistent security properties}, author={Annalisa Bossi and Riccardo Focardi and Carla Piazza and Sabina Rossi}, journal={Computer Languages, Systems \& Structures}, volume={30}, number={3}, pages={231--258}, year={2004} } @inproceedings{rossi2009information, title={Information flow security for service compositions.}, author={Sabina Rossi and Damiano Macedonio}, booktitle={ICUMT}, pages={1--8}, year={2009} } @incollection{focardi2001classification, title={Classification of security properties}, author={Riccardo Focardi and Roberto Gorrieri}, booktitle={Foundations of Security Analysis and Design}, pages={331--396}, year={2001}, publisher={Springer} } @inproceedings{mantel2000possibilistic, title={Possibilistic definitions of security-an assembly kit}, author={Heiko Mantel}, booktitle={{IEEE} Computer Security Foundations}, pages={185--199}, year={2000}, organization={IEEE} } @inproceedings{mantel2001preserving, title={Preserving information flow properties under refinement}, author={Heiko Mantel}, booktitle={{IEEE} Computer Security Foundations}, pages={78--91}, year={2001} } @inproceedings{mantel2002composition, title={On the composition of secure systems}, author={Heiko Mantel}, booktitle={{IEEE} Security and Privacy}, pages={88--101}, year={2002} } @article{zakinthinos1995composability, title={The composability of non-interference}, author={Aris Zakinthinos and E Stewart Lee}, journal={Journal of Computer Security}, volume={3}, number={4}, pages={269--281}, year={1995} } @inproceedings{johnson1988security, title={Security and the Composition of Machines.}, author={Dale M Johnson and F Javier Thayer}, booktitle={CSFW}, volume={88}, pages={72--89}, year={1988} } @article{askarov2008cryptographically, title={Cryptographically-masked flows}, author={Aslan Askarov and Daniel Hedin and Andrei Sabelfeld}, journal={Theoretical Computer Science}, volume={402}, number={2}, pages={82--101}, year={2008}, publisher={Elsevier} } @Misc{rivest2006threeballot, author = {Ronald L. Rivest}, title = {The {ThreeBallot} voting system}, howpublished = {\url{http://theory.lcs.mit.edu/\~rivest/Rivest-TheThreeBallotVotingSystem.pdf}}, month = Oct, year = 2006} @Misc{rivest2007three, title = {Three Voting Protocols: {ThreeBallot}, {VAV}, and {Twin}}, author= {Rivest, Ronald L and Smith, Warren D}, howpublished = {\url{http://people.csail.mit.edu/rivest/pubs/RS07.pdf}}, year = 2007} @inproceedings{clark2007security, title={On the security of ballot receipts in E2E voting systems}, author={Jeremy Clark and Aleks Essex and Carlisle Adams}, booktitle={Workshop on Trustworthy Elections ({WOTE})}, year={2007} } @incollection{chatzikokolakis2007making, title={Making random choices invisible to the scheduler}, author={Konstantinos Chatzikokolakis and Catuscia Palamidessi}, booktitle={CONCUR}, pages={42--58}, year={2007}, publisher={Springer} } @incollection{canetti2006time, title={Time-bounded task-PIOAs: A framework for analyzing security protocols}, author={Ran Canetti and Ling Cheung and Dilsun Kaynar and Moses Liskov and Nancy Lynch and Olivier Pereira and Roberto Segala}, booktitle={Distributed Computing}, pages={238--253}, year={2006}, publisher={Springer} } @article{CanettiCKLLPS08, author = {Ran Canetti and Ling Cheung and Dilsun Kirli Kaynar and Moses Liskov and Nancy A. Lynch and Olivier Pereira and Roberto Segala}, title = {Analyzing Security Protocols Using Time-Bounded Task-{PIOAs}}, journal = {Discrete Event Dynamic Systems}, volume = {18}, number = {1}, pages = {111--159}, year = {2008} } @article{mccamant2008quantitative, title={Quantitative information flow as network flow capacity}, author={Stephen McCamant and Michael D Ernst}, journal={ACM SIGPLAN Notices ({PLDI})}, volume={43}, number={6}, pages={193--205}, year={2008}, publisher={ACM} } @incollection{guttman2014security, title={Security Goals and Evolving Standards}, author={Joshua D Guttman and Moses D Liskov and Paul D Rowe}, booktitle={Security Standardisation Research}, pages={93--110}, year={2014}, publisher={Springer} } @Article{MoranHeatherSchneider2015, author = {Murat Moran and James Heather and Steve Schneider}, title = {Automated anonymity verification of the {ThreeBallot} and {VAV} voting systems}, journal = {Software and Systems Modeling}, year = 2015, note = {Forthcoming}} @incollection{sabelfeld2010dynamic, title={From dynamic to static and back: Riding the roller coaster of information-flow control research}, author={Andrei Sabelfeld and Alejandro Russo}, booktitle={Perspectives of Systems Informatics}, pages={352--365}, year={2010}, publisher={Springer} } @inproceedings{RamsdellDGR14, author = {John D. Ramsdell and Daniel J. Dougherty and Joshua D. Guttman and Paul D. Rowe}, title = {A Hybrid Analysis for Security Protocols with State}, booktitle = {Integrated Formal Methods}, pages = {272--287}, year = {2014}, url = {http://dx.doi.org/10.1007/978-3-319-10181-1_17}, doi = {10.1007/978-3-319-10181-1_17}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/ifm/RamsdellDGR14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @article{denning1977certification, title={Certification of programs for secure information flow}, author={Dorothy E Denning and Peter J Denning}, journal={Communications of the ACM}, volume={20}, number={7}, pages={504--513}, year={1977}, publisher={ACM} } @inproceedings{Mattern1989, author = "Friedemann Mattern", editor = "M. Cosnard", title = "Virtual Time and Global States of Distributed Systems", booktitle = "Proc. Workshop on Parallel and Distributed Algorithms", year = "1989", pages = "215--226", address = "North-Holland / Elsevier", note = {(Reprinted in: Z. Yang, T.A. Marsland (Eds.), "Global States and Time in Distributed Systems", IEEE, 1994, pp. 123-133.)} } @inproceedings{balliu2011epistemic, title={Epistemic temporal logic for information flow security}, author={Musard Balliu and Mads Dam and Gurvan Le Guernic}, booktitle={Programming Languages and Analysis for Security}, year={2011}, organization={ACM} } @inproceedings{landauer1993lattice, title={A lattice of information}, author={Jaisook Landauer and Timothy Redmond}, booktitle={Computer Security Foundations Workshop}, pages={65--70}, year={1993}, organization={IEEE} } @inproceedings{cade92-pvs-old, AUTHOR = {{S.} Owre and {J.} {M.} Rushby and {N.} Shankar}, TITLE = {{PVS:} {A} Prototype Verification System}, BOOKTITLE = {Conference on Automated Deduction}, YEAR = 1992, SERIES = {LNAI}, MONTH = jun, note = {\url{http://pvs.csl.sri.com}} } @inproceedings{GuttmanNadel88, author = {Joshua D. Guttman and Mark E. Nadel}, title = {What Needs Securing?}, booktitle = {{IEEE} Computer Security Foundations Workshop}, pages = {34--57}, year = {1988} } @inproceedings{HuntMastroeni05, author = {Sebastian Hunt and Isabella Mastroeni}, title = {The {PER} Model of Abstract Non-interference}, booktitle = {Static Analysis Symposium {SAS}}, pages = {171--185}, year = {2005} } @inproceedings{KuhlmanMBET08, author = {Doug Kuhlman and Ryan Moriarty and Tony Braskich and Steve Emeott and Mahesh V. Tripunitara}, title = {{A Correctness Proof of a Mesh Security Architecture}}, booktitle = {CSF}, year = {2008}, pages = {315-330}, ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2008.23}, crossref = {DBLP:conf/csfw/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{HeSDDM05, author = {Changhua He and Mukund Sundararajan and Anupam Datta and Ante Derek and John C. Mitchell}, title = {{A modular correctness proof of IEEE 802.11i and TLS}}, booktitle = {ACM Conference on Computer and Communications Security}, year = {2005}, pages = {2-15}, ee = {http://doi.acm.org/10.1145/1102120.1102124}, crossref = {DBLP:conf/ccs/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{BhargavanFGS08, author = {Karthikeyan Bhargavan and C{\'e}dric Fournet and Andrew D. Gordon and Nikhil Swamy}, title = {{Verified implementations of the information card federated identity-management protocol}}, booktitle = {ASIACCS}, year = {2008}, pages = {123-135}, ee = {http://doi.acm.org/10.1145/1368310.1368330}, crossref = {DBLP:conf/ccs/2008asia}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{BhargavanFCZ12, author = {Karthikeyan Bhargavan and C{\'e}dric Fournet and Ricardo Corin and Eugen Zalinescu}, title = {{Verified Cryptographic Implementations for TLS}}, journal = {ACM Trans. Inf. Syst. Secur.}, volume = {15}, number = {1}, year = {2012}, pages = {3}, ee = {http://doi.acm.org/10.1145/2133375.2133378}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{MitchellRRS08, author = {John C. Mitchell and Arnab Roy and Paul Rowe and Andre Scedrov}, title = {Analysis of {EAP-GPSK} Authentication Protocol}, booktitle = {ACNS}, year = {2008}, pages = {309-327}, ee = {http://dx.doi.org/10.1007/978-3-540-68914-0_19}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{rfc4120, author="C. Neuman and T. Yu and S. Hartman and K. Raeburn", title="{The Kerberos Network Authentication Service (V5)}", series="Request for Comments", number="4120", howpublished="RFC 4120 (Proposed Standard)", publisher="IETF", organization="Internet Engineering Task Force", year=2005, month=jul, note="Updated by RFCs 4537, 5021, 5896, 6111, 6112, 6113, 6649, 6806", url="http://www.ietf.org/rfc/rfc4120.txt", } @misc{rfc4556, author="L. Zhu and B. Tung", title="{Public Key Cryptography for Initial Authentication in Kerberos (PKINIT)}", series="Request for Comments", number="4556", howpublished="RFC 4556 (Proposed Standard)", publisher="IETF", organization="Internet Engineering Task Force", year=2006, month=jun, note="Updated by RFC 6112", url="http://www.ietf.org/rfc/rfc4556.txt", } @article{CervesatoJSTW08, author = {Iliano Cervesato and Aaron D. Jaggard and Andre Scedrov and Joe-Kai Tsay and Christopher Walstad}, title = {Breaking and fixing public-key {Kerberos}}, journal = {Inf. Comput.}, volume = {206}, number = {2-4}, year = {2008}, pages = {402-424}, ee = {http://dx.doi.org/10.1016/j.ic.2007.05.005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{rfc5746, author="E. Rescorla and M. Ray and S. Dispensa and N. Oskov", title="{Transport Layer Security (TLS) Renegotiation Indication Extension}", series="Request for Comments", number="5746", howpublished="RFC 5746 (Proposed Standard)", publisher="IETF", organization="Internet Engineering Task Force", year=2010, month=feb, url="http://www.ietf.org/rfc/rfc5746.txt", } @misc{rfc5246, author="T. Dierks and E. Rescorla", title="{The Transport Layer Security (TLS) Protocol Version 1.2}", series="Request for Comments", number="5246", howpublished="RFC 5246 (Proposed Standard)", publisher="IETF", organization="Internet Engineering Task Force", year=2008, month=aug, note="Updated by RFCs 5746, 5878, 6176", url="http://www.ietf.org/rfc/rfc5246.txt", } @article{BasinCM13, author = {David A. Basin and Cas Cremers and Simon Meier}, title = {Provably repairing the {ISO/IEC} 9798 standard for entity authentication}, journal = {Journal of Computer Security}, volume = {21}, number = {6}, year = {2013}, pages = {817-846}, ee = {http://dx.doi.org/10.3233/JCS-130472}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article {Meadows03, author = {Catherine Meadows}, title = {Formal methods for cryptographic protocol analysis: Emerging issues and trends}, journal = {IEEE Journal on Selected Areas in Communications}, volume = {21}, number = {1}, year = {2003}, pages = {44-54}, ee = {http://dx.doi.org/10.1109/JSAC.2002.806125}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article {PimentelM08, author = {Juan Carlos L{\'o}pez Pimentel and Raul Monroy}, title = {Formal Support to Security Protocol Development: A Survey}, journal = {Computaci{\'o}n y Sistemas}, volume = {12}, number = {1}, year = {2008}, ee = {http://cys.cic.ipn.mx/ojs/index.php/CyS/article/view/1190}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings {BhargavanDFPS14, author = {Karthikeyan Bhargavan and Antoine Delignat-Lavaud and C{\'e}dric Fournet and Alfredo Pironti and Pierre-Yves Strub}, title = {Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over {TLS}}, booktitle = {IEEE Symposium on Security and Privacy}, year = {2014} } @article {DattaDMR07, author = {Anupam Datta and Ante Derek and John C. Mitchell and Arnab Roy}, title = {Protocol Composition Logic ({PCL})}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {172}, year = {2007}, pages = {311-358}, } @Unpublished{RoweEtAl2015, author = {Paul D. Rowe and Joshua D. Guttman and Moses D. Liskov}, title = {Measuring Protocol Strength with Security Goals}, note = {Submitted to \emph{IJIS} in the SSR 2014 special issue. Available at \url{http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf}}, month = {April}, year = 2015} @Article{RoweEtAl2016, author = {Paul D. Rowe and Joshua D. Guttman and Moses D. Liskov}, title = {Measuring Protocol Strength with Security Goals}, journal = {International Journal of Information Security}, year = 2016, volume = 15, number = 6, month = nov, pages = {575--596}, note = {DOI 10.1007/s10207-016-0319-z, \url{http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdf}}} @inproceedings{KremerKuennemann14, author = {Steve Kremer and Robert K{\"{u}}nnemann}, title = {Automated Analysis of Security Protocols with Global State}, booktitle = {{IEEE} Symposium on Security and Privacy}, pages = {163--178}, year = {2014}, url = {http://dx.doi.org/10.1109/SP.2014.18}, doi = {10.1109/SP.2014.18}, timestamp = {Tue, 02 Dec 2014 18:47:29 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/sp/KremerK14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{MeierSCB13, author = {Simon Meier and Benedikt Schmidt and Cas Cremers and David A. Basin}, title = {The {tamarin} Prover for the Symbolic Analysis of Security Protocols}, booktitle = {Computer Aided Verification ({CAV})}, pages = {696--701}, year = 2013, url = {http://dx.doi.org/10.1007/978-3-642-39799-8_48}, doi = {10.1007/978-3-642-39799-8_48}, timestamp = {Fri, 12 Jul 2013 13:57:42 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/cav/MeierSCB13}, bibsource = {dblp computer science bibliography, http://dblp.org} } @Misc{GLRR2015a, author = {Joshua D. Guttman and Moses D. Liskov and John D. Ramsdell and Paul D. Rowe}, title = {Formal Support for Standardizing Protocols with State (extended version)}, howpublished = {Arxiv}, month = sep, year = 2015, note = {Available at \url{http://arxiv.org/abs/1509.07552}}} @InProceedings{AlmousaEtAl2015, author = {Omar Almousa and Sebastian A. M\"{o}dersheim and Paolo Modesti and Luca Vigan\`{o}}, title = {Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment}, booktitle = {ESORICS}, year = 2015, series = {LNCS}, month = sep, publisher = {Springer}} @InProceedings{AndoGuttman15, author = {Megumi Ando and Joshua D. Guttman}, title = {Composable Bounds on Information Flow from Distribution Differences}, booktitle = {Data Privacy Management, and Security Assurance}, year = 2015, volume = 9481, series = {LNCS}, pages = {13--29}, publisher = {Springer}} @InProceedings{AdaoEtAl16, author = {Pedro Ad{\~a}o and Riccardo Focardi and Flaminia L. Luccio and Joshua D. Guttman}, title = {Localizing Firewall Security Policies}, booktitle = {{IEEE} Symp. Computer Security Foundations}, year = 2016, month = {June}, organization = {{IEEE} Computer Society}} @Inbook{GuttmanEtAl2016, author="Joshua D. Guttman and John D. Ramsdell and Paul D. Rowe", title="Cross-Tool Semantics for Protocol Security Goals", bookTitle="Security Standardisation Research, SSR 2016", year="2016", publisher="Springer", pages="32--61", isbn="978-3-319-49100-4", doi="10.1007/978-3-319-49100-4_2", url="http://dx.doi.org/10.1007/978-3-319-49100-4_2" } @inproceedings{DeMoura08, author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj}, title = {Z3: An Efficient SMT Solver}, booktitle = {Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, series = {TACAS'08/ETAPS'08}, year = {2008}, isbn = {3-540-78799-2, 978-3-540-78799-0}, location = {Budapest, Hungary}, pages = {337--340}, numpages = {4}, url = {https://github.com/Z3Prover/z3/wiki}, acmid = {1792766}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg} } @inproceedings{Maurer05, author = {Ueli M. Maurer}, title = {Abstract Models of Computation in Cryptography}, booktitle = {Cryptography and Coding}, pages = {1--12}, year = {2005}, publisher = {Springer}, volume = {3796}, series = {LNCS}, url = {https://doi.org/10.1007/11586821_1}, doi = {10.1007/11586821_1}, timestamp = {Tue, 30 May 2017 16:36:52 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/ima/Maurer05}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{BartheFFMSS14, author = {Gilles Barthe and Edvard Fagerholm and Dario Fiore and John C. Mitchell and Andre Scedrov and Benedikt Schmidt}, title = {Automated Analysis of Cryptographic Assumptions in Generic Group Models}, booktitle = {{CRYPTO}}, pages = {95--112}, year = 2014, publisher = {Springer}, volume = 8616, series = {LNCS}, url = {https://doi.org/10.1007/978-3-662-44371-2_6}, doi = {10.1007/978-3-662-44371-2_6}, timestamp = {Fri, 02 Jun 2017 20:50:15 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/crypto/BartheFFMSS14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{Shoup97, author = {Victor Shoup}, title = {Lower Bounds for Discrete Logarithms and Related Problems}, booktitle = {{EUROCRYPT}}, pages = {256--266}, year = {1997}, series = {Lecture Notes in Computer Science}, volume = {1233}, publisher = {Springer}, url = {https://doi.org/10.1007/3-540-69053-0_18}, doi = {10.1007/3-540-69053-0_18}, timestamp = {Mon, 22 May 2017 17:12:28 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/eurocrypt/Shoup97}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{LiskovThayer14, author = {Moses Liskov and F. Javier Thayer}, title = {Modeling {Diffie-Hellman} Derivability for Automated Analysis}, booktitle = {{IEEE} Computer Security Foundations}, pages = {232--243}, year = 2014, url = {https://doi.org/10.1109/CSF.2014.24}, doi = {10.1109/CSF.2014.24}, timestamp = {Thu, 25 May 2017 00:40:51 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/csfw/LiskovT14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{MoedersheimKatsoris14, author = {Sebastian M{\"{o}}dersheim and Georgios Katsoris}, title = {A Sound Abstraction of the Parsing Problem}, booktitle = {{IEEE} {CSF}}, pages = {259--273}, year = {2014}, url = {https://doi.org/10.1109/CSF.2014.26}, doi = {10.1109/CSF.2014.26}, timestamp = {Thu, 25 May 2017 00:40:50 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/csfw/ModersheimK14}, bibsource = {dblp computer science bibliography, http://dblp.org} } @inproceedings{GuttmanLRR15, author = {Joshua D. Guttman and Moses D. Liskov and John D. Ramsdell and Paul D. Rowe}, title = {Formal Support for Standardizing Protocols with State}, booktitle = {Security Standardisation Research {SSR}}, pages = {246--265}, year = {2015}, note = {Extended version at \url{http://arxiv.org/abs/1509.07552}}, url = {https://doi.org/10.1007/978-3-319-27152-1_13}, doi = {10.1007/978-3-319-27152-1_13}, timestamp = {Sun, 21 May 2017 00:17:16 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/secsr/GuttmanLRR15}, bibsource = {dblp computer science bibliography, http://dblp.org} } @InCollection{BaaderSnyder01, author = {Franz Baader and Wayne Snyder}, title = {Unification Theory}, booktitle = {Handbook of Automated Reasoning}, publisher = {The {MIT} Press}, year = 2001, editor = {Alan Robinson and Andrei Voronkov}, volume = 1, chapter = 8} @InCollection{BaaderSnyder01troublesome, author = {Franz Baader and Wayne Snyder}, title = {Unification Theory}, booktitle = {Handbook of Automated Reasoning}, publisher = {The {MIT} Press}, year = 2001, editor = {Alan Robinson and Andrei Voronkov}, volume = 1, chapter = 8, note = {\url{http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf‎}}} @Misc{LiskovGRRT18, author = {Moses D. Liskov and Joshua D. Guttman and John D. Ramsdell and Paul D. Rowe and F. Javier Thayer}, title = {Enrich-by-need Protocol Analysis for {Diffie-Hellman} (Extended Version)}, howpublished = {\url{http://arxiv.org/abs/1804.05713}}, month = {April}, year = 2018} @article{vigano2006automated, title={Automated security protocol analysis with the {AVISPA} tool}, author={Luca Vigan{\`o}}, journal={Electronic Notes in Theoretical Computer Science}, volume=155, pages={61--86}, year=2006, publisher={Elsevier} } @inproceedings{turuani2006cl, title={The {CL-Atse} protocol analyser}, author={Mathieu Turuani}, booktitle={Rewriting Techniques and Applications}, pages={277--286}, year={2006}, organization={Springer} } @inproceedings{Molina-MarkhamR17, author = {Andres Molina{-}Markham and Paul D. Rowe}, title = {Continuous Verification for Cryptographic Protocol Development}, booktitle = {Proceedings of the 1st {ACM} Workshop on the Internet of Safe Things, SafeThings@SenSys 2017, Delft, The Netherlands, November 5, 2017}, pages = {51--56}, year = {2017}, url = {https://doi.org/10.1145/3137003.3137006}, doi = {10.1145/3137003.3137006}, timestamp = {Tue, 06 Nov 2018 16:57:58 +0100}, biburl = {https://dblp.org/rec/bib/conf/sensys/Molina-MarkhamR17}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{AvoineBGG0OR17, author = {Gildas Avoine and Xavier Bultel and S{\'{e}}bastien Gambs and David G{\'{e}}rault and Pascal Lafourcade and Cristina Onete and Jean{-}Marc Robert}, editor = {Ramesh Karri and Ozgur Sinanoglu and Ahmad{-}Reza Sadeghi and Xun Yi}, title = {A Terrorist-fraud Resistant and Extractor-free Anonymous Distance-bounding Protocol}, booktitle = {Proceedings of the 2017 {ACM} on Asia Conference on Computer and Communications Security, AsiaCCS 2017, Abu Dhabi, United Arab Emirates, April 2-6, 2017}, pages = {800--814}, publisher = {{ACM}}, year = {2017}, url = {https://doi.org/10.1145/3052973.3053000}, doi = {10.1145/3052973.3053000}, timestamp = {Mon, 16 Sep 2019 15:24:37 +0200}, biburl = {https://dblp.org/rec/conf/ccs/AvoineBGG0OR17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{CremersRSC12, author = {Cas J. F. Cremers and Kasper Bonne Rasmussen and Benedikt Schmidt and Srdjan {\v{C}}apkun}, title = {Distance Hijacking Attacks on Distance Bounding Protocols}, booktitle = {{IEEE} Symposium on Security and Privacy, {SP} 2012, 21-23 May 2012, San Francisco, California, {USA}}, pages = {113--127}, publisher = {{IEEE} Computer Society}, year = {2012}, url = {https://doi.org/10.1109/SP.2012.17}, doi = {10.1109/SP.2012.17}, timestamp = {Wed, 16 Oct 2019 14:14:51 +0200}, biburl = {https://dblp.org/rec/conf/sp/CremersRSC12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{MauwSTT18, author = {Sjouke Mauw and Zach Smith and Jorge Toro{-}Pozo and Rolando Trujillo{-}Rasua}, title = {Distance-Bounding Protocols: Verification without Time and Location}, booktitle = {2018 {IEEE} Symposium on Security and Privacy, {SP} 2018, Proceedings, 21-23 May 2018, San Francisco, California, {USA}}, pages = {549--566}, publisher = {{IEEE} Computer Society}, year = {2018}, url = {https://doi.org/10.1109/SP.2018.00001}, doi = {10.1109/SP.2018.00001}, timestamp = {Sat, 19 Oct 2019 20:19:29 +0200}, biburl = {https://dblp.org/rec/conf/sp/MauwSTT18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{ChothiaRS18, author = {Tom Chothia and Joeri de Ruiter and Ben Smyth}, editor = {William Enck and Adrienne Porter Felt}, title = {Modelling and Analysis of a Hierarchy of Distance Bounding Attacks}, booktitle = {27th {USENIX} Security Symposium, {USENIX} Security 2018, Baltimore, MD, USA, August 15-17, 2018}, pages = {1563--1580}, publisher = {{USENIX} Association}, year = {2018}, url = {https://www.usenix.org/conference/usenixsecurity18/presentation/chothia}, timestamp = {Mon, 20 Aug 2018 15:16:57 +0200}, biburl = {https://dblp.org/rec/conf/uss/ChothiaRS18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{MaurerS96, author = {Ueli M. Maurer and Pierre E. Schmid}, title = {A Calculus for Security Bootstrapping in Distributed Systems}, journal = {Journal of Computer Security}, volume = {4}, number = {1}, pages = {55--80}, year = {1996}, url = {https://doi.org/10.3233/JCS-1996-4104}, doi = {10.3233/JCS-1996-4104}, timestamp = {Fri, 26 May 2017 22:53:13 +0200}, biburl = {https://dblp.org/rec/journals/jcs/MaurerS96.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{ThayerSG10, author = {F. Javier Thayer and Vipin Swarup and Joshua D. Guttman}, title = {Metric Strand Spaces for Locale Authentication Protocols}, booktitle = {Trust Management, {IFIP} {WG} 11.11}, series = {{IFIP} Advances in Information and Communication Technology}, volume = {321}, pages = {79--94}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-13446-3\_6}, doi = {10.1007/978-3-642-13446-3\_6}, timestamp = {Sat, 19 Oct 2019 20:14:34 +0200}, biburl = {https://dblp.org/rec/conf/ifiptm/ThayerSG10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{BrandsC93, author = {Stefan Brands and David Chaum}, editor = {Tor Helleseth}, title = {Distance-Bounding Protocols (Extended Abstract)}, booktitle = {Advances in Cryptology - {EUROCRYPT} '93, Workshop on the Theory and Application of of Cryptographic Techniques, Lofthus, Norway, May 23-27, 1993, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {765}, pages = {344--359}, publisher = {Springer}, year = {1993}, url = {https://doi.org/10.1007/3-540-48285-7\_30}, doi = {10.1007/3-540-48285-7\_30}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/eurocrypt/BrandsC93.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{RasmussenC10, author = {Kasper Bonne Rasmussen and Srdjan Capkun}, title = {Realization of {RF} Distance Bounding}, booktitle = {19th {USENIX} Security Symposium, Washington, DC, USA, August 11-13, 2010, Proceedings}, pages = {389--402}, publisher = {{USENIX} Association}, year = {2010}, url = {http://www.usenix.org/events/sec10/tech/full\_papers/Rasmussen.pdf}, timestamp = {Wed, 04 Jul 2018 13:06:34 +0200}, biburl = {https://dblp.org/rec/conf/uss/RasmussenC10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @incollection{MeadowsPPCS07, author = {Catherine A. Meadows and Radha Poovendran and Dusko Pavlovic and LiWu Chang and Paul F. Syverson}, editor = {Radha Poovendran and Sumit Roy and Cliff Wang}, title = {Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks}, booktitle = {Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks}, series = {Advances in Information Security}, volume = {30}, pages = {279--298}, publisher = {Springer}, year = {2007}, url = {https://doi.org/10.1007/978-0-387-46276-9\_12}, doi = {10.1007/978-0-387-46276-9\_12}, timestamp = {Tue, 16 May 2017 14:24:25 +0200}, biburl = {https://dblp.org/rec/series/ais/MeadowsPPCS07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{AvoineT09, author = {Gildas Avoine and Aslan Tchamkerten}, editor = {Pierangela Samarati and Moti Yung and Fabio Martinelli and Claudio Agostino Ardagna}, title = {An Efficient Distance Bounding {RFID} Authentication Protocol: Balancing False-Acceptance Rate and Memory Requirement}, booktitle = {Information Security, 12th International Conference, {ISC} 2009, Pisa, Italy, September 7-9, 2009. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5735}, pages = {250--261}, publisher = {Springer}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-04474-8\_21}, doi = {10.1007/978-3-642-04474-8\_21}, timestamp = {Tue, 14 May 2019 10:00:53 +0200}, biburl = {https://dblp.org/rec/conf/isw/AvoineT09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{Trujillo-RasuaMA10, author = {Rolando Trujillo{-}Rasua and Benjamin Martin and Gildas Avoine}, editor = {Siddika Berna Ors Yalcin}, title = {The Poulidor Distance-Bounding Protocol}, booktitle = {Radio Frequency Identification: Security and Privacy Issues - 6th International Workshop, RFIDSec 2010, Istanbul, Turkey, June 8-9, 2010, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {6370}, pages = {239--257}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-16822-2\_19}, doi = {10.1007/978-3-642-16822-2\_19}, timestamp = {Tue, 14 May 2019 10:00:38 +0200}, biburl = {https://dblp.org/rec/conf/rfidsec/Trujillo-RasuaMA10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{HanckeK05, author = {Gerhard P. Hancke and Markus G. Kuhn}, title = {An {RFID} Distance Bounding Protocol}, booktitle = {First International Conference on Security and Privacy for Emerging Areas in Communications Networks, SecureComm 2005, Athens, Greece, 5-9 September, 2005}, pages = {67--73}, publisher = {{IEEE}}, year = {2005}, url = {https://doi.org/10.1109/SECURECOMM.2005.56}, doi = {10.1109/SECURECOMM.2005.56}, timestamp = {Wed, 16 Oct 2019 14:14:54 +0200}, biburl = {https://dblp.org/rec/conf/securecomm/HanckeK05.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{MauwTT16, author = {Sjouke Mauw and Jorge Toro{-}Pozo and Rolando Trujillo{-}Rasua}, title = {A Class of Precomputation-Based Distance-Bounding Protocols}, booktitle = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2016, Saarbr{\"{u}}cken, Germany, March 21-24, 2016}, pages = {97--111}, publisher = {{IEEE}}, year = {2016}, url = {https://doi.org/10.1109/EuroSP.2016.19}, doi = {10.1109/EuroSP.2016.19}, timestamp = {Wed, 16 Oct 2019 14:14:55 +0200}, biburl = {https://dblp.org/rec/conf/eurosp/MauwTT16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{KimA09, author = {Chong Hee Kim and Gildas Avoine}, editor = {Juan A. Garay and Atsuko Miyaji and Akira Otsuka}, title = {{RFID} Distance Bounding Protocol with Mixed Challenges to Prevent Relay Attacks}, booktitle = {Cryptology and Network Security, 8th International Conference, {CANS} 2009, Kanazawa, Japan, December 12-14, 2009. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5888}, pages = {119--133}, publisher = {Springer}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-10433-6\_9}, doi = {10.1007/978-3-642-10433-6\_9}, timestamp = {Tue, 14 May 2019 10:00:50 +0200}, biburl = {https://dblp.org/rec/conf/cans/KimA09.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{MunillaP08, author = {Jorge Munilla and Alberto Peinado}, title = {Distance bounding protocols for {RFID} enhanced by using void-challenges and analysis in noisy channels}, journal = {Wireless Communications and Mobile Computing}, volume = {8}, number = {9}, pages = {1227--1232}, year = {2008}, url = {https://doi.org/10.1002/wcm.590}, doi = {10.1002/wcm.590}, timestamp = {Wed, 17 May 2017 14:25:29 +0200}, biburl = {https://dblp.org/rec/journals/wicomm/MunillaP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{ReidNTS07, author = {Jason Reid and Juan Manuel Gonz{\'{a}}lez Nieto and Tee Tang and Bouchra Senadji}, editor = {Feng Bao and Steven Miller}, title = {Detecting relay attacks with timing-based protocols}, booktitle = {Proceedings of the 2007 {ACM} Symposium on Information, Computer and Communications Security, {ASIACCS} 2007, Singapore, March 20-22, 2007}, pages = {204--213}, publisher = {{ACM}}, year = {2007}, url = {https://doi.org/10.1145/1229285.1229314}, doi = {10.1145/1229285.1229314}, timestamp = {Tue, 06 Nov 2018 11:07:29 +0100}, biburl = {https://dblp.org/rec/conf/ccs/ReidNTS07.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{KimAKSP08, author = {Chong Hee Kim and Gildas Avoine and Fran{\c{c}}ois Koeune and Fran{\c{c}}ois{-}Xavier Standaert and Olivier Pereira}, editor = {Pil Joong Lee and Jung Hee Cheon}, title = {The Swiss-Knife {RFID} Distance Bounding Protocol}, booktitle = {Information Security and Cryptology - {ICISC} 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {5461}, pages = {98--115}, publisher = {Springer}, year = {2008}, url = {https://doi.org/10.1007/978-3-642-00730-9\_7}, doi = {10.1007/978-3-642-00730-9\_7}, timestamp = {Tue, 14 May 2019 10:00:36 +0200}, biburl = {https://dblp.org/rec/conf/icisc/KimAKSP08.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{AvoineBGGLOR17, author = {Gildas Avoine and Xavier Bultel and S{\'{e}}bastien Gambs and David G{\'{e}}rault and Pascal Lafourcade and Cristina Onete and Jean{-}Marc Robert}, title = {A Terrorist-fraud Resistant and Extractor-free Anonymous Distance-bounding Protocol}, journal = {{IACR} Cryptology ePrint Archive}, volume = {2017}, pages = {297}, year = {2017}, url = {http://eprint.iacr.org/2017/297}, timestamp = {Tue, 14 Aug 2018 17:08:17 +0200}, biburl = {https://dblp.org/rec/journals/iacr/AvoineBGGLOR17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{ChothiaGRBT15, author = {Tom Chothia and Flavio D. Garcia and Joeri de Ruiter and Jordi van den Breekel and Matthew Thompson}, editor = {Rainer B{\"{o}}hme and Tatsuaki Okamoto}, title = {Relay Cost Bounding for Contactless {EMV} Payments}, booktitle = {Financial Cryptography and Data Security - 19th International Conference, {FC} 2015, San Juan, Puerto Rico, January 26-30, 2015, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {8975}, pages = {189--206}, publisher = {Springer}, year = {2015}, url = {https://doi.org/10.1007/978-3-662-47854-7\_11}, doi = {10.1007/978-3-662-47854-7\_11}, timestamp = {Tue, 14 May 2019 10:00:38 +0200}, biburl = {https://dblp.org/rec/conf/fc/ChothiaGRBT15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{MauwSTT19, author = {Sjouke Mauw and Zach Smith and Jorge Toro{-}Pozo and Rolando Trujillo{-}Rasua}, editor = {Lorenzo Cavallaro and Johannes Kinder and XiaoFeng Wang and Jonathan Katz}, title = {Post-Collusion Security and Distance Bounding}, booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2019, London, UK, November 11-15, 2019}, pages = {941--958}, publisher = {{ACM}}, year = {2019}, url = {https://doi.org/10.1145/3319535.3345651}, doi = {10.1145/3319535.3345651}, timestamp = {Fri, 08 Nov 2019 12:58:49 +0100}, biburl = {https://dblp.org/rec/conf/ccs/MauwSTT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DebantD19, author = {Alexandre Debant and St{\'{e}}phanie Delaune}, editor = {Flemming Nielson and David Sands}, title = {Symbolic Verification of Distance Bounding Protocols}, booktitle = {Principles of Security and Trust - 8th International Conference, {POST} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11426}, pages = {149--174}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-17138-4\_7}, doi = {10.1007/978-3-030-17138-4\_7}, timestamp = {Fri, 31 Jan 2020 21:32:30 +0100}, biburl = {https://dblp.org/rec/conf/post/DebantD19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{Desmedt88, author={Yvo Desmedt}, title={Major security problems with the `unforgeable' (feige)-fiat-shamir proofs of identity and how to overcome them}, booktitle={SECURICOM'88}, year={1988}, pages={15--17} } @inproceedings{AlTurkiKKNST18, author = {Musab A. AlTurki and Max I. Kanovich and Tajana Ban Kirigin and Vivek Nigam and Andre Scedrov and Carolyn L. Talcott}, editor = {David Lie and Mohammad Mannan}, title = {Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols}, booktitle = {Proceedings of the 2018 Workshop on Cyber-Physical Systems Security and PrivaCy, CPS-SPC@CCS 2018, Toronto, ON, Canada, October 19, 2018}, pages = {60--71}, publisher = {{ACM}}, year = {2018}, url = {https://doi.org/10.1145/3264888.3264895}, doi = {10.1145/3264888.3264895}, timestamp = {Wed, 21 Nov 2018 12:44:06 +0100}, biburl = {https://dblp.org/rec/conf/ccs/AlTurkiKKNST18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{KanovichKNST17, author = {Max I. Kanovich and Tajana Ban Kirigin and Vivek Nigam and Andre Scedrov and Carolyn L. Talcott}, title = {Time, computational complexity, and probability in the analysis of distance-bounding protocols}, journal = {Journal of Computer Security}, volume = {25}, number = {6}, pages = {585--630}, year = {2017}, url = {https://doi.org/10.3233/JCS-0560}, doi = {10.3233/JCS-0560}, timestamp = {Wed, 30 Aug 2017 15:38:06 +0200}, biburl = {https://dblp.org/rec/journals/jcs/KanovichKNST17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{KanovichKNST16, author = {Max I. Kanovich and Tajana Ban Kirigin and Vivek Nigam and Andre Scedrov and Carolyn L. Talcott}, editor = {Martin Fr{\"{a}}nzle and Nicolas Markey}, title = {Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems}, booktitle = {Formal Modeling and Analysis of Timed Systems - 14th International Conference, {FORMATS} 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9884}, pages = {228--244}, publisher = {Springer}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-44878-7\_14}, doi = {10.1007/978-3-319-44878-7\_14}, timestamp = {Tue, 14 May 2019 10:00:38 +0200}, biburl = {https://dblp.org/rec/conf/formats/KanovichKNST16.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{AlTurkiKKNST19, author = {Musab A. AlTurki and Tajana Ban Kirigin and Max I. Kanovich and Vivek Nigam and Andre Scedrov and Carolyn L. Talcott}, editor = {Joshua D. Guttman and Carl E. Landwehr and Jos{\'{e}} Meseguer and Dusko Pavlovic}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {192--213}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-19052-1\_13}, doi = {10.1007/978-3-030-19052-1\_13}, timestamp = {Fri, 24 May 2019 17:45:03 +0200}, biburl = {https://dblp.org/rec/conf/birthday/AlTurkiKKNST19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }