From Mohamed-Salah.Bouassida at loria.fr Fri Jan 20 18:23:51 2006 From: Mohamed-Salah.Bouassida at loria.fr (Mohamed Salah Bouassida) Date: Mon Jan 23 11:01:27 2006 Subject: [Avispa-users] problem in the AVISPA web page Message-ID: <43D11CA7.8090600@loria> Hello, there is a problem in the web page of the AVISPA tool, at any execution, we obtain the following message: Sorry too many backends are running and there are not enough resources available. Please try later.. Best regards, Mohamed Salah From armando at armandobook.mrg.dist.unige.it Mon Jan 23 17:11:10 2006 From: armando at armandobook.mrg.dist.unige.it (Alessandro Armando) Date: Mon Jan 23 18:15:46 2006 Subject: [Avispa-users] Hello and Introduction In-Reply-To: Message from "Desai, Bhavin" of "Fri, 09 Dec 2005 10:02:52 GMT." <6216396AEBE36247BF62B505A88ADA0A0C222E83@uk-ex002.groupinfra.com> Message-ID: <20060123161115.73BFE1E72F4@armandobook.mrg.dist.unige.it> Dear Desai, sorry for taking so long to reply. You may find a concise description of the AVISPA Tool as well as a brief summary of experimental results showing the level of automation that our tool is capable of at the following URL: http://www.avispa-project.org/papers/avispa-cav05.ps This paper, together with the information available at the AVISPA web page, provides a good starting point. Should you need further information please do not hesitate to contact us. We will be more reactive next time. I promise! :-) Best Regards, alessandro -- Alessandro Armando e-mail: armando@dist.unige.it Artificial Intelligence Laboratory http://www.ai.dist.unige.it/armando DIST - Universita' di Genova, phone: +39-0103532216 viale Causa 13, fax: +39-0103532948 16145 GENOVA, ITALY mobile: +39-3281003201 > Hello, > > > > How are you? I am taking the (part time) MSc in Information Security at > Royal Holloway University of London. I would appreciate any comments or > suggestions that you have regarding my initial ideas as described below. > > > > I would like to do my MSc project (to be completed by 8 September 2006) > on mathematical analysis of security protocols. The BAN logic (Mike > Burrows, Martin Abadi, and Roger Needham) may provide a good starting > point since it was the first and is probably the most famous analytical > method. However, there are other formal methodologies. Some suitable > websites that I have found as a result of an initial search are as > follows (although I have not investigated them very deeply at present): > > > > * http://www.avispa-project.org/ (of course) > > * http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html > > * http://www.stcatz.ox.ac.uk/academic_staff_pages/lowe_gavin.htm > > * > http://portal.surrey.ac.uk/portal/page?_pageid=798,332537&_dad=portal&_s > chema=PORTAL > > * And many others!!! > > > > It would be interesting to see if the newer methods can find known (and > possibly additional) vulnerabilities that have already been found by > utilisation of the traditional methods, but perhaps shorter, faster or > more elegantly. It may also be interesting to see whether security > protocols that have not yet been formally analysed could be subjected to > modern mathematical analyses. To find a significant vulnerability in a > relatively new protocol would be an excellent bonus for this MSc > project, although the time constraints may preclude this eventuality. > > > > In addition to the MSc in Information Security which is in progress at > present, my formal academic & professional qualifications are as > follows: > > > > * BSc, Grade II(i), Pure Mathematics, University of Kent, 1984. > > * MPhil (by thesis), Mathematical Logic, University of > Nottingham, 1987. > > * BCS ISEB Certificate in Information Security Management > Principles, 2000. > > * Certified Information Systems Security Professional (CISSP), > 2004. > > * (plus many other smaller/specialised security courses and > training.) > > > > A brief overview of my career and experience is as follows. In the > Systems Assurance Division of EDS in the early 1990s I was in a team > that developed a Z tool in Lisp on Sun workstations, for CESG. Then I > moved into projects performing safety critical static source code > analysis using SPADE and MALPAS. We also developed a proprietary static > code analysis tool written initially in Prolog and then completely > rewritten in SML. After that I joined the CLEF part of EDS to do an > ITSEC E3 evaluation of a database. In 1996 I joined the Logica CLEF to > do further ITSEC and Common Criteria evaluations covering operating > systems, databases, firewalls, crypto tools, etc. From 2000 to 2002 I > worked for Platform 7 Limited (which was bought by Datacard) on smart > card security. I am currently in the LogicaCMG CLEF at Leatherhead, > doing Common Criteria security evaluations and consultancy. > > > > Thanks in advance for your general comments on the above. > > > > I look forward to your reply. > > > > Bhavin. > > _____________ > > > > Bhavin Desai > > Security Consultant > > Security Practice > > LogicaCMG > > Chaucer House > > Springfield Drive > > Leatherhead > > Surrey > > KT22 7LP > > United Kingdom > > T: +44 (0) 1372 369 639 > > F: +44 (0) 1372 369834 > > e: bhavin.desai@logicacmg.com > > w: http://www.logicacmg.com/ > > > > > > > > > > > > > > > > This e-mail and any attachment is for authorised use by the intended recipient(s) only. It may contain proprietary material, confidential information and/or be subject to legal privilege. It should not be copied, disclosed to, retained or used by, any other party. If you are not an intended recipient then please promptly delete this e-mail and any attachment and all copies and inform the sender. Thank you. > _______________________________________________ > Avispa-users mailing list > Avispa-users@avispa-project.org > http://www.avispa-project.org/mailman/listinfo/avispa-users From Michael.Rusinowitch at loria.fr Tue Jan 24 17:49:39 2006 From: Michael.Rusinowitch at loria.fr (Michael Rusinowitch) Date: Tue Jan 24 18:54:11 2006 Subject: [Avispa-users] Workshop on Collaboration and Security Message-ID: <43D65AA3.7000704@loria> CALL FOR PAPERS Workshop on Collaboration and Security (COLSEC'06) The 2006 International Symposium on Collaborative Technologies and Systems (CTS'06) May 14-17, 2006 Las Vegas, Nevada, USA http://www.engr.udayton.edu/faculty/wsmari/cts06/ ------------------------------------------------------------------------- Submission Deadline: February 7, 2006 ------------------------------------------------------------------------- Brief Description: Collaboration relies on distributed systems that provide the required security properties. Virtual organizations often use the Internet to support collaboration. The Internet, operating systems and distributed environments currently suffer from poor security support and cannot resist common attacks (spamming, worms, session hijacking, buffer overflow, denial of service, social engineering, etc.). Collaborative organizations require better security properties (strong authentication, efficient encryption, Mandatory Access Control, insurance of confidentiality, integrity, non-repudiation and availability). Nowadays, collaborative organizations use new technologies such as mobile devices, smartcards, wireless networks, high performance networks and grid computing. These environments introduce new needs, requirements and difficulties related to security. Hence, collaborative organizations and technologies face several challenges in the field of security. This Workshop on Security and Collaboration - to be held as part of the 2006 International Symposium on Collaborative Technologies and Systems (CTS'06) - will focus on security issues related to collaborative systems with emphasis on distributed environments, smartcards, grid or clustering systems for cooperation, mobile and wireless cooperation. The aim is to have a dedicated workshop that fosters closer interactions among researchers and users communities, providing an excellent opportunity for them to meet and discuss their ideas. It addresses specifically relationships between collaborative systems and security. It intends to present new challenges and solutions related to latest security requirements, specific methods of access control enabling large scale cooperation, usage of mobile technologies and smartcards, new security infrastructures supporting better prevention, detection, recovery and healing in the context of cooperative systems. It will also consider security in different domains of application (e.g., e-Government, e-Business, Public Services, P2P, e-Social Security, Medical Collaboration, ...). We invite original contributions from researchers in academia, research institutions and industry on these emerging and important areas of information technology. Workshop topics include, but are not limited to, the following: * Frameworks for Security in Collaborative Systems * Access Control in Collaborative Environments * Trusted Operating Systems for Distributed Environments * Security of Grid and Cluster Architectures Supporting Cooperative Applications * Honeypots for Collaborative Systems * Intrusion and Attacks Detection for Collaborative Systems * Role Based, Reputation, and Trust * Encryption and Cryptography Systems Supporting Cooperative Systems * Use of Smartcards in the Context of Collaboration * Security in Mobile and Wireless Networks * Disclosure and Integrity Issues * Resistance to Denial of Service * Detection and Self-Recovery Schemes and Strategies Supporting Cooperation * Security for Specific Collaboration Domains (e.g., e-Government, e-Business, Public Services, P2P, e-Social Security, Medical Collaboration) Submission Instructions: Papers reporting original and unpublished research results on above and any other related topics are solicited. Submission should include a cover page with authors' names, affiliations, addresses, fax and phone numbers, and email addresses. Please indicate clearly the corresponding author. Include up to 6 keywords from the above list and an abstract of no more than 300 words. Please submit a PDF copy of your full manuscript (not to exceed 15 double-spaced pages including figures, tables, and references, or not to exceed 8 pages in length in single-space, two columns IEEE format Conference style) to christian.toinard@ensi-bourges.fr and jean-francois.lalande@ensi-bourges.fr. Electronic submissions will be accepted only in PDF format, sent at the email address above or uploaded at http://www.univ-orleans.fr/lifo/Manifestations/CTS2006/COLSEC2006/. For other electronic formats, please check with the organizers. Consistent with standard practice, each submitted paper will receive a minimum of three reviews. Papers will be selected based on their originality, timeliness, significance, relevance, and clarity of presentation. Initial selection will be based on full papers. Submission implies the willingness of at least one of the authors to register and present the paper, if accepted. All accepted papers in the Workshop are required to be presented and will be included in the Symposium proceedings. It is our intent to have the proceedings formally published in hard and soft copies and be available at the time of the conference. Further instructions will be provided at http://www.univ-orleans.fr/lifo/Manifestations/CTS2006/COLSEC2006/ Organizers Information: Prof. Christian Toinard and Dr Jean-Fran?ois Lalande Laboratoire d'Informatique Fondamentale d'Orl?ans (LIFO) ENSI-Bourges 10 Bld Lahitolle 18020 Bourges Cedex France Emails: christian.toinard@ensi-bourges.fr , jean-francois.lalande@ensi-bourges.fr Technical Program Committee: All submitted papers will be rigorously reviewed by the workshop technical program committee members. Dr. Elisa Bertino (Purdue University, USA) Dr. Jorge R. Cuellar(Siemens AG Corporate Technology, Germany) Dr. Nora Cuppens (ENST Bretagne, France) Dr. Michel Cukier (University of Maryland, USA) Dr. Jean-Bernard Fisher (Oberthur Card Systems, France) Mr. Vincent Glaume (CEA, France) Pr. Claude Godard (INRIA Lorraine, France) Pr. Herv? Guyennet (LIFC, France) Dr. Fabien Laguillaumie (INRIA Futurs/LIX, France) Dr. Volkmar Lotz (SAP, France) Pr. Pierre Paradinas (CNAM Paris, France) Dr. Emmanuel Prouff (Oberthur Card Systems, France) Dr. Michael Rusinowitch (INRIA Lorraine, France) Dr. Luca Spalazzi (Universita' Politecnica delle Marche, Italy) Pr. Pascal Urien (ENST, France) Important Dates: Extended Paper Submission Deadline: --------------------- February 7, 2006 Notification of Acceptance: ----------------------------- February 23, 2006 Registration & Camera-Ready Paper Due: ------------------ March 10, 2006 For information or questions about the workshop and the paper submission procedure, please contact the Workshop organizers. For information or questions about Symposium's paper submission, tutorials, exhibits, demos, panel and special sessions organization, please consult the conference web site at URL: http://www.engr.udayton.edu/faculty/wsmari/cts06/ or contact the symposium co-chairs: Bill McQuay at AFRL/IFSD, WPAFB (William.McQuay@wpafb.af.mil) or Waleed W. Smari at the Dept. of Electrical and Computer Engineering, University of Dayton (Waleed.Smari@notes.udayton.edu). From compa at dist.unige.it Tue Feb 7 14:40:19 2006 From: compa at dist.unige.it (Luca Compagna) Date: Tue Feb 7 14:47:38 2006 Subject: [Avispa-users] Re: exp operator Message-ID: <43E8A343.10700@dist.unige.it> Dear Khaled, sorry for the long silence but apparently your mail has been recognized as a bounce mail by our system. > Dear all, > > Is there any particular problem with the exp operator? > > I?m validating a protocol using the exp operator. The HLPSL > translation seems OK but when using SATMC tool the result is inconclusive. > > Any suggestion? > The exp operator should work fine but only for those tools that support it. SATMC is not one of them. OFMC and CL-atse should support this operator. In case you have any other question do not hesitate to contact us. Ciao, Luca > Thanks in advance > > Best regards > > Khaled > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > Khaled MASMOUDI (PhD student) > > Institut National des T?l?communications > > Wireless Networks and Multimedia Services Department (RS2M) > > Mobility and Security Group > > CNRS UMR SAMOVAR 5157 > > 9, rue Charles Fourier - 91011 Evry Cedex > > Personal Page: www.masmoudi.net > > T?l : +33 1 60 76 42 65 > > Fax : +33 1 60 76 45 78 > > khaled.masmoudi@int-evry.fr > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From khaled.masmoudi at int-evry.fr Tue Feb 7 15:12:08 2006 From: khaled.masmoudi at int-evry.fr (Khaled Masmoudi) Date: Tue Feb 7 15:10:59 2006 Subject: [Avispa-users] RE: exp operator In-Reply-To: <43E8A343.10700@dist.unige.it> Message-ID: <005c01c62bf0$7c1d7ad0$7e679f9d@PAT4876> Dear Luca, Thanks a lot for your reply. It finally worked (so marvelous to see SAFE) with OFMC and CL-atse :) Cheers Khaled -------------------------------------------------------------------------- -- Khaled MASMOUDI (PhD student) Institut National des Télécommunications Wireless Networks and Multimedia Services Department (RS2M) Mobility and Security Group CNRS UMR SAMOVAR 5157 9, rue Charles Fourier - 91011 Evry Cedex Personal Page: www.masmoudi.net Tél : +33 1 60 76 42 65 Fax : +33 1 60 76 45 78 khaled.masmoudi@int-evry.fr -----Message d'origine----- De : Luca Compagna [mailto:compa@dist.unige.it] Envoyé : mardi 7 février 2006 14:40 À : Khaled.Masmoudi@int-evry.fr; AVISPA User Forum Objet : Re: exp operator Dear Khaled, sorry for the long silence but apparently your mail has been recognized as a bounce mail by our system. > Dear all, > > Is there any particular problem with the exp operator? > > I’m validating a protocol using the exp operator. The HLPSL > translation seems OK but when using SATMC tool the result is inconclusive. > > Any suggestion? > The exp operator should work fine but only for those tools that support it. SATMC is not one of them. OFMC and CL-atse should support this operator. In case you have any other question do not hesitate to contact us. Ciao, Luca > Thanks in advance > > Best regards > > Khaled > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > > Khaled MASMOUDI (PhD student) > > Institut National des Télécommunications > > Wireless Networks and Multimedia Services Department (RS2M) > > Mobility and Security Group > > CNRS UMR SAMOVAR 5157 > > 9, rue Charles Fourier - 91011 Evry Cedex > > Personal Page: www.masmoudi.net > > Tél : +33 1 60 76 42 65 > > Fax : +33 1 60 76 45 78 > > khaled.masmoudi@int-evry.fr > > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ begin 666 smime.p7s M,( &"2J&2(;W#0$'`J" ,( "`0$Q"S )!@4K#@,"&@4`,( &"2J&2(;W#0$' M`0``H(((YS""`F\P@@'8H ,"`0("`P_Z#C -!@DJADB&]PT!`00%`#!B,0LP M"08#500&$P):03$E,",&`U4$"A,<5&AA=W1E($-O;G-U;'1I;F<@*%!T>2D@ M3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E9 MH/ G=%O[D_7:A/8T^WSSM4G$-*9SJ10I[[1EA5M52L#FTUOO0@_LC;72.>6! M32&NCA>&I$-.)!W X ]]T?]G`CJ8>IR$R^FT'VO8?AD6"MHDPF M1PBW3S""`RTP@@*6H ,"`0("`0`P#08)*H9(AO<-`0$$!0`P@=$Q"S )!@-5 M! 83`EI!,14P$P8#500($PQ797-T97)N($-A<&4Q$C 0!@-5! <3"4-A<&4@ M5&]W;C$:,!@&`U4$"A,15&AA=W1E($-O;G-U;'1I;F%PTY-C Q,#$P,# P,#!:%PTR,#$R M,S$R,S4Y-3E:,('1,0LP"08#500&$P):03$5,!,&`U4$"!,,5V5S=&5R;B!# M87!E,1(P$ 8#500'$PE#87!E(%1O=VXQ&C 8!@-5! H3$51H87=T92!#;VYS M=6QT:6YG,2@P)@8#500+$Q]#97)T:69I8V%T:6]N(%-EE'V Q1MNIRD;"$ M7GTM#8][$M^%)74H=#I"+&,GGY5[2^]^&8<=ANJCW;G.EF0:PA1N1*Q\YH_H M30]Q'T XI@"CAWCV^92&7JWJP%YVZ]D4HUUN>GP,I4M5?P89*7^>FB;5:KLX M) AJF,>QVJ.8D?UYV^5:Q!RY`@,!``&C$S 1, \&`U4=$P$!_P0%, ,!`?\P M#08)*H9(AO<-`0$$!0`#@8$`Q^R2?D[X]9:E9V(JI/!-$6#0;XU@6&&L)KM2 M-5P(SS#[J$J6BA]B0B.,%P_TNF2<%ZQ'*=^=F%[2;&!Q7**LW'GCYVX`1Q^U M#2CH`IWDFOT3]*;9?+'XW%\C)@F1@'/0%!O>0ZF#)?+FG"\5ROZFJXH'=8L, MW5&$:^3XT2D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E M_0( "9->GIKN?9='%*E2%#T@$?Z>VT3QA!$ >9!ER M8+?[`@,!``&C@90P@9$P$@8#51T3`0'_! @P!@$!_P(!`#!#!@-5'1\$/# Z M,#B@-J TAC)H='1P.B\O8W)L+G1H87=T92YC;VTO5&AA=W1E4&5R,!PQ&C 8 M!@-5! ,3$5!R:79A=&5,86)E;#(M,3,X, T&"2J&2(;W#0$!!04``X&!`$B, MT5"#Z@LNS VC9JQG#W^OK+["%Z%#EI2=?TPAN/@V'ZHMGS8OP/0<4""3<#S] MK>%A8L/9.AE^A+&9&P#%&@N"=)XE4)1BQ]LG<52D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E2D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060208/e2f5012e/attachment.htm From moedersheim at inf.ethz.ch Tue Feb 14 14:35:43 2006 From: moedersheim at inf.ethz.ch (Sebastian Alexander Moedersheim) Date: Tue Feb 14 14:35:37 2006 Subject: [Avispa-users] OFMC --- new version Message-ID: <17393.56495.797340.910689@gargle.gargle.HOWL> Dear AVISPA users and developers, A new version of OFMC has just been released. The most important new feature is that the user can specify a custom algebraic theory modulo which the entire protocol analysis is performed. You can download the new version from http://www.inf.ethz.ch/personal/moedersheim/research/ Kind regards, Sebastian Moedersheim From enis01amor at yahoo.fr Fri Mar 3 20:28:08 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Fri Mar 3 20:27:24 2006 Subject: [Avispa-users] documentation Message-ID: <20060303192808.40159.qmail@web26002.mail.ukl.yahoo.com> hello can you give me documentation . How to specify a protocol in HLPSL I readed the tutorial and user-manual but it's not clear . Especially what i put in the environnement role(): in some exemple we make three session P,S and I,S and P,I P:peer S:server I:intruder and in some exemple we put only two session that are identical P,S and P,S thanks for help --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060303/23e1def5/attachment.htm From paul.drielsma at inf.ethz.ch Mon Mar 6 11:59:40 2006 From: paul.drielsma at inf.ethz.ch (Paul Hankes Drielsma) Date: Mon Mar 6 11:58:49 2006 Subject: [Avispa-users] documentation In-Reply-To: <20060303192808.40159.qmail@web26002.mail.ukl.yahoo.com> References: <20060303192808.40159.qmail@web26002.mail.ukl.yahoo.com> Message-ID: Hello, What sorts of sessions you want depends on the protocol and what sorts of attacks you think the protocol might be vulnerable to. And also what sorts of assumptions you have on your protocol. For instance, in the example you list, the session P,I has the intruder playing the role of the server. Many protocols assume that the server is trusted and not compromised, so if we are working with this assumption then there is no need to analyze a session where the intruder plays the role of the server. (If you do, you may of course find attacks, but they may be trivial.) So if you have an authentication protocol between A and B which you want to analyze for vulnerability to Man-in-the-middle attacks, sessions between (A,B) (A,I) and (I,B) are good bets. Two identical sessions between (A,B) and (A,B) are useful to look for replay-style attacks. I realize this is a bit of a heuristic, but it can be useful to experiment with different analysis scenarios in order to give yourself greater confidence in your protocol. I hope this helps, Paul. On Mar 3, 2006, at 8:28 PM, chikh omar wrote: > hello > can you give me documentation . > How to specify a protocol in HLPSL > I readed the tutorial and user-manual but it's not clear . > Especially what i put in the environnement role(): in some exemple > we make three session P,S and I,S and P,I > P:peer > S:server > I:intruder > > and in some exemple we put only two session that are identical P,S > and P,S > > thanks for help > > > > Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez > les tarifs exceptionnels pour appeler la France et l'international. > T?l?chargez la version beta. > _______________________________________________ > Avispa-users mailing list > Avispa-users@avispa-project.org > http://www.avispa-project.org/mailman/listinfo/avispa-users From kremer at lsv.ens-cachan.fr Wed Mar 15 16:45:19 2006 From: kremer at lsv.ens-cachan.fr (Steve Kremer) Date: Wed Mar 15 16:44:24 2006 Subject: [Avispa-users] ARTIST2 Workshop on Security Specification and Verification of Embedded Systems Message-ID: <4418368F.3090706@lsv.ens-cachan.fr> *** Apologies for multiple copies *** Dear colleague, We wish to invite you to participate to the ARTIST-2 informal workshop on security of embedded systems. ARTIST-2 is a European Network of Excellence on Embedded Systems Design (http://www.artist-embedded.org/FP6/). The workshop will focus on the formal specification and verification of security properties, and in particular on the specification and formal verification of security protocols. Topics include, but are not limited to: * formal definition and verification of security properties * formal analysis and design of cryptographic protocols * modeling information flow * formal techniques for (mobile) code security; * security in real-time/probabilistic systems; * language-based security; * theory and application of policy languages and trust management One of the goals of the workshop is to bring together the part of the Artist2 community working on security, nevertheless, the workshop is open to anyone. The program of the workshop will include invited talks, regular talks and plenty of time for discussion. We expect to include both short (~10-20 minutes) and long (~40-50 minutes) talks. The workshop will take place at Pisa, Tuscany, Italy on May 18th and will be co-located with iTrust2006 (http://www.iit.cnr.it/iTrust2006/). If you are interested in giving a talk, please send an email before April 7 to artist2-sw@iit.cnr.it indicating a title, a short abstract (one or two paragraphs) and whether you intend to give a long or a short talk. The participation to the workshop is free but registration is mandatory. Updated information will be accessible at the workshop website: http://www.artist-embedded.org/FP6/ARTIST2Events/Events/Security-Pisa/ The organizing committee Bruno Bouyssounouse Sandro Etalle Steve Kremer Yassine Lakhnech Fabio Martinelli Marinella Petrocchi From mmannan at gmail.com Thu Mar 16 20:18:56 2006 From: mmannan at gmail.com (Mohammad Mannan) Date: Thu Mar 16 20:17:57 2006 Subject: [Avispa-users] password protocol and parameter passing Message-ID: <96f6d49f0603161118qb88c90fmf11ae580b387cef0@mail.gmail.com> Hi List -- 1. Could someone point to more AVISPA examples on password-based protocols (in addition to SRP, EKE, SPEKE available in the current distribution)? 2. What are the differences between a parameter declared in a "role" and inside a role as a "local" variable? Thanks for your time. -- Mohammad Mannan http://www.scs.carleton.ca/~mmannan From Laurent.Vigneron at Loria.Fr Tue Mar 21 09:24:24 2006 From: Laurent.Vigneron at Loria.Fr (Laurent Vigneron) Date: Tue Mar 21 09:23:21 2006 Subject: [Avispa-users] password protocol and parameter passing Message-ID: <17439.47160.116092.925462@valhey.loria.fr> Hi Mohammad, > 2. What are the differences between a parameter declared in a "role" > and inside a role as a "local" variable? This is exactly the same difference as between a parameter and a local variable in the declaration of a function: a parameter is an information comming from the outside; it is instantiated when the role is called; a local variable belongs only to the role where it is defined, and it may not have an initial value. Laurent. From enis01amor at yahoo.fr Thu Mar 30 10:39:17 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Thu Mar 30 10:37:57 2006 Subject: [Avispa-users] arguments pour choisir AVISPA Message-ID: <20060330083917.8557.qmail@web26002.mail.ukl.yahoo.com> Bonjour, Quelles sont les arguments qui peut convaincre les validateurs de choisir AVISPA comme outils de validation formelle et non pas un autre outils comme CASPER ou EVA ...? y a t-il de documentation qui explique les arguments de choisir AVISPA. ? Cordialement Omar --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060330/27ea3664/attachment.htm From zrelli at jaist.ac.jp Thu Mar 30 10:44:06 2006 From: zrelli at jaist.ac.jp (Saber Zrelli) Date: Thu Mar 30 10:42:52 2006 Subject: [Avispa-users] about 'secrecy' statement and Kerberos Message-ID: <20060330084406.GA10101@mlserv.jaist.ac.jp> Hi, In the user-manual (p.26 guidelines about secrecy goal specification) , it is said that "If a value T that should be kept secret is determined by a single role (in particular, if it is an atomic value like a nonce produced by new()), then the secrecy statement should be given in -- and only in -- the role introducing the value". In case of Kerberos, the TGS session key (the key that will be shared between a client and the TGS) is generated by the AS, hence the secrecy statement related to TGS sessoin should be present only on the AS role. However, in the example "Kerbers-basic" provided in the "The AVISPA Library of protocols" the secrecy statement of TGS session key is present in the AS, TGS and the client. So, I guess that one of the following is true : - I did not understood what is said in the HLPSL guidelines - There is a mistake in the HLPSL specification of Kerberos-basic I would appreciate any clarifications, Regards, Saber. From ug85bas at cs.bham.ac.uk Thu Mar 30 10:57:19 2006 From: ug85bas at cs.bham.ac.uk (Ben Smyth) Date: Thu Mar 30 10:55:52 2006 Subject: [Avispa-users] arguments pour choisir AVISPA In-Reply-To: <20060330083917.8557.qmail@web26002.mail.ukl.yahoo.com> References: <20060330083917.8557.qmail@web26002.mail.ukl.yahoo.com> Message-ID: <442B9D6F.2010309@cs.bham.ac.uk> Bonjour, My french is no good, so I will try to write in basic English. You need to use the best tool (program) for the job (task). I could not find anything about CASPER or EVA, do you have the web address? Here is my argument for using ProVerif in favour of AVISPA and CAPSL. My goals are: prove that a state is unreachable (secrecy) and demonstrate privacy using observational equivalence. I need to be able to define equations. (this is taken straight from my dissertation, so probably isn't basic english. Its in LaTeX format) CAPSL is unsuitable since it can only model authentication and key-exchange. Similarly AVISPA supports only authentication and secrecy. Although in theory it is possible to define one's own rules using AVISPA's Intermediate Format (IF) language~\cite{AVISPA03} - which would permit the modeling of further requirements - in reality such usage is unsupported\footnotemark. ProVerif permits the verification of privacy using observational equivalence. However, its ability is not complete and thus it is commonly necessary to complete a proof by hand. Although not perfect ProVerif is the only tool which meets the demands of the analysis. \footnotetext{Sebastian M\"{o}dersheim has since made claims that AVISPA's \emph{On-the-Fly Model-Checker} (OFMC) back-end is now capable (February, 2006) of handling user defined algebraic expressions. At the time of analysis support was classified as beta and it was therefore decided to utilise a tool which is known to provide the necessary functionality.} au revior, Ben chikh omar wrote: > Bonjour, > > Quelles sont les arguments qui peut convaincre les validateurs de choisir AVISPA comme outils de validation formelle et non pas un autre outils comme CASPER ou EVA ...? > > y a t-il de documentation qui explique les arguments de choisir AVISPA. ? > > Cordialement > Omar > > > --------------------------------- > Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. > > > ------------------------------------------------------------------------ > > _______________________________________________ > Avispa-users mailing list > Avispa-users@avispa-project.org > http://www.avispa-project.org/mailman/listinfo/avispa-users From enis01amor at yahoo.fr Tue Apr 4 10:13:47 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Tue Apr 4 10:12:23 2006 Subject: [Avispa-users] question Message-ID: <20060404081347.25823.qmail@web26006.mail.ukl.yahoo.com> pourquoi vous ?crivez PRF(K.na.nb) et non PRF(K, na.nb)? en fait vous utilisez les deux notations ce qui rend les choses ambigu?: dans eap-AKA: AT_MAC1? = HMAC(PRF_SHA1(NAI,IK?,CK?),AT_RAND?.AT_AUTN?) (avec virgule) Bonjour, Est ce que quelqu'un peut m'?clairsir les choses suivantes. dans eap-archie : il faut verifier que mic recu egale au mic calcul? localement. quand on d?clare la propri?te secret (key...) ? dans un seul role suffit ou bien a chaque fois qu'on utilise ? quelle sont les propri?t?s qu?on peut v?rifier avec AVISPA et comment ? (par quellle primitives) Cordialement Cheikhrouhou Omar --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/024f6b05/attachment.htm From hichemest9 at yahoo.fr Tue Apr 4 10:37:59 2006 From: hichemest9 at yahoo.fr (HICHEM KILENI) Date: Tue Apr 4 10:36:32 2006 Subject: [Avispa-users] message Message-ID: <20060404083759.40533.qmail@web26209.mail.ukl.yahoo.com> bonjour, tu peux m' envoyer le simulateur spin. merci --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/8cfdfc50/attachment.htm From enis01amor at yahoo.fr Tue Apr 4 10:38:08 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Tue Apr 4 10:36:40 2006 Subject: [Avispa-users] =?iso-8859-1?q?there_is_ambiquit=E9?= Message-ID: <20060404083809.6505.qmail@web26001.mail.ukl.yahoo.com> Skipped content of type multipart/alternative-------------- next part -------------- A non-text attachment was scrubbed... Name: There is ambigu?t? in the EAP_archie.zip Type: application/x-zip-compressed Size: 7092 bytes Desc: 1521434262-There is ambigu?t? in the EAP_archie.zip Url : http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/95fd382e/ThereisambigutintheEAP_archie.bin From enis01amor at yahoo.fr Tue Apr 4 10:50:53 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Tue Apr 4 10:49:24 2006 Subject: [Avispa-users] general comments Message-ID: <20060404085053.89711.qmail@web26014.mail.ukl.yahoo.com> Hello, there is 3 months that i was reading and learning about the avispa tools and i have some suggestion to ameliorate the comprehension of such tools. *i is very helpful if each authors (of specification ) add comments in his specification to help undestanding. in fact there is some ambiguit? in protocole like EAP protocole. *if possible authors let there contact (email) to can contact them and discuss about their idea of sp?cification Thanks for help Omar Cheikhrouhou Engineer & Researcher @ ReDCAD Research in Development and Control of Distributed Applications University of Sfax, National School of Engineers BP W, Sfax, 3038, Tunisia Tel: +216 21 17 96 17 Email : enis01amor@yahoo.fr --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez les tarifs exceptionnels pour appeler la France et l'international.T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/7dcd0bce/attachment.htm From enis01amor at yahoo.fr Tue Apr 4 11:02:20 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Tue Apr 4 11:00:53 2006 Subject: [Avispa-users] question about the specification of EAP-AKA Message-ID: <20060404090220.42264.qmail@web26005.mail.ukl.yahoo.com> hello, in the sp?cification of EAP-AKa , role peer, state=2, in order to verify the validity of the AT_MAC field received from server , normally the peer must calculate first the value of key IK and CK for this we must use := and not = we must write IK:= F3(...) CK:=F4(...) i am wrong? also when i have changed (=) by (:=) , the avispa tool generate error ??? why? thanks for help Omar Cheikhrouhou Engineer & Researcher @ ReDCAD Research in Development and Control of Distributed Applications University of Sfax, National School of Engineers BP W, Sfax, 3038, Tunisia Tel: +216 21 17 96 17 Email : enis01amor@yahoo.fr --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger. Appelez le monde entier ? partir de 0,012 ?/minute ! T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/65ed0d64/attachment.htm From enis01amor at yahoo.fr Tue Apr 4 11:26:36 2006 From: enis01amor at yahoo.fr (chikh omar) Date: Tue Apr 4 11:25:10 2006 Subject: [Avispa-users] about witness et request Message-ID: <20060404092636.79475.qmail@web26012.mail.ukl.yahoo.com> hello, i wish to understant the two primitives request and witness: * which property they verify ? *they only can verify mutual authentication ? if yes why in EAP-AKA we use AT_MAC and AT_AUTH for authentication ??? thanks for help Omar Cheikhrouhou Engineer & Researcher @ ReDCAD Research in Development and Control of Distributed Applications University of Sfax, National School of Engineers BP W, Sfax, 3038, Tunisia Tel: +216 21 17 96 17 Email : enis01amor@yahoo.fr --------------------------------- Nouveau : t?l?phonez moins cher avec Yahoo! Messenger. Appelez le monde entier ? partir de 0,012 ?/minute ! T?l?chargez la version beta. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060404/3a0cc969/attachment-0001.htm From David.von.Oheimb at siemens.com Tue Apr 4 11:47:27 2006 From: David.von.Oheimb at siemens.com (David von Oheimb) Date: Tue Apr 4 11:46:01 2006 Subject: [Avispa-users] about 'secrecy' statement and Kerberos In-Reply-To: <20060330084406.GA10101@mlserv.jaist.ac.jp> References: <20060330084406.GA10101@mlserv.jaist.ac.jp> Message-ID: <443240AF.7020801@siemens.com> Hi Saber, > In the user-manual (p.26 guidelines about secrecy goal specification) > , it is said that "If a value T that should be kept secret is > determined by a single role (in particular, if it is an atomic value > like a nonce produced by new()), then the secrecy statement should > be given in -- and only in -- the role introducing the value". > > In case of Kerberos, the TGS session key (the key that will be > shared between a client and the TGS) is generated by the AS, > hence the secrecy statement related to TGS sessoin should be present > only on the AS role. > > However, in the example "Kerbers-basic" provided in the "The AVISPA > Library of protocols" the secrecy statement of TGS session key is > present in the AS, TGS and the client. > > > So, I guess that one of the following is true : > > - I did not understood what is said in the HLPSL guidelines > - There is a mistake in the HLPSL specification of Kerberos-basic I'm not the author of the Kerberos specs, but did some updates on them last year. I think that the extra secrecy statements in Kerb-* are still there for historical reasons and should be removed. Regards, David +------------------------------------------------------------------<><-+ | Dr. David von Oheimb Senior Research Scientist | | Siemens AG - CT IC 3 Phone: +49 89 636 41173 | | Otto-Hahn-Ring 6 Fax : +49 89 636 48000 | | D-81730 M?nchen, Germany EMail: David.von.Oheimb@siemens.com | | http://scd.siemens.de/db4/lookUp?tcgid=Z000ECRO http://ddvo.net/ | +----------------------------------------------------------------------+ From Thomas.Genet at irisa.fr Tue Apr 4 12:03:36 2006 From: Thomas.Genet at irisa.fr (Thomas Genet) Date: Tue Apr 4 12:04:42 2006 Subject: [Avispa-users] HLSPL protocol Animator and Graphical Interface for AVISPA Message-ID: <44324478.5010403@irisa.fr> Hi to all avispa users, Here in IRISA, we are currently developping an animation tool to ease the design of HLPSL specifications. From an HLPSL specification, it is possible to interactively produce a Message Sequence Chart (MSC) corresponding to an execution of the specification. Here are some features: 1) When the protocol is non-deterministic or several sessions are runned in parallel, choices are proposed to the user in order to select a particular execution. 2) It is possible to go back in the execution 3) Save, run again MSCs 4) Hide/show content of variables of roles The tool also contains a graphical interface equivalent to the web interface of AVISPA but which permits a local use. The tool is currently under development but is already usable. When the development will be completed, the tool will be distributed under an open source licence. For the moment, if someone is interested in early testing of a binary version (linux and Tk) of this tool, please mail me (thomas.genet@irisa.fr) or the main developper (yann.glouche@irisa.fr). Yann and I hope this will help in the tuning of HLPSL specification, Best regards, Thomas -- Thomas Genet - IFSIC/IRISA Campus de Beaulieu, 35042 Rennes cedex, France T?l: +33 (0) 2 99 84 73 44 E-mail: genet@irisa.fr http://www.irisa.fr/lande/genet From paul.drielsma at inf.ethz.ch Tue Apr 4 12:06:23 2006 From: paul.drielsma at inf.ethz.ch (Paul Hankes Drielsma) Date: Tue Apr 4 12:04:55 2006 Subject: [Avispa-users] about witness et request In-Reply-To: <20060404092636.79475.qmail@web26012.mail.ukl.yahoo.com> References: <20060404092636.79475.qmail@web26012.mail.ukl.yahoo.com> Message-ID: <344C331F-B459-4665-A214-8BC6FBB05423@inf.ethz.ch> Hi Omar, They verify authentication. One pair of witness/request serves for unilateral authentication, if you want mutual then you need to define two pairs. I wrote an email with an analogy of witness/request facts answering a similar question a while back. Maybe it will be of some help. ---------------------------------------- witness and request events are kinda complicated, but they work and they are actually reasonably powerful. Here's the deal: let's say you and me are sitting in our houses down the street from each other executing NSPK. You're Alice and I'm Bob. You create for me some random nonce called Na and send it to me in a letter. When you do this, you raise a little red flag that indicates what the random value for Na was, let's say 17. So at your house you fly a red flag that says "Marie's value for Paul, which is called Na, is 17." In AVISPA, we call these flags witness facts. So in NSPK, the fact witness(A,B,bob_alice_na,Na') that Alice emits in the example on the web means "My name is A, and I created the value Na' for the guy named B. I created it for the purpose called bob_alice_na." The purpose is just a name and could be anything, but it ensures that the intruder can't do any funny stuff like take a value that you intended as your nonce Na, and inject it someplace else where I want you to send me, for example, your public key. Ok, so that's you. Now over at my place I'm Bob. I get a letter from you. It's got what is supposedly your nonce in it and your name, encrypted for me. Then at the end of the protocol, you have sent me back my Nb and that's supposed to prove to me that it's really you, right? So what I do after I get that last message is I fly a little blue flag at my house that indicates what I believe your value for Na was. So my flag says "I'm Paul, and the value for Na that I believe I got from Marie, is 17." This, in AVISPA, is done with a request flag. In NSPK, in the Bob role we have request(B,A,bob_alice_na,Na) and this says "I'm B, I believe I'm talking to A and she sent me the value Na for the purpose bob_alice_na." So far so good? I hope so. So where's the intruder? The intruder is the mailman. He's carrying the letters between our two houses, and he can open 'em, read 'em, and replace them with his own letters if he wants. The only thing he can't do is decrypt stuff when he doesn't have the key. ALSO, he can't climb on top of our houses and replace the flags. So when you fly your red flag and I fly my blue one, he can't screw around with those or take them down. Almost finished I promise. So where's the AVISPA Tool? The AVISPA Tool is a guy across the street with binoculars. His job is to look our for flags and make sure they match in a particular way. What way? Well, for authentication what he looks for is this: if he EVER sees a blue flag go up (Bob's flag), then there MUST be a red flag someplace with the same people, the same purpose, and the same value. So if my flag says I believe the value 17 came from you, your flag must say you created the value 17 for me for the same purpose. And if you have replay protection (i.e. request and not wrequest), then those flags better be unique. If I fly two blue flags that look the same, there better be two red flags on your house. Otherwise it means the intruder, the mailman, photocopied your letters and is delivering them to me again (maybe even after you moved away!). That's how witness and request events work. The AVISPA Tool looks for situations in which they see the first request flag above, and make sure that when it comes there is a matching witness that looks like the one above. If not, it's an attack. Who decides the goals? That's one of the challenges of modelling protocols. Generally, we try to extract them from the description of the protocol that's in an RFC or something. They are sometimes intuitively clear: if two people exchange a key for instance, it's reasonable to assume that good goals include that the key should be secret and they should agree upon its value, so it should be authenticated. ---------------------------------------- Cheers, Paul. On Apr 4, 2006, at 11:26 AM, chikh omar wrote: > hello, > > i wish to understant the two primitives request and witness: > * which property they verify ? > *they only can verify mutual authentication ? if yes why in EAP-AKA > we use AT_MAC and AT_AUTH for authentication ??? > > thanks for help > > > > > > > > Omar Cheikhrouhou > Engineer & Researcher @ ReDCAD > Research in Development and Control of Distributed Applications > University of Sfax, National School of Engineers > BP W, Sfax, 3038, Tunisia > Tel: +216 21 17 96 17 > Email : enis01amor@yahoo.fr > > Nouveau : t?l?phonez moins cher avec Yahoo! Messenger. Appelez le > monde entier ? partir de 0,012 ?/minute ! T?l?chargez la version beta. > _______________________________________________ > Avispa-users mailing list > Avispa-users@avispa-project.org > http://www.avispa-project.org/mailman/listinfo/avispa-users From paul.drielsma at inf.ethz.ch Tue Apr 4 12:07:48 2006 From: paul.drielsma at inf.ethz.ch (Paul Hankes Drielsma) Date: Tue Apr 4 12:06:18 2006 Subject: [Avispa-users] message In-Reply-To: <20060404083759.40533.qmail@web26209.mail.ukl.yahoo.com> References: <20060404083759.40533.qmail@web26209.mail.ukl.yahoo.com> Message-ID: Hello Hichem, This is really not what we work on so we can't answer questions about SPIN, but you can look here: http://spinroot.com/spin/whatispin.html Paul On Apr 4, 2006, at 10:37 AM, HICHEM KILENI wrote: > bonjour, tu peux m' envoyer le simulateur spin. merci > > Nouveau : t?l?phonez moins cher avec Yahoo! Messenger ! D?couvez > les tarifs exceptionnels pour appeler la France et l'international. > T?l?chargez la version beta. > _______________________________________________ > Avispa-users mailing list > Avispa-users@avispa-project.org > http://www.avispa-project.org/mailman/listinfo/avispa-users From ychevali at irit.fr Wed Apr 5 16:35:03 2006 From: ychevali at irit.fr (Yannick CHEVALIER) Date: Wed Apr 5 16:33:34 2006 Subject: [Avispa-users] announcement In-Reply-To: References: <20060404083759.40533.qmail@web26209.mail.ukl.yahoo.com> Message-ID: <4433D597.8000902@irit.fr> Hi all, just a small message to advertize the issue of an update for the xemacs mode. It will be available in the next avispa tool release, but you can download it now from: http://www.irit.fr/recherches/LILAC/Pers/Chevalier/ among other things.. key sequence+space inserts ":a" ": agent," ":ch" ": channel (dy)," ":f" ": function," ":m" ": message," ":n" ": nat," ":pi" ": protocol_id," ":pk" ": public_key," nil 2 ":sk" ": symmetric_key," ":t" ": text," plus: * ":enc" prompts to insert an encrypted message plus * no pretty-printing yet, but some auto-indentation stuff, insert of patterns (e.g. b_r and c_r for respectively basic and composition roles) Any feedback, especially before the tool release, welcomed ! Cheers, Yannick Chevalier From armando at armandobook.mrg.dist.unige.it Thu Apr 6 10:24:37 2006 From: armando at armandobook.mrg.dist.unige.it (Alessandro Armando) Date: Thu Apr 6 10:23:12 2006 Subject: [Avispa-users] HLSPL protocol Animator and Graphical Interface for AVISPA In-Reply-To: Your message of "Tue, 04 Apr 2006 12:03:36 +0200." <44324478.5010403@irisa.fr> Message-ID: <20060406082442.2BF841E72F4@armandobook.mrg.dist.unige.it> Hi Thomas, > Here in IRISA, we are currently developping an animation tool to ease > the design of HLPSL specifications. From an HLPSL specification, it is > possible to interactively produce a Message Sequence Chart (MSC) > corresponding to an execution of the specification. Here are some > features: > > 1) When the protocol is non-deterministic or several sessions are > runned in parallel, choices are proposed to the user in order to > select a particular execution. > > 2) It is possible to go back in the execution > > 3) Save, run again MSCs > > 4) Hide/show content of variables of roles > > > The tool also contains a graphical interface equivalent to the web > interface of AVISPA but which permits a local use. The tool is > currently under development but is already usable. When the > development will be completed, the tool will be distributed under an > open source licence. Great! The tool your are developing is very interesting and has many interesting features that are currently missing in the AVISPA Tool. So the your activity is very welcomed! > For the moment, if someone is interested in early testing of a binary > version (linux and Tk) of this tool, please mail me > (thomas.genet@irisa.fr) or the main developper (yann.glouche@irisa.fr). I'd be interested. Could you please send me a copy (or instruction on how to get it)? Best Regards, alessandro -- Alessandro Armando e-mail: armando@dist.unige.it Artificial Intelligence Laboratory http://www.ai.dist.unige.it/armando DIST - Universita' di Genova, phone: +39-0103532216 viale Causa 13, fax: +39-0103532948 16145 GENOVA, ITALY mobile: +39-3281003201 From Michael.Rusinowitch at loria.fr Fri Apr 7 08:48:40 2006 From: Michael.Rusinowitch at loria.fr (Michael Rusinowitch) Date: Fri Apr 7 08:47:18 2006 Subject: [Avispa-users] arguments pour choisir AVISPA Message-ID: <44360B48.90109@loria> Dear Ben - HLPSL/IF have a large expressiveness, basically we can formulate all kinds of distributed systems and also custom goals - There are quite different back-ends connected to AVISPA, allowing us to perform verification both for a small number of sessions of complicated protocols and goals, and (like ProVerif) an unbounded number of sessions for simple protocols and secrecy. - Cl-AtSe and OFMC avispa back ends can handle algebraic properties, as Cl-AtSe has efficient implementations for the most popular properties, and OFMC allows the user to even specify his custom algebraic theory. This helps when modelling new cryptographic primitives or abstracting away details of the protocol. - also i dont understand the connection you made in your mail between the limitations on properties like authentication and secrecy and the algebraic expressions; note also that since ProveriF is based on applied pi calculus it may need more equational presentations (e.g. for standard encryption/decryption) where for avispa it is built-in; i am not completely sure about that but it might be the source of the confusion. - maybe it would be useful for all if you show samples of the equational properties you need to model , so that we can compare the different techniques best regards michael %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Ben Smyth ug85bas at cs.bham.ac.uk Thu Mar 30 10:57:19 CEST 2006 * Previous message: [Avispa-users] arguments pour choisir AVISPA * Next message: [Avispa-users] about 'secrecy' statement and Kerberos Bonjour, My french is no good, so I will try to write in basic English. You need to use the best tool (program) for the job (task). I could not find anything about CASPER or EVA, do you have the web address? Here is my argument for using ProVerif in favour of AVISPA and CAPSL. My goals are: prove that a state is unreachable (secrecy) and demonstrate privacy using observational equivalence. I need to be able to define equations. (this is taken straight from my dissertation, so probably isn't basic english. Its in LaTeX format) CAPSL is unsuitable since it can only model authentication and key-exchange. Similarly AVISPA supports only authentication and secrecy. Although in theory it is possible to define one's own rules using AVISPA's Intermediate Format (IF) language~\cite{AVISPA03} - which would permit the modeling of further requirements - in reality such usage is unsupported\footnotemark. ProVerif permits the verification of privacy using observational equivalence. However, its ability is not complete and thus it is commonly necessary to complete a proof by hand. Although not perfect ProVerif is the only tool which meets the demands of the analysis. \footnotetext{Sebastian M\"{o}dersheim has since made claims that AVISPA's \emph{On-the-Fly Model-Checker} (OFMC) back-end is now capable (February, 2006) of handling user defined algebraic expressions. At the time of analysis support was classified as beta and it was therefore decided to utilise a tool which is known to provide the necessary functionality.} au revior, Ben From ug85bas at cs.bham.ac.uk Mon Apr 10 12:49:56 2006 From: ug85bas at cs.bham.ac.uk (Ben Smyth) Date: Mon Apr 10 12:47:50 2006 Subject: [Avispa-users] arguments pour choisir AVISPA In-Reply-To: <44360B48.90109@loria> References: <44360B48.90109@loria> Message-ID: <443A3854.7080606@cs.bham.ac.uk> Dear Michael, I would be more than happy to share my views. Feel free to ask any questions. I first used AVISPA during September 2005 at which point I believe it was unable to model any algebraic properties. I can't recall the precise construct I was modeling at the time - but it was related to the CRS'05 electronic voting protocol. Claims have since been made (February, 2006) via this mailing list that user defined equations are compatible with OFMC. At present I haven't had the time to confirm this claim for myself. I will do so at some point in the future. Having re-read my previous comments, I can see how I've caused confusion! They were written in note form (which are pretty difficult to read for anyone else). My key point are: * AVISPA cannot model observational equivalence - to the best of my knowledge. * AVISPA was previously (before Feb 2006) unable to model user defined equations. For this reason I chose ProVerif as opposed to AVISPA. The inability to define ones own equation was the biggest flaw and has (apparently - I need to confirm for myself) now been incorporated into OFMC. To give a taste for the equations I have been modelling here's a basic example: R_0^r_f_0 R_1^r_f_1 S^r_v' = U^-c R_0^s_f_0 R_1^s_f_1 S^s_v' Where U = R_0^f_0 R_1^f_1 S^v', s_f_0 = r_f_0 + c*f_0, s_f_1 = r_f_1 + c*f_1 and s_v' = r_v' + c*v' To witness this fact we must realise: R_0^r_f_0 R_1^r_f_1 S^r_v' = R_0^(-c*f_0) R_1^(-c*f_1) S^(-c*v') R_0^s_f_0 R_1^s_f_1 S^s_v' As I have said, it may now be possible to model this in AVISPA. Regards, Ben CRS'05 Chaum, Ryan and Schneider (2005) Pret a voter. Michael Rusinowitch wrote: > Dear Ben > > - HLPSL/IF have a large expressiveness, basically we can formulate all > kinds of distributed systems and also custom goals > > - There are quite different back-ends connected to AVISPA, allowing us > to perform verification both for a small number of sessions of > complicated protocols and goals, and (like ProVerif) an unbounded > number of sessions for simple protocols and secrecy. > > - Cl-AtSe and OFMC avispa back ends can handle algebraic properties, as > Cl-AtSe has efficient implementations for the most popular properties, > and OFMC allows the user to even specify his custom algebraic theory. > This helps when modelling new cryptographic primitives or abstracting > away details of the protocol. > > - also i dont understand the connection you made in your mail > between the limitations on properties like > authentication and secrecy and the algebraic expressions; > note also that since ProveriF is based on applied pi > calculus it may need more equational presentations > (e.g. for standard encryption/decryption) where for avispa it is > built-in; i am not completely sure about that but it might be the source > of the confusion. > > - maybe it would be useful for all if you show samples of the > equational properties you need to model , so that we can compare the > different techniques > > best regards > > michael > > > > %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% > Ben Smyth ug85bas at cs.bham.ac.uk > Thu Mar 30 10:57:19 CEST 2006 > > * Previous message: [Avispa-users] arguments pour choisir AVISPA > * Next message: [Avispa-users] about 'secrecy' statement and Kerberos > > > Bonjour, > > My french is no good, so I will try to write in basic English. > > You need to use the best tool (program) for the job (task). I could not > find anything about CASPER or EVA, do you have the web address? > > Here is my argument for using ProVerif in favour of AVISPA and CAPSL. My > goals are: prove that a state is unreachable (secrecy) and demonstrate > privacy using observational equivalence. I need to be able to define > equations. (this is taken straight from my dissertation, so probably > isn't basic english. Its in LaTeX format) > > CAPSL is unsuitable since it can only model authentication and > key-exchange. Similarly AVISPA supports only authentication and secrecy. > Although in theory it is possible to define one's own rules using > AVISPA's Intermediate Format (IF) language~\cite{AVISPA03} - which would > permit the modeling of further requirements - in reality such usage is > unsupported\footnotemark. ProVerif permits the verification of privacy > using observational equivalence. However, its ability is not complete > and thus it is commonly necessary to complete a proof by hand. Although > not perfect ProVerif is the only tool which meets the demands of the > analysis. > > \footnotetext{Sebastian M\"{o}dersheim has since made claims that > AVISPA's \emph{On-the-Fly Model-Checker} (OFMC) back-end is now capable > (February, 2006) of handling user defined algebraic expressions. At the > time of analysis support was classified as beta and it was therefore > decided to utilise a tool which is known to provide the necessary > functionality.} > > > au revior, > > Ben > > > > From vigano at inf.ethz.ch Tue Apr 11 15:36:19 2006 From: vigano at inf.ethz.ch (vigano@inf.ethz.ch) Date: Tue Apr 11 15:34:44 2006 Subject: [Avispa-users] 2nd CFP: FCS-ARSPA'06 (Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis) Message-ID: <20060411133619.GA24616@inf.ethz.ch> apologies for multiple copies ****************************************** *** NEW: post-workshop Special Issue *** *** of Information and Computatation *** ****************************************** ************************ **** **** **** FCS-ARSPA'06 **** **** **** ************************ A LICS'06 (and FLoC'06) Affiliated Workshop on FOUNDATIONS OF COMPUTER SECURITY and AUTOMATED REASONING FOR SECURITY PROTOCOL ANALYSIS Seattle, Washington, August 15-16, 2006 http://www.inf.ethz.ch/~vigano/fcs-arspa06 *********************** *** CALL FOR PAPERS *** *********************** Submission deadline: May 10, 2006 BACKGROUND, AIM AND SCOPE ========================= Computer security is an established field of computer science of both theoretical and practical significance. In recent years, there has been increasing interest in logic-based foundations for various methods in computer security, including the formal specification, analysis and design of security protocols and their applications, the formal definition of various aspects of security such as access control mechanisms, mobile code security and denial-of-service attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis. The workshop FCS-ARSPA'06 is the fusion of two workshops. The workshop FCS continues a tradition, initiated with the Workshops on Formal Methods and Security Protocols (FMSP) in 1998 and 1999, then with the Workshop on Formal Methods and Computer Security (FMCS) in 2000, and finally with the LICS satellite Workshop on Foundations of Computer Security (FCS) in 2002 through 2005, of bringing together formal methods and the security community. The ARSPA workshop is the third in a series of workshops on Automated Reasoning for Security Protocol Analysis, bringing together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. The first two ARSPA workshops were held as satellite events of IJCAR'04 and of ICALP'05, respectively. The aim of the joint workshop FCS-ARSPA'06 is to provide a forum for continued activity in these areas, to bring computer security researchers in closer contact with the LICS community, and to give LICS attendees an opportunity to talk to experts in computer security. We thus solicit submissions of papers both on mature work and on work in progress. We are interested both in new results in theories of computer security and also in more exploratory presentations that examine open questions and raise fundamental concerns about existing theories, as well as in new results on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. Possible topics include, but are not limited to: Automated reasoning techniques Access control and resource usage control Composition issues Authentication Formal specification Availability and denial of service Foundations of verification Covert channels Information flow analysis Confidentiality Language-based security Integrity and privacy Logic-based design for Intrusion detection Program transformation Malicious code Security models Mobile code Static analysis Mutual distrust Statistical methods Privacy Tools Security policies Trust management Security protocols All submissions will be peer-reviewed. Authors of accepted papers must guarantee that their paper will be presented at the workshop. SUBMISSION ========== Submissions should be at most 15 pages (a4paper, 11pt), including references, in the Springer LNCS style available at the URL http://www.springer.de/comp/lncs/authors.html The cover page should include title, names of authors, co-ordinates of the corresponding author, an abstract, and a list of keywords. It is recommended that submissions adhere to the specified format and length. Submissions that are clearly too long may be rejected immediately. Additional material intended for the referees but not for publication in the final version - for example details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. Simultaneous submissions to a journal or another conference are accepted. Authors are invited to submit their papers electronically, as portable document format (pdf) or postscript (ps); please, do not send files formatted for work processing packages (e.g., Microsoft Word or Wordperfect files). The only mechanism for paper submissions is via the electronic submission web-site (which will soon be available). IMPORTANT DATES =============== Papers due: May 10, 2006 Notification of acceptance: June 16, 2006 Final paper versions due: July 14, 2006 Workshop: August 15-16, 2006 PUBLICATION =========== Informal proceedings will be made available in electronic format and they will be distributed to all participants of the workshop. Moreover, workshop participants will be invited to submit full versions of their papers to a special issue of Information and Computation, which will be open also to non-participants, in all cases with fresh reviewing. INVITED TALKS ============= To be announced PROGRAM COMMITTEE ================= * Alessandro Armando (Universita` di Genova, Italy) * Jorge R. Cuellar (SIEMENS AG, Munich, Germany) * Anupam Datta (Stanford University, USA) * Pierpaolo Degano (Universita` di Pisa, Italy; co-chair) * Pablo Giambiagi (Swedish Institute of Computer Science, Sweden) * Virgil Gligor (University of Maryland, USA) * Roberto Gorrieri (Universita` di Bologna, Italy) * Carl A. Gunter (University of Illinois at Urbana-Champaign, USA) * Joshua Guttman (Mitre, USA) * Ralf Kuesters (Christian-Albrechts-Universitaet zu Kiel, Germany; co-chair) * Ninghui Li (Purdue University, USA) * Sjouke Mauw (University of Eindhoven, The Netherlands) * Peter Ryan (University of Newcastle, UK) * Luca Vigano` (ETH Zurich, Switzerland; co-chair) * Laurent Vigneron (INRIA-LORRAINE, Nancy, France) * Bogdan Warinschi (INRIA-LORRAINE, Nancy, France) * Steve Zdancewic (University of Pennsylvania, USA; co-chair) FCS Steering Committee: * Martin Abadi (University of California at Santa Cruz, USA) * Joshua Guttman (MITRE, USA) * John Mitchell (Stanford University, USA) * Andrei Sabelfeld (Chalmers, Sweden; chair) * Andre Scedrov (University of Pennsylvania, USA) ADDITIONAL INFORMATION ====================== Information about registration, travel, and venue can be found at the LICS'06 and FLoC'06 web-sites. For further information send an email to the workshop co-chairs at fcs-arspa06 -at- lists.inf.ethz.ch From n1k1ta_ at mail.ru Wed Apr 12 22:53:18 2006 From: n1k1ta_ at mail.ru (=?koi8-r?Q?=EE=C9=CB=C9=D4=C1=20=EC=C5=CF=CE=D4=D8=C5=D7?=) Date: Wed Apr 12 22:51:46 2006 Subject: [Avispa-users] Re: Avispa-users Digest, Vol 7, Issue 2 In-Reply-To: <20060410104749.F2FF76F80A@carroll.ai.dist.unige.it> Message-ID: hello all, i wish to understant the IKEv2 specification can you help me with oakley(aggresive, conservative mode) specification what goals should be used? only secrecy_of a_sk and authentification_on sk? thanks for help From kemm16 at hotmail.com Mon Apr 17 19:01:27 2006 From: kemm16 at hotmail.com (Kamal-Eldin Mohamed) Date: Mon Apr 17 18:59:45 2006 Subject: [Avispa-users] Error Message Message-ID: An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060417/0bb68a2c/attachment.htm From jacopo.mantovani at unige.it Tue Apr 18 12:18:36 2006 From: jacopo.mantovani at unige.it (Jacopo Mantovani) Date: Tue Apr 18 12:16:39 2006 Subject: [Avispa-users] Error Message In-Reply-To: References: Message-ID: <4444BCFC.3020403@unige.it> Dear Kamal, Kamal-Eldin Mohamed wrote: > Hi, > > I'm a new AVISPA user, and for the last 24 hours I have repeatedly been > trying to run the Web Interface version of AVISPA, but I keep getting > the following error message everytime I attempt to run a protocol: > > *"The HLPSL2IF translator is reporting the following error:* > > *Secure connection to 130.251.7.42 refused."* > > Is it something has to do with my computer/connection? or is it the > AVISPA temporarily down? No, it has nothing to do with your machine at all. The fault was on our side: one of the servers we currently use for the avispa interface crashed, but it should be fine now. Please let me know if you're still experiencing problems. Best Regards, Jacopo. -- Jacopo Mantovani Artificial Intelligence Laboratory DIST - University of Genova, Italy http://www.ai.dist.unige.it/jacopo From kemm16 at hotmail.com Tue Apr 18 19:53:42 2006 From: kemm16 at hotmail.com (Kamal-Eldin Mohamed) Date: Tue Apr 18 19:52:09 2006 Subject: [Avispa-users] Kerberos_5 with ticket cashing Message-ID: An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060418/7bf4a429/attachment.htm From khaled.masmoudi at int-evry.fr Wed Apr 19 08:57:49 2006 From: khaled.masmoudi at int-evry.fr (Khaled Masmoudi) Date: Wed Apr 19 08:56:04 2006 Subject: [Avispa-users] Kerberos_5 with ticket cashing In-Reply-To: Message-ID: <000001c6637e$9244cf50$51679f9d@micro.intevry.fr> Skipped content of type multipart/alternative-------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/x-pkcs7-signature Size: 3060 bytes Desc: not available Url : http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060419/3ed37cdd/smime-0001.bin From feghali at fi.usj.edu.lb Wed Apr 19 10:20:12 2006 From: feghali at fi.usj.edu.lb (Toni Feghali) Date: Wed Apr 19 09:18:17 2006 Subject: [Avispa-users] Kerberos_5 with ticket cashing In-Reply-To: <000001c6637e$9244cf50$51679f9d@micro.intevry.fr> Message-ID: Hi Kamal, Check with kerb-preauth.hlpsl that you have with in hlpsl folder of your avispa installation, it may help you, A question for everybody, Can we model multicast with avispa ( I mean a multicast channel) ? Thanks Toni Feghali Universit? Saint Joseph de Beyrouth _____ From: avispa-users-bounces@avispa-project.org [mailto:avispa-users-bounces@avispa-project.org] On Behalf Of Khaled Masmoudi Sent: Wednesday, April 19, 2006 8:58 AM To: 'Kamal-Eldin Mohamed'; avispa-users@avispa-project.org Subject: RE: [Avispa-users] Kerberos_5 with ticket cashing Hi, Isn?t it already modelled in HLPSL? Check the list of protocols .. Cheers Khaled ---------------------------------------------------------------------------- ---------- Khaled MASMOUDI (PhD student) Institut National des T?l?communications Wireless Networks and Multimedia Services Department (RS2M) Mobility and Security Group CNRS UMR SAMOVAR 5157 9, rue Charles Fourier - 91011 Evry Cedex Personal Page: www.masmoudi.net T?l : +33 1 60 76 42 65 Fax : +33 1 60 76 45 78 khaled.masmoudi@int-evry.fr _____ De : avispa-users-bounces@avispa-project.org [mailto:avispa-users-bounces@avispa-project.org] De la part de Kamal-Eldin Mohamed Envoy? : mardi 18 avril 2006 19:54 ? : avispa-users@avispa-project.org Objet : [Avispa-users] Kerberos_5 with ticket cashing Hi All, Im working on modeling Kerberos-5 authentication protocol, and Im having difficulty modeling the protocol with the authenticator being cashed (i.e. Ticket Cashing). Any help or guidance on this matter is truly appreciated. Thanks, Kamal _____ Don't just search. Find. MSN Search Check out the new MSN Search! -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060419/a3169d16/attachment.htm From A00472021 at itesm.mx Fri Apr 21 04:17:24 2006 From: A00472021 at itesm.mx (A00472021@itesm.mx) Date: Fri Apr 21 04:15:56 2006 Subject: [Avispa-users] Is it possible a valid session with the intruder? Message-ID: <442FD1C900012208@mailserver1.itesm.mx> Hi list, I'm trying to find a counterexample to the Woo Lam Mutual Authentication protocol with avispa toolkit, I know that the protocol is faulty. The counterexample is establishing two parallel sessions with the intruder (available in http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html). My questions is: It is possible to do valid sessions with the intruder?, it is because until now, avispa (ofmc and clatse) cannot obtain an attack on the Woo Lam Auth protocol. Put differently, in this counterexample there isn't the participation of Alice and Bob, rather, the participation is only between Alice and Intruder. Because of that my question ..... Attached the hlspl specification of Woo Lam protocol, I hope someone may help me ... Thanks a lot for your trouble ..... Juan Carlos -------------- next part -------------- A non-text attachment was scrubbed... Name: WooLamMutualAuth-fault.hlpsl Type: application/octet-stream Size: 4832 bytes Desc: not available Url : http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060420/efdae718/WooLamMutualAuth-fault-0001.obj From ychallal at hds.utc.fr Wed Apr 26 10:28:01 2006 From: ychallal at hds.utc.fr (Yacine Challal) Date: Wed Apr 26 10:22:56 2006 Subject: [Avispa-users] A->B:K ? Message-ID: <444F2F11.3000503@hds.utc.fr> Dear Avispa users, We are beginners in using Avispa. We specified a simple protocol using HLPSL : A-> B : K , where K is a secret between A and B. We claimed that this protocol guarantees unilateral authentication. It is easy to see that this protocol is not safe, and we expected Avispa to say : UNSAFE, and a trace attack would be for instance : i->(a,3) : start (a,3)->i : kab i->(b,3) : kab This is not the case. Avispa says the protocol is SAFE. We wonder if we made a mistake in our specification. Please find attach to this message our HLPSL specification. Thank you for your cooperation. Best regards, Ouadjaout Abdelraouf (USTHB-Algiers) Yacine Challal (UTC-Compi?gne) -- ------------------------------------- Yacine Challal Heudiasyc Lab. Royallieu Research Center Compiegne University of Technology PoBox: 20529 60205, France. Tel: +33 3 44 23 46 99 Post: 4280 Fax: +33 3 44 23 44 77 Web: http://www.hds.utc.fr/~ychallal/ ------------------------------------- From khaled.masmoudi at int-evry.fr Wed Apr 26 10:31:45 2006 From: khaled.masmoudi at int-evry.fr (Khaled Masmoudi) Date: Wed Apr 26 10:30:03 2006 Subject: [Avispa-users] A->B:K ? In-Reply-To: <444F2F11.3000503@hds.utc.fr> Message-ID: <004c01c6690b$da51d2b0$51679f9d@micro.intevry.fr> Hi Yacine, You forgot the HLPSL file :) Cheers Khaled -------------------------------------------------------------------------- -- ---------- Khaled MASMOUDI Institut National des Télécommunications Wireless Networks and Multimedia Services Department (RS2M) 9, rue Charles Fourier - 91011 Evry Cedex Personal Page: www.masmoudi.net Tél : +33 1 60 76 42 65 Fax : +33 1 60 76 45 78 khaled.masmoudi@int-evry.fr -----Message d'origine----- De : avispa-users-bounces@avispa-project.org [mailto:avispa-users-bounces@avispa-project.org] De la part de Yacine Challal Envoyé : mercredi 26 avril 2006 10:28 À : avispa-users@avispa-project.org; ouadjaout@gmail.com Objet : [Avispa-users] A->B:K ? Dear Avispa users, We are beginners in using Avispa. We specified a simple protocol using HLPSL : A-> B : K , where K is a secret between A and B. We claimed that this protocol guarantees unilateral authentication. It is easy to see that this protocol is not safe, and we expected Avispa to say : UNSAFE, and a trace attack would be for instance : i->(a,3) : start (a,3)->i : kab i->(b,3) : kab This is not the case. Avispa says the protocol is SAFE. We wonder if we made a mistake in our specification. Please find attach to this message our HLPSL specification. Thank you for your cooperation. Best regards, Ouadjaout Abdelraouf (USTHB-Algiers) Yacine Challal (UTC-Compiègne) -- ------------------------------------- Yacine Challal Heudiasyc Lab. Royallieu Research Center Compiegne University of Technology PoBox: 20529 60205, France. Tel: +33 3 44 23 46 99 Post: 4280 Fax: +33 3 44 23 44 77 Web: http://www.hds.utc.fr/~ychallal/ ------------------------------------- _______________________________________________ Avispa-users mailing list Avispa-users@avispa-project.org http://www.avispa-project.org/mailman/listinfo/avispa-users begin 666 smime.p7s M,( &"2J&2(;W#0$'`J" ,( "`0$Q"S )!@4K#@,"&@4`,( &"2J&2(;W#0$' M`0``H(((YS""`F\P@@'8H ,"`0("`P_Z#C -!@DJADB&]PT!`00%`#!B,0LP M"08#500&$P):03$E,",&`U4$"A,<5&AA=W1E($-O;G-U;'1I;F<@*%!T>2D@ M3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E9 MH/ G=%O[D_7:A/8T^WSSM4G$-*9SJ10I[[1EA5M52L#FTUOO0@_LC;72.>6! M32&NCA>&I$-.)!W X ]]T?]G`CJ8>IR$R^FT'VO8?AD6"MHDPF M1PBW3S""`RTP@@*6H ,"`0("`0`P#08)*H9(AO<-`0$$!0`P@=$Q"S )!@-5 M! 83`EI!,14P$P8#500($PQ797-T97)N($-A<&4Q$C 0!@-5! <3"4-A<&4@ M5&]W;C$:,!@&`U4$"A,15&AA=W1E($-O;G-U;'1I;F%PTY-C Q,#$P,# P,#!:%PTR,#$R M,S$R,S4Y-3E:,('1,0LP"08#500&$P):03$5,!,&`U4$"!,,5V5S=&5R;B!# M87!E,1(P$ 8#500'$PE#87!E(%1O=VXQ&C 8!@-5! H3$51H87=T92!#;VYS M=6QT:6YG,2@P)@8#500+$Q]#97)T:69I8V%T:6]N(%-EE'V Q1MNIRD;"$ M7GTM#8][$M^%)74H=#I"+&,GGY5[2^]^&8<=ANJCW;G.EF0:PA1N1*Q\YH_H M30]Q'T XI@"CAWCV^92&7JWJP%YVZ]D4HUUN>GP,I4M5?P89*7^>FB;5:KLX M) AJF,>QVJ.8D?UYV^5:Q!RY`@,!``&C$S 1, \&`U4=$P$!_P0%, ,!`?\P M#08)*H9(AO<-`0$$!0`#@8$`Q^R2?D[X]9:E9V(JI/!-$6#0;XU@6&&L)KM2 M-5P(SS#[J$J6BA]B0B.,%P_TNF2<%ZQ'*=^=F%[2;&!Q7**LW'GCYVX`1Q^U M#2CH`IWDFOT3]*;9?+'XW%\C)@F1@'/0%!O>0ZF#)?+FG"\5ROZFJXH'=8L, MW5&$:^3XT2D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!E M_0( "9->GIKN?9='%*E2%#T@$?Z>VT3QA!$ >9!ER M8+?[`@,!``&C@90P@9$P$@8#51T3`0'_! @P!@$!_P(!`#!#!@-5'1\$/# Z M,#B@-J TAC)H='1P.B\O8W)L+G1H87=T92YC;VTO5&AA=W1E4&5R,!PQ&C 8 M!@-5! ,3$5!R:79A=&5,86)E;#(M,3,X, T&"2J&2(;W#0$!!04``X&!`$B, MT5"#Z@LNS VC9JQG#W^OK+["%Z%#EI2=?TPAN/@V'ZHMGS8OP/0<4""3<#S] MK>%A8L/9.AE^A+&9&P#%&@N"=)XE4)1BQ]LG<52D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!EID?;7QNALB3!G!@DJADB& M]PT!"0\Q6C!8, H&""J&2(;W#0,', X&""J&2(;W#0,"`@(`@# -!@@JADB& M]PT#`@(!0# '!@4K#@,"!S -!@@JADB&]PT#`@(!*# '!@4K#@,"&C *!@@J MADB&]PT"!3!X!@DK!@$$`8(W$ 0Q:S!I,&(Q"S )!@-5! 83`EI!,24P(P8# M500*$QQ4:&%W=&4@0V]N2D@3'1D+C$L,"H&`U4$`Q,C5&AA=W1E(%!EX$ K;-&9R%HT5DIO5!0)_4<)6;*X<*T($=FZ)D2:-I8!&^?Q MH,:9QH?)`DNO7;QL9S%ZZ3N$.] )*7V:@EHA.?R08E\F@G).I,:A1L[PC,;V MFMLW!L>OG%@5F+":5B : K Message-ID: <444F35ED.8030303@hds.utc.fr> Dear Avispa users, We are beginners in using Avispa. We specified a simple protocol using HLPSL : A-> B : K , where K is a secret between A and B. We claimed that this protocol guarantees unilateral authentication. It is easy to see that this protocol is not safe, and we expected Avispa to say : UNSAFE, and a trace attack would be for instance : i->(a,3) : start (a,3)->i : kab i->(b,3) : kab This is not the case. Avispa says the protocol is SAFE. We wonder if we made a mistake in our specification. Please find attach to this message our HLPSL specification. Thank you for your cooperation. Best regards, Ouadjaout Abdelraouf (USTHB-Algiers) Yacine Challal (UTC-Compi?gne) -- ------------------------------------- Yacine Challal Heudiasyc Lab. Royallieu Research Center Compiegne University of Technology PoBox: 20529 60205, France. Tel: +33 3 44 23 46 99 Post: 4280 Fax: +33 3 44 23 44 77 Web: http://www.hds.utc.fr/~ychallal/ ------------------------------------- -------------- next part -------------- %% Author : Ouadjaout Abdelraouf (ouadjaout@gmail.com) %% Date : 18/04/2006 %% Description : A simple unilateral authentication, comparable to telnet %% Assumptions : A and B share a secret key K (the password) %% A-B model : %% A -> B : K role alice ( A, B : agent, K : symmetric_key, Snd, Rcv : channel(dy) ) played_by A def= local State : nat init State := 0 transition 1. State = 0 /\ Rcv(start) =|> State':=2 /\ Snd(K) /\ witness(A,B,bob_alice_k,K) end role role bob ( A, B : agent, K : symmetric_key, Snd, Rcv : channel(dy) ) played_by B def= local State : nat init State := 1 transition 1. State = 1 /\ Rcv(K) =|> State':=3 /\ request(B,A,bob_alice_k,K) end role role session ( A, B : agent, K : symmetric_key ) def= local SA, RA, SB, RB : channel(dy) composition alice(A,B,K,SA,RA) /\ bob(A,B,K,SB,RB) end role role environment() def= const bob_alice_k : protocol_id, kab, kai, kbi: symmetric_key, a,b : agent intruder_knowledge = {a,b,kai,kbi} composition session(a,b,kab) /\ session(a,i,kai) /\ session(i,b,kbi) end role goal authentication_on bob_alice_k end goal environment() From compa at dist.unige.it Wed Apr 26 13:14:39 2006 From: compa at dist.unige.it (Luca Compagna) Date: Wed Apr 26 13:16:40 2006 Subject: [Avispa-users] Is it possible a valid session with the intruder? In-Reply-To: <442FD1C900012208@mailserver1.itesm.mx> References: <442FD1C900012208@mailserver1.itesm.mx> Message-ID: <444F561F.1080805@dist.unige.it> Dear Juan, A00472021@itesm.mx wrote: >Hi list, > >I'm trying to find a counterexample to the Woo Lam Mutual Authentication >protocol with avispa toolkit, I know that the protocol is faulty. The counterexample >is establishing two parallel sessions with the intruder (available in http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html). > My questions is: > >It is possible to do valid sessions with the intruder?, > Yes this is possible. As example you can look at NSPK protocol were the Lowe's attack relies on a session between Alice and the intruder. >it is because until >now, avispa (ofmc and clatse) cannot obtain an attack on the Woo Lam Auth >protocol. Put differently, in this counterexample there isn't the participation >of Alice and Bob, rather, the participation is only between Alice and Intruder. >Because of that my question ..... > >Attached the hlspl specification of Woo Lam protocol, I hope someone may >help me ... > > This might be due to a typo in the protocol_id constants. Namely, you use two protocol_id "ab" and "ba" (see "step6and7" transition) that are undeclared and that are not appropriately referenced from any of the goal you have declared. Try to fix the problem and to run again the tools. Hope this help. Best regards, Luca >Thanks a lot for your trouble ..... > >Juan Carlos > > > > >------------------------------------------------------------------------ > >_______________________________________________ >Avispa-users mailing list >Avispa-users@avispa-project.org >http://www.avispa-project.org/mailman/listinfo/avispa-users > > -- Dr Luca Compagna Senior Scientist SAP Research - Security and Trust SAP Labs France 805 Avenue du Dr Maurice Donat 06254 Mougins Cedex - France T +33/492286495 F +33/492286201 M +33/622700209 mailto:luca.compagna@sap.com http://www.sap.com From compa at dist.unige.it Wed Apr 26 13:39:52 2006 From: compa at dist.unige.it (Luca Compagna) Date: Wed Apr 26 13:41:53 2006 Subject: [Avispa-users] A->B : K In-Reply-To: <444F35ED.8030303@hds.utc.fr> References: <444F35ED.8030303@hds.utc.fr> Message-ID: <444F5C08.30403@dist.unige.it> Dear Yacine, Yacine Challal wrote: > Dear Avispa users, > We are beginners in using Avispa. > We specified a simple protocol using HLPSL : > A-> B : K , > where K is a secret between A and B. Why don't you check for secrecy violation instead of authentication? > We claimed that this protocol guarantees unilateral authentication. > It is easy to see that this protocol is not safe, and we expected > Avispa to say : UNSAFE, and a trace attack would be for instance : > i->(a,3) : start > (a,3)->i : kab > i->(b,3) : kab indeed I think this should not interpreted as an authentication flaw. In the end 'a' and 'b' are sure of their identity even if the intruder has been involved in the communication. A closer look to your specification made me think to "why don't we find a replay attack like the following": i->(a,3) : start (a,3)->i : kab i->(b,3) : kab i->(b,10) : kab where the intruder learns "kab" and uses it to fake 'b' in their session. Well the reason is that in your HLPSL specification, the shared key is given to the agent from the beginning so that they can refuse any communication that does not use the appropriate key. Hope this help. Best regards, Luca > > This is not the case. Avispa says the protocol is SAFE. > We wonder if we made a mistake in our specification. Please find > attach to this message our HLPSL specification. > Thank you for your cooperation. > Best regards, > > Ouadjaout Abdelraouf (USTHB-Algiers) > Yacine Challal (UTC-Compi?gne) > >------------------------------------------------------------------------ > >_______________________________________________ >Avispa-users mailing list >Avispa-users@avispa-project.org >http://www.avispa-project.org/mailman/listinfo/avispa-users > > -- Dr Luca Compagna Senior Scientist SAP Research - Security and Trust SAP Labs France 805 Avenue du Dr Maurice Donat 06254 Mougins Cedex - France T +33/492286495 F +33/492286201 M +33/622700209 mailto:luca.compagna@sap.com http://www.sap.com From A00472021 at itesm.mx Thu Apr 27 19:33:23 2006 From: A00472021 at itesm.mx (=?ISO-8859-1?Q?Juan_Carlos_L=F3pez_Pimentel?=) Date: Thu Apr 27 19:31:35 2006 Subject: [Avispa-users] Is it possible a valid session with the intruder? In-Reply-To: <444F561F.1080805@dist.unige.it> References: <442FD1C900012208@mailserver1.itesm.mx> <444F561F.1080805@dist.unige.it> Message-ID: <44510063.1010401@itesm.mx> Thanks Luca, I have revised in detail Woo Lam protocol, I found out that for getting the counter-example I was looking for, the authentication should be established between Alice and Server (protocol_id alice_server_kab)... The typo pinpointed for you also has been fixed ... thanks again and best wishes, Juan Carlos Luca Compagna wrote: >Dear Juan, > >A00472021@itesm.mx wrote: > > > >>Hi list, >> >>I'm trying to find a counterexample to the Woo Lam Mutual Authentication >>protocol with avispa toolkit, I know that the protocol is faulty. The counterexample >>is establishing two parallel sessions with the intruder (available in http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html). >>My questions is: >> >>It is possible to do valid sessions with the intruder?, >> >> >> >Yes this is possible. As example you can look at NSPK protocol were the >Lowe's attack relies on a session between Alice and the intruder. > > > >>it is because until >>now, avispa (ofmc and clatse) cannot obtain an attack on the Woo Lam Auth >>protocol. Put differently, in this counterexample there isn't the participation >>of Alice and Bob, rather, the participation is only between Alice and Intruder. >>Because of that my question ..... >> >>Attached the hlspl specification of Woo Lam protocol, I hope someone may >>help me ... >> >> >> >> >This might be due to a typo in the protocol_id constants. Namely, you >use two protocol_id "ab" and "ba" (see "step6and7" transition) that are >undeclared and that are not appropriately referenced from any of the >goal you have declared. Try to fix the problem and to run again the tools. > >Hope this help. Best regards, >Luca > > > >>Thanks a lot for your trouble ..... >> >>Juan Carlos >> >> >> >> >>------------------------------------------------------------------------ >> >>_______________________________________________ >>Avispa-users mailing list >>Avispa-users@avispa-project.org >>http://www.avispa-project.org/mailman/listinfo/avispa-users >> >> >> >> > > > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060427/a79483d1/attachment.htm From A00472021 at itesm.mx Thu Apr 27 22:01:02 2006 From: A00472021 at itesm.mx (=?ISO-8859-1?Q?Juan_Carlos_L=F3pez_Pimentel?=) Date: Thu Apr 27 21:59:02 2006 Subject: [Avispa-users] May Avispa find an attack after a second one? Message-ID: <445122FE.5090406@itesm.mx> Hi List, I'm verifying CCITTX509(1) protocol whose specification is one step as follows: 1 A --> B: A, {B, Nxa, {Nya}_Kb}_inv(Ka) I know that the protocol is faulty, the attack should be (following the option -p of OFMC): Attack 1: i -> (a,3): start (a,3) -> i: a.{b.Nxa(1).{Nya(1)}_kb}_inv(ka) i -> (b,10): i.{b.x38.{Nya(1)}_kb}_inv(ki) However, I still don't know how to find this attack, I have played in different way the environment role and I have only found the following attack: Attack 2: i -> (a,3): start (a,3) -> i: a.{b.Nxa(1).{a.Nya(1)}_kb}_inv(ka) i -> (b,3): a.{b.Nxa(1).{a.Nya(1)}_kb}_inv(ka) i -> (b,6): a.{b.Nxa(1).{a.Nya(1)}_kb}_inv(ka) I have the following assumption: "I know that the first attack is within the branch-searched tree, maybe, when any backend searches for an attack, the first attack found is Attack 2 and maybe Attack 1 is situated after the first one". Therefore, I have two questions: 1. If my assumption is correct, how may I find the first attack (Attack 1)? 2. Otherwise, Will I be doing something erroneous in the hlpsl specification? Attached to this message the hlpsl specification of CCITTX509(1) protocol... I hope someone may help me ... Thanks a lot for your trouble ..... Juan Carlos L?pez Pimentel PhD student, ITESM-CEM, M?xico -------------- next part -------------- %% CCITTX5091 protocol %1 A --> B : A, {B, Nxa, {Nya}K+B}K-A %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role alice(A,B:agent, KA, KB: public_key, Snd, Rcv: channel (dy)) played_by A def= local State: nat, Nxa, Nya: text const nxa,secret_Nya, nya: protocol_id init State := 0 transition %% Start of the protocol %1 A --> B : A, {B, Nxa, {Nya}K+B}K-A step1. State = 0 /\ Rcv(start) =|> State':= 1 /\ Nxa':= new() /\ Nya':= new() /\ Snd(A.{B.Nxa'.{Nya'}_KB}_inv(KA)) /\ witness(A,B,nxa,Nxa') /\ witness(A,B,nya,Nya') /\ secret(Nya',secret_Nya,{A,B}) % /\ request(A,B,ba_nya,Nya') end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %1 A --> B : A, {B, Nxa, {Nya}K+B}K-A role bob(A,B:agent, KA,KB: public_key, Rec: channel (dy)) played_by B def= local State: nat, NonceUsed: text set, Nxa, Nya: text const nya: protocol_id init State := 0 transition %1 A --> B : A, {B, Nxa, {Nya}K+B}K-A step1. State = 0 /\ Rec(A.{B.Nxa'.{Nya'}_KB}_inv(KA)) =|> State':= 1 /\ request(B,A,nxa,Nxa') /\ request(B,A,nya,Nya') end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%% %% The role representing a partial session between alice and bob role ccittx5091(A,B: agent, KA, KB: public_key) def= local S_AB, R_S,R_AB: channel (dy) composition alice (A,B,KA,KB,S_AB,R_S) /\ bob (A,B,KA,KB,R_AB) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% The main role role environment() def= const a, b, i : agent, ka, kb, ki : public_key intruder_knowledge = {ki, inv(ki), ka, kb, a, b, i} composition ccittx5091(a,b,ka,kb) /\ ccittx5091(a,b,ka,kb) % /\ ccittx5091(b,a,kb,ka) % /\ ccittx5091(i,b,ki,kb) % /\ ccittx5091(a,i,ka,ki) /\ ccittx5091(i,b,ki,kb) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Properties to verify goal secrecy_of secret_Nya %% authentication_on nxa authentication_on nya %% authentication_on nxa %% authentication_on ta %% authentication_on na %% weak_authentication_on bob_alice_na end goal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Call of the main role environment() From Laurent.Vigneron at loria.fr Fri Apr 28 09:40:32 2006 From: Laurent.Vigneron at loria.fr (Laurent Vigneron) Date: Fri Apr 28 09:38:44 2006 Subject: [Avispa-users] May Avispa find an attack after a second one? Message-ID: <17489.50928.719427.926066@valhey.loria.fr> Hi Juan Carlos, The attack raised by the AVISPA tool shows that this protocol does not satisfy strong authentication on Nya. If you ask for checking weak authentication, there will not be any attack. About the first attack that you are looking for, I am not convinced this is one. Could you explain what is the property that is not satisfied? In the trace > Attack 1: > i -> (a,3): start > (a,3) -> i: a.{b.Nxa(1).{Nya(1)}_kb}_inv(ka) > i -> (b,10): i.{b.x38.{Nya(1)}_kb}_inv(ki) b knows that i has sent him this message, and as i is the intruder, there is no authentication done between b and i. Laurent. From armando at armandobook.mrg.dist.unige.it Fri Apr 28 14:41:54 2006 From: armando at armandobook.mrg.dist.unige.it (Alessandro Armando) Date: Fri Apr 28 14:39:40 2006 Subject: [Avispa-users] Survey of AVISPA related activities Message-ID: <20060428124159.57AE51E72F4@armandobook.mrg.dist.unige.it> Dear AVISPA users, as the number of AVISPA users steadily increases we feel it is imporant to collect and make available information about the past/ongoing/planned usage of the tool. We believe this would increase the awareness of the AVISPA users' community and promote synergy among the AVISPA users. To this end we ask to send me (armando@dist.unige.it) a brief description of your usage of the AVISPA Tool by using the following template. -------------------------------------------------------------------- 1. FIRST NAME: 2. FAMILY NAME: 3. AFFILIATION: 4. E-MAIL ADDRESS: 5. WEB PAGE: 6. BRIEF DESCRIPTION OF THE USAGE OF THE AVISPA TOOL (max 100 words): 7. RESULTS (e.g. HLPSL specifications, papers, technical reports, lectures, seminars. Please provides bibliographic references and/or pointers to online copy of the material, if available): 8. AUTHORIZATION (please delete one of the sentences below): I consent the AVISPA Team to include my name in the survey. I do not consent the AVISPA Team to include my name in the survey -------------------------------------------------------------------- Thank you very much for your help, Alessandro Armando (on behalf of the AVISPA Team) -- Alessandro Armando e-mail: armando@dist.unige.it Artificial Intelligence Laboratory http://www.ai.dist.unige.it/armando DIST - Universita' di Genova, phone: +39-0103532216 viale Causa 13, fax: +39-0103532948 16145 GENOVA, ITALY mobile: +39-3281003201 From A00472021 at itesm.mx Fri Apr 28 20:12:58 2006 From: A00472021 at itesm.mx (=?ISO-8859-1?Q?Juan_Carlos_L=F3pez_Pimentel?=) Date: Fri Apr 28 20:11:02 2006 Subject: [Avispa-users] May Avispa find an attack after a second one? In-Reply-To: <17489.50928.719427.926066@valhey.loria.fr> References: <17489.50928.719427.926066@valhey.loria.fr> Message-ID: <44525B2A.6070704@itesm.mx> Hi Laurent, thanks for your soon answer... In the protocol: 1 A --> B: A, {B, Nxa, {Nya}_Kb}_inv(Ka) Laurent Vigneron wrote: >About the first attack that you are looking for, I am not convinced >this is one. Could you explain what is the property that is not >satisfied? >In the trace > > > Attack 1: > > i -> (a,3): start > > (a,3) -> i: a.{b.Nxa(1).{Nya(1)}_kb}_inv(ka) > > i -> (b,10): i.{b.x38.{Nya(1)}_kb}_inv(ki) > >b knows that i has sent him this message, and as i is the intruder, >there is no authentication done between b and i. > > Maybe I have an erroneous idea about the role that "i" (the intruder) is playing with respect to "b". In the above attack I have the idea that "b", naively, thinks that "i" is a honest agent and "b" could authenticate to "i" on Nya (same variable where "a" does a witness). This attack is shown in http://www.lsv.ens-cachan.fr/spore/ccittx509_1.html If you think that I have an erroneous idea, please I will be grateful you tell me why... best regards, Juan Carlos > > From xheo at yahoo.fr Mon May 1 11:01:26 2006 From: xheo at yahoo.fr (Bassem Fennani) Date: Mon May 1 10:59:29 2006 Subject: [Avispa-users] help plz Message-ID: <20060501090126.4562.qmail@web26706.mail.ukl.yahoo.com> hello , i'm a new user of Avispa Tool i would be grateful if you can provide me with SET protocol Hpls specification thx --------------------------------- Faites de Yahoo! votre page d'accueil sur le web pour retrouver directement vos services pr?f?r?s : v?rifiez vos nouveaux mails, lancez vos recherches et suivez l'actualit? en temps r?el. Cliquez ici. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060501/fe27e75b/attachment.htm From iwk20 at ui.edu Mon May 1 11:09:45 2006 From: iwk20 at ui.edu (Ilham Kurnia) Date: Mon May 1 11:07:49 2006 Subject: [Avispa-users] help plz In-Reply-To: <20060501090126.4562.qmail@web26706.mail.ukl.yahoo.com> References: <20060501090126.4562.qmail@web26706.mail.ukl.yahoo.com> Message-ID: <1146474586.8544.9.camel@riset-a-s1-112.riset.cs.ui.ac.id> Hi there, Found two specs at http://avispa-project.org/library/index.html : http://avispa-project.org/library/SET-purchase.html and http://avispa-project.org/library/SET-purchase-honest-payment-gateway.html The hlpsl spec for each is at the bottom half of the page. Cheers, Ilham On Mon, 2006-05-01 at 11:01 +0200, Bassem Fennani wrote: > hello , > i'm a new user of Avispa Tool > i would be grateful if you can provide me with SET protocol Hpls > specification > thx > > ______________________________________________________________________ From xheo at yahoo.fr Mon May 1 13:00:14 2006 From: xheo at yahoo.fr (Bassem Fennani) Date: Mon May 1 12:58:11 2006 Subject: [Avispa-users] about TLS Message-ID: <20060501110014.36069.qmail@web26712.mail.ukl.yahoo.com> hi , i know that the replay attack exists on TLS protocol (since the server decrypt all messages sent by the client )but it's not mentionned in TLS spec . i would like to know why. thx --------------------------------- Faites de Yahoo! votre page d'accueil sur le web pour retrouver directement vos services pr?f?r?s : v?rifiez vos nouveaux mails, lancez vos recherches et suivez l'actualit? en temps r?el. Cliquez ici. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://carroll.ai.dist.unige.it/pipermail/avispa-users/attachments/20060501/fbb7c0fe/attachment.htm From iwk20 at ui.edu Mon May 1 15:14:28 2006 From: iwk20 at ui.edu (Ilham Kurnia) Date: Mon May 1 15:12:39 2006 Subject: [Avispa-users] OFMC: exponentiation support question Message-ID: <1146489269.8544.48.camel@riset-a-s1-112.riset.cs.ui.ac.id> Hi all, I have been trying to verify the authentication protocol B proposed by European Telecommunications Standard Institute and used in authentication part of Horn-Preneel UTMSPayment protocol. The protocol uses exponentiation as shown in Alice-Bob model below: U -> V: exp(g,u) V -> U: r; h2(K; r; V); Timestamp; certV where K = h1(exp(g,u),v) U -> V: {Sig_U(h3(exp(g,u); exp(g,v); r; V; Timestamp; Alpha_T); certU; Alpha_T}_K h1, h2, and h3 are hash functions; u and r are nonces, while v is the private key of V and exp(g,v) is V's public key. When I tested my complete model using OFMC as backend with sessco option on, the following message appeared. ofmc: OFMC can't see how the protocol can be executed. See manual for more information. I have reduced the HLPSL file (attached) to a model of which this behaviour is still observable. Have I used the exponentiation function incorrectly such that OFMC rejects my specification? Thank you very much for your trouble. Regards, Ilham Kurnia ------ Undergraduate Student Faculty of Computer Science University of Indonesia -------------- next part -------------- role user(U, V : agent, H1, H2, H3 : function, F : function, G : text, % Generator g Kv : message, % public key of V, from exp(g,v) Ku : public_key, % dummy for signature Kca : public_key, % Certificate authority public key Kpriv_v : text, Cert_u : {message}_inv(public_key), Snd, Rcv : channel(dy)) played_by U def= local State: nat, Random_u : text, % randomly generated number Timestamp : text, Random_r : text, Cert_v : {message}_inv(public_key), Random_u_exp : message, Session_key : text, Hash2 : message init State := 0 transition 0. State = 0 /\ Rcv(start) =|> State' := 2 /\ Random_u' := new() /\ Random_u_exp' := exp(G,Random_u') /\ Snd(Random_u_exp') 2. State = 2 /\ Rcv(Random_r'.H2(H1(exp(Kv,Random_u).Random_r').Random_r'.V).Timestamp'.{V.Kv}_inv(Kca)) =|> State' := 4 /\ Session_key' := H1(exp(Kv,Random_u).Random_r') /\ secret(Session_key',session_key,{U,V}) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role vasp(U, V : agent, H1, H2, H3 : function, Ku : public_key, Kca : public_key, % certificate authority public key Kpriv_v : text, Cert_v : {message}_inv(public_key), Snd, Rcv : channel(dy)) played_by V def= local State: nat, Random_u_exp : message, Random_r : text, Timestamp : text, Session_key : message const session_key : protocol_id init State := 1 transition 1. State = 1 /\ Rcv(Random_u_exp') =|> State' := 3 /\ Timestamp' := new() /\ Random_r' := new() /\ Session_key' := H1(exp(Random_u_exp',Kpriv_v).Random_r') /\ Snd(Random_r'.H2(Session_key'.Random_r'.V).Timestamp'.Cert_v) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role session(U, V : agent, H1, H2, H3, F : function, G, T : text, Kpriv_v : text, % V's private key Ku, Kca : public_key, Cert_u, Cert_v : {message}_inv(public_key)) def= local Su, Ru, Sv, Rv : channel(dy) composition user(U, V, H1, H2, H3, F, G, exp(G,Kpriv_v), Ku, Kca, Kpriv_v, Cert_u, Su, Ru) /\ vasp(U, V, H1, H2, H3, Ku, Kca, Kpriv_v, Cert_v, Sv, Rv) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% role environment() def= const u, v, a, i : agent, h1, h2, h3, f, exp : function, g, t, kv, ki : text, ku, ka, kca, kpi : public_key intruder_knowledge = {u,v,a,i,h1,h2,h3,f,g,t,exp(g,kv),{v.exp(g,kv)}_inv(kca),{u.ku}_inv(kca),kca,ku,ki,exp(g,ki),kpi,ka} composition session(u,v,h1,h2,h3,f,g,t,kv,ku,kca,{u.ku}_inv(kca),{v.exp(g,kv)}_inv(kca)) end role %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% goal secrecy_of session_key end goal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% environment()