{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:46:48Z","timestamp":1725515208839},"publisher-location":"Boston, MA","reference-count":22,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387096988"},{"type":"electronic","value":"9780387096995"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-09699-5_10","type":"book-chapter","created":{"date-parts":[[2008,7,16]],"date-time":"2008-07-16T18:12:54Z","timestamp":1216231974000},"page":"141-155","source":"Crossref","is-referenced-by-count":2,"title":["A B Formal Framework for Security Developments in the Domain of Smart Card Applications"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"first","affiliation":[]},{"given":"Marie-Laure","family":"Potet","sequence":"additional","affiliation":[]},{"given":"R\u00e9gis","family":"Tissot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"J-R. Abrial and L. Mussat. Introducing Dynamic Constrains in B. In D. Bert, editor, Proceedings of the 2nd Int. B Conference, volume 1393 of LNCS. Springer, 1998."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"P. Behm and all. M\u2019et\u2019eor: A Successful Application of B in a Large Project. In FM\u201999 - Formal Methods, volume 1708 of LNCS, pages 348\u2013387. Springer, September 1999.","DOI":"10.1007\/3-540-48119-2_22"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"N. Benaissa, D. Cansell, and D. Mery. Integration of Security Policy into System Modeling. In Julliand and Kouchnarenko [15].","DOI":"10.1007\/11955757_19"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"D. Bert, S. Boulm\u2019e, M-L. Potet, A. Requet, and L. Voisin. Adaptable Translator of B Specifications to Embedded C programs. In FME 2003: Formal Methods, volume 2805 of LNCS. Springer, 2003.","DOI":"10.1007\/978-3-540-45236-2_7"},{"key":"10_CR6","unstructured":"F. Bouquet, F. Celletti, G. Debois, A. De Lavernette, E. Jaffuel, J. Julliand, B. Legeard, J. Lidoine, J.-C. Plessis, and P.-A. Masson. Model-based security testing, application to a smart card identity applet. In eSmart 2006, 7th Int. Conf. on Smart Cards, Sophia-Antipolis, France, September 2006."},{"key":"10_CR7","unstructured":"Common Criteria for Information Technology Security Evaluation, Part 2: Security functional components. Technical Report CCMB-2006-09-002, version 3.1, sept 2006."},{"key":"10_CR8","unstructured":"Common Criteria for Information Technology Security Evaluation, Part 3: Security assurance components. Technical Report CCMB-2006-09-003, version 3.1, sept 2006."},{"key":"10_CR9","unstructured":"Common Criteria for Information Technology Security Evaluation, version 3.1. Technical Report CCMB-2006-09-001, sept 2006."},{"key":"10_CR10","unstructured":"E.W. Dijkstra. A discipline of Programming. Prentice-Hall, 1976."},{"key":"10_CR11","unstructured":"The Gixel web site. http:\/\/gixel.fr."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"A. Haddad. Meca: a Tool for Access Control Models. In Julliand and Kouchnarenko [15].","DOI":"10.1007\/11955757_30"},{"key":"10_CR13","unstructured":"Smart Card Standard: Part 4: Interindustry Commands for Interchange. Technical report, ISO\/IEC, 1995."},{"key":"10_CR14","unstructured":"E. Jaffuel and B. Legeard. LEIRIOS Test Generator: Automated Test Generation from B Models. In Julliand and Kouchnarenko [15]."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"J. Julliand and O. Kouchnarenko, editors. B 2007: Formal Specification ans Development in B, volume 4355 of LNCS. Springer, 2007.","DOI":"10.1007\/11955757"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Lamport. A temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, may 1994.","DOI":"10.1145\/177492.177726"},{"key":"10_CR17","unstructured":"J-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In CARDIS\u201998, number 1820 in LNCS. Springer, 1998."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"K. Li, L. Mounier, and R. Groz. Test Generation from Security Policies Specified in Or-BAC. In COMPSAC \u2013 IEEE International Workshop on Secuirty in Software Engineering (IWSSE\u201907), Beijing, July 2007.","DOI":"10.1109\/COMPSAC.2007.210"},{"issue":"1","key":"10_CR19","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"B.Schneider. Fred","year":"2000","unstructured":"Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30\u201350, 2000.","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"N. Stouls and M-L. Potet. Security Policy Enforcement through Refinement Process. In Julliand and Kouchnarenko [15].","DOI":"10.1007\/11955757_18"},{"issue":"1","key":"10_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0169-7552(96)00017-7","volume":"29","author":"J. Tretmans","year":"1996","unstructured":"J. Tretmans. Conformance testing with labelled transition systems: Implementation relations and test generation. Computer Networks and ISDN Systems, 29(1):49\u201379, 1996.","journal-title":"Computer Networks and ISDN Systems"},{"key":"10_CR22","unstructured":"M. Utting and B. Legeard. Practical Model-Based Testing - A tools approach. Elsevier Science, 2006. 550 pages."}],"container-title":["IFIP \u2013 The International Federation for Information Processing","Proceedings of The Ifip Tc 11 23rd International Information Security Conference"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-09699-5_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:45:32Z","timestamp":1619574332000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-09699-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387096988","9780387096995"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-09699-5_10","relation":{},"ISSN":["1571-5736"],"issn-type":[{"type":"print","value":"1571-5736"}],"subject":[]}}