<?xml version="1.0" encoding="utf-8"?><!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.0 20120330//EN" "JATS-journalpublishing1.dtd"><article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" article-type="article">
<front>
    <journal-meta>
        <journal-id journal-id-type="publisher-id">INFEDU</journal-id>
        <journal-title-group>
            <journal-title>Informatics in Education</journal-title>
        </journal-title-group>
        <issn pub-type="epub">1648-5831</issn>
        <issn pub-type="ppub">1648-5831</issn>
        <publisher>
            <publisher-name>VU</publisher-name>
        </publisher>
    </journal-meta>
    <article-meta>
                <article-id pub-id-type="publisher-id">INFE2020_3_19</article-id>
                        <article-id pub-id-type="doi">10.15388/infedu.2020.19</article-id>
                        <article-categories>
            <subj-group subj-group-type="heading">
                <subject>Article</subject>
            </subj-group>
        </article-categories>
                        <title-group>
            <article-title>Integrating Formal Methods for Security in Software Security Education</article-title>
        </title-group>
                        <contrib-group>
                                        <contrib contrib-type="author">
                                                <name>
                    <surname>MODESTI</surname>
                    <given-names>Paolo</given-names>
                </name>
                                <email xlink:href="mailto:p.modesti@tees.ac.uk">p.modesti@tees.ac.uk</email>
                                                <xref ref-type="aff" rid="j_INFEDU_aff_000"/>
                                            </contrib>
                        <aff id="j_INFEDU_aff_000">Department of Computer Science and Information Systems, Teesside University
Middlesbrough, United Kingdom</aff>
                                </contrib-group>
                                                                            <volume>19</volume>
                                <issue>3</issue>
                                    <fpage>425</fpage>
                        <lpage>454</lpage>
                                <pub-date pub-type="epub">
                        <day>16</day>
                                    <month>09</month>
                        <year>2020</year>
        </pub-date>
                                <permissions>
                                    <copyright-year>2020</copyright-year>
                                    <copyright-holder>Vilnius University, ETH Zürich</copyright-holder>
                                    <license
                                    license-type="open-access"
                                            >
                <license-p>Open access article under the CC BY license.</license-p>
            </license>
                    </permissions>
                        <abstract>
                        <p>As the number of software vulnerabilities discovered increases, the industry is facing difficulties to find specialists to cover the vacancies for security software developers. Considering relevant teaching and learning theories, along with existing approaches in software security education, we present the pedagogic rationale and the concrete implementation of a course on security protocol development that integrates formal methods for security research into the teaching practice. A novelty of the framework is the adoption of a conceptual model aligned with the level of abstraction used for the symbolic (high-level) representation of cryptographic and communication primitives. This is aimed not only at improving skills in secure software development, but also at bridging the gap between the formal representation and the actual implementation, making formal methods and tools more accessible to students and practitioners.</p>
                    </abstract>
                <kwd-group>
            <label>Keywords</label>
                        <kwd>software security education</kwd>
                        <kwd>formal methods for security</kwd>
                        <kwd>programming abstractions</kwd>
                        <kwd>research-led teaching</kwd>
                        <kwd>constructivism</kwd>
                    </kwd-group>
    </article-meta>
</front>
</article>
