{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T11:40:01Z","timestamp":1749987601754,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319539454"},{"type":"electronic","value":"9783319539461"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-53946-1_5","type":"book-chapter","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T12:42:51Z","timestamp":1487162571000},"page":"75-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Formal Verification of Gate-Level Multiple Side Channel Parameters to Detect Hardware Trojans"],"prefix":"10.1007","author":[{"given":"Imran Hafeez","family":"Abbasi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Faiq Khalid","family":"Lodhi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Awais Mehmood","family":"Kamboh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"issue":"5","key":"5_CR1","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/MSPEC.2008.4505310","volume":"45","author":"S Adee","year":"2008","unstructured":"Adee, S.: The hunt for the kill switch. IEEE Spectr. 45(5), 34\u201339 (2008)","journal-title":"IEEE Spectr."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Agrawal, D., Baktir, S., Karakoyunlu, D., Rohatgi, P., Sunar, B.: Trojan detection using IC fingerprinting. In: Symposium on Security and Privacy, pp. 296\u2013310. IEEE (2007)","DOI":"10.1109\/SP.2007.36"},{"key":"5_CR3","unstructured":"Anderson, M.S., North, C., Yiu, K.K.: Towards countering the rise of the silicon Trojan. In: Annual Report. Defence Science and Technology Organisation, DSTO-TR-2220, Australia (2008)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bara, A., Bazargan-Sabet, P., Chevallier, R., Encrenaz, E.: Formal Verification of Timed VHDL Programs. In: Specification & Design Languages, pp. 1\u20136. IET (2010)","DOI":"10.1049\/ic.2010.0133"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bhasin, S., Regazzoni, F.: A survey on hardware Trojan detection techniques. In: Circuits and Systems, pp. 2021\u20132024. IEEE (2015)","DOI":"10.1109\/ISCAS.2015.7169073"},{"issue":"8","key":"5_CR6","doi-asserted-by":"publisher","first-page":"1229","DOI":"10.1109\/JPROC.2014.2334493","volume":"102","author":"S Bhunia","year":"2014","unstructured":"Bhunia, S., Hsiao, M.S., Banga, M., Narasimhan, S.: Hardware Trojan attacks: threat analysis and countermeasures. Proceedings of IEEE 102(8), 1229\u20131247 (2014)","journal-title":"Proceedings of IEEE"},{"issue":"6","key":"5_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S1571-0661(04)80468-7","volume":"65","author":"M Bozga","year":"2002","unstructured":"Bozga, M., Jianmin, H.: Maler: verification of asynchronous circuits using timed automata. Electron. Notes Theoret. Comput. Sci. 65(6), 47\u201359 (2002)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-08867-9_22"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-04138-9_28","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2009","author":"RS Chakraborty","year":"2009","unstructured":"Chakraborty, R.S., Wolff, F., Paul, S., Papachristou, C., Bhunia, S.: MERO: a statistical approach for hardware Trojan detection. In: Clavier, C., Gaj, K. (eds.) CHES 2009. LNCS, vol. 5747, pp. 396\u2013410. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04138-9_28"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45657-0_29"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Claris\u00f3, R., Cortadella, J.: Verification of timed circuits with symbolic delays. In: Asia and South Pacific Design Automation Conference, pp. 628\u2013633. IEEE (2004)","DOI":"10.1109\/ASPDAC.2004.1337668"},{"key":"5_CR12","unstructured":"Di Natale, G., Dupuis, S.: Is side-channel analysis really reliable for detecting hardware Trojans?. In: Design of Circuits and Integrated Systems, pp. 238\u2013242 (2012)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Drechsler, R., et al.: Advanced Formal Verification. Springer (2004)","DOI":"10.1007\/b105236"},{"key":"5_CR14","unstructured":"Force, T.: High performance microchip supply. In: Annual Report. Defense Technical Information Center (DTIC), USA (2005). http:\/\/www.acq.osd.mil\/dsb\/reports\/ADA435563.pdf"},{"key":"5_CR15","unstructured":"Jin, Y., Makris, Y.: Hardware Trojan Detection using Path Delay Fingerprint. In: Hardware-Oriented Security and Trust, 2008. pp. 51\u201357. IEEE (2008)"},{"key":"5_CR16","unstructured":"Lin, J.Y., Liu, T.C., Shen, W.Z.: A cell-based power estimation in CMOS combinational circuits. In: Computer-Aided Design, pp. 304\u2013309. IEEE (1994)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Lodhi, F.K., Abbasi, I., Khalid, F., Hasan, O., Awwad, F., Hasan, S.R.: A self-learning framework to detect the intruded integrated circuits. In: International Symposium on Circuits and Systems, pp. 1702\u20131705 (2016)","DOI":"10.1109\/ISCAS.2016.7538895"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Lodhi, F.K., Hasan, S.R., Hasan, O., Awwad, F.: Hardware Trojan detection in soft error tolerant macro synchronous micro asynchronous (MSMA) pipeline. In: Midwest Symposium on Circuits and Systems. pp. 659\u2013662 (2014)","DOI":"10.1109\/ISVLSI.2014.59"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Lodhi, F., Hasan, S., Hasan, O., Awwad, F.: Formal analysis of macro synchronous micro asychronous pipeline for hardware Trojan detection. In: Nordic Circuits and Systems Conference & International Symposium on System-on-Chip, pp. 1\u20134. IEEE (2015)","DOI":"10.1109\/NORCHIP.2015.7364384"},{"key":"5_CR20","unstructured":"MathSAT 5: (2016). http:\/\/mathsat.fbk.eu\/"},{"issue":"2","key":"5_CR21","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/MSPEC.2015.7024511","volume":"52","author":"S Mitra","year":"2015","unstructured":"Mitra, S., Wong, H.S.P., Wong, S.: The Trojan-proof chip. IEEE Spectr. 52(2), 46\u201351 (2015)","journal-title":"IEEE Spectr."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Mukhopadhyay, D., Chakraborty, R.S.: Hardware Security: Design, Threats, and Safeguards. CRC (2014)","DOI":"10.1201\/b17555"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Ngo, X.T., Danger, J.L., Guilley, S., Najm, Z., Emery, O.: Hardware property checker for run-time hardware Trojan detection. In: 2015 European Conference on Circuit Theory and Design (ECCTD), pp. 1\u20134. IEEE (2015)","DOI":"10.1109\/ECCTD.2015.7300085"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Qu, G., Yuan, L.: Design THINGS for the internet of things-an EDA perspective. In: International Conference on Computer-Aided Design (ICCAD), pp. 411\u2013416. IEEE (2014)","DOI":"10.1109\/ICCAD.2014.7001384"},{"key":"5_CR25","unstructured":"Rabaey, J.M., Chandrakasan, A.P., Nikolic, B.: Digital Integrated Circuits, vol. 2. Prentice Hall (2002)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Rai, D., Lach, J.: Performance of delay-based trojan detection under parameter variations. In: Hardware-Oriented Security and Trust, pp. 58\u201365. IEEE (2009)","DOI":"10.1109\/HST.2009.5224966"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Rathmair, M., Schupfer, F.: Hardware Trojan detection by specifying malicious circuit properties. In: Electronics Information and Emergency Communication, pp. 317\u2013320. IEEE (2013)","DOI":"10.1109\/ICEIEC.2013.6835515"},{"issue":"1","key":"5_CR28","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MDT.2010.7","volume":"27","author":"M Tehranipoor","year":"2010","unstructured":"Tehranipoor, M., Koushanfar, F.: A survey of hardware trojan taxonomy and detection. IEEE Des. Test Comput. 27(1), 10\u201325 (2010)","journal-title":"IEEE Des. Test Comput."},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Wang, L., Xie, H., Luo, H.: Malicious circuitry detection using transient power analysis for IC security. In: Quality, Reliability, Risk, Maintenance, and Safety Engineering, pp. 1164\u20131167. IEEE (2013)","DOI":"10.1109\/QR2MSE.2013.6625774"},{"issue":"3","key":"5_CR30","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1109\/TIFS.2011.2157341","volume":"6","author":"S Wei","year":"2011","unstructured":"Wei, S., Meguerdichian, S., Potkonjak, M.: Malicious circuitry detection using thermal conditioning. IEEE Trans. Inf. Forensics Secur. 6(3), 1136\u20131145 (2011)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"5_CR31","unstructured":"Weste, N., Harris, D.: CMOS VLSI Design: A Circuits and Systems Perspective. Pearson (2011)"},{"issue":"1","key":"5_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2906147","volume":"22","author":"K Xiao","year":"2016","unstructured":"Xiao, K., Forte, D., Jin, Y., Karri, R., Bhunia, S., Tehranipoor, M.: Hardware Trojans: lessons learned after one decade of research. ACM Transactions on Design Automation of Electronic Systems 22(1), 1\u201323 (2016)","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Zhang, X., Tehranipoor, M.: Detecting hardware Trojans in third-party digital IP cores. In: Hardware-Oriented Security and Trust (HOST), pp. 67\u201370. IEEE (2011)","DOI":"10.1109\/HST.2011.5954998"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53946-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T11:20:42Z","timestamp":1749986442000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53946-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319539454","9783319539461"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53946-1_5","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"16 February 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FTSCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Formal Techniques for Safety-Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ftscs2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ftscs.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}