28 citations · 71 across the 10 of their papers we have counts for
11 papers
A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
Roberto Metere, Changyu Dong
Programs using random values can either make all choices in advance (eagerly) or sample as needed (lazily). In formal proofs, we focus on indistinguishability between two lazy prog…
An Overview of Cyber Security and Privacy on the Electric Vehicle Charging Infrastructure
Roberto Metere, Zoya Pourmirza, Sara Walker +1
Electric vehicles (EVs) are key to alleviate our dependency on fossil fuels. The future smart grid is expected to be populated by millions of EVs equipped with high-demand batterie…
cyberaCTIve: a STIX-based Tool for Cyber Threat Intelligence in Complex Models
Ricardo M. Czekster, Roberto Metere, Charles Morisset
Cyber threat intelligence (CTI) is practical real-world information that is collected with the purpose of assessing threats in cyber-physical systems (CPS). A practical notation fo…
Automating Cryptographic Protocol Language Generation from Structured Specifications
Roberto Metere, Luca Arnaboldi
Security of cryptographic protocols can be analysed by creating a model in a formal language and verifying the model in a tool. All such tools focus on the last part of the analysi…
Securing the Electric Vehicle Charging Infrastructure
Roberto Metere, Myriam Neaimeh, Charles Morisset +3
Electric Vehicles (EVs) can help alleviate our reliance on fossil fuels for transport and electricity systems. However, charging millions of EV batteries requires management to pre…
Modelling Load-Changing Attacks in Cyber-Physical Systems
Luca Arnaboldi, Ricardo M. Czekster, Roberto Metere +1
Cyber-Physical Systems (CPS) are present in many settings addressing a myriad of purposes. Examples are Internet-of-Things (IoT) or sensing software embedded in appliances or even…
Towards a Data Centric Approach for the Design and Verification of Cryptographic Protocols
Luca Arnaboldi, Roberto Metere
We propose MetaCP, a Meta Cryptography Protocol verification tool, as an automated tool simplifying the design of security protocols through a graphical interface. The graphical in…
TrABin: Trustworthy Analyses of Binaries
Andreas Lindner, Roberto Guanciale, Roberto Metere
Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analy…
Sound Transpilation from Binary to Machine-Independent Code
Roberto Metere, Andreas Lindner, Roberto Guanciale
In order to handle the complexity and heterogeneity of mod- ern instruction set architectures, analysis platforms share a common design, the adoption of hardware-independent interm…
Analysing and Patching SPEKE in ISO/IEC
Feng Hao, Roberto Metere, Siamak F. Shahandashti +1
Simple Password Exponential Key Exchange (SPEKE) is a well-known Password Authenticated Key Exchange (PAKE) protocol that has been used in Blackberry phones for secure messaging an…
Automated Cryptographic Analysis of the Pedersen Commitment Scheme
Roberto Metere, Changyu Dong
Aiming for strong security assurance, recently there has been an increasing interest in formal verification of cryptographic constructions. This paper presents a mechanised formal…